Metamath Proof Explorer


Theorem mulgnn0dir

Description: Sum of group multiples, generalized to NN0 . (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnndir.b B = Base G
mulgnndir.t · ˙ = G
mulgnndir.p + ˙ = + G
Assertion mulgnn0dir G Mnd M 0 N 0 X B M + N · ˙ X = M · ˙ X + ˙ N · ˙ X

Proof

Step Hyp Ref Expression
1 mulgnndir.b B = Base G
2 mulgnndir.t · ˙ = G
3 mulgnndir.p + ˙ = + G
4 mndsgrp Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for |- ( G e. Mnd -> G e. Smgrp ) with typecode |-
5 4 adantr Could not format ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp ) : No typesetting found for |- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp ) with typecode |-
6 5 ad2antrr Could not format ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> G e. Smgrp ) : No typesetting found for |- ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> G e. Smgrp ) with typecode |-
7 simplr G Mnd M 0 N 0 X B M N M
8 simpr G Mnd M 0 N 0 X B M N N
9 simpr3 G Mnd M 0 N 0 X B X B
10 9 ad2antrr G Mnd M 0 N 0 X B M N X B
11 1 2 3 mulgnndir Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) : No typesetting found for |- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) with typecode |-
12 6 7 8 10 11 syl13anc G Mnd M 0 N 0 X B M N M + N · ˙ X = M · ˙ X + ˙ N · ˙ X
13 simpll G Mnd M 0 N 0 X B N = 0 G Mnd
14 simpr1 G Mnd M 0 N 0 X B M 0
15 14 adantr G Mnd M 0 N 0 X B N = 0 M 0
16 simplr3 G Mnd M 0 N 0 X B N = 0 X B
17 1 2 13 15 16 mulgnn0cld G Mnd M 0 N 0 X B N = 0 M · ˙ X B
18 eqid 0 G = 0 G
19 1 3 18 mndrid G Mnd M · ˙ X B M · ˙ X + ˙ 0 G = M · ˙ X
20 13 17 19 syl2anc G Mnd M 0 N 0 X B N = 0 M · ˙ X + ˙ 0 G = M · ˙ X
21 simpr G Mnd M 0 N 0 X B N = 0 N = 0
22 21 oveq1d G Mnd M 0 N 0 X B N = 0 N · ˙ X = 0 · ˙ X
23 1 18 2 mulg0 X B 0 · ˙ X = 0 G
24 16 23 syl G Mnd M 0 N 0 X B N = 0 0 · ˙ X = 0 G
25 22 24 eqtrd G Mnd M 0 N 0 X B N = 0 N · ˙ X = 0 G
26 25 oveq2d G Mnd M 0 N 0 X B N = 0 M · ˙ X + ˙ N · ˙ X = M · ˙ X + ˙ 0 G
27 21 oveq2d G Mnd M 0 N 0 X B N = 0 M + N = M + 0
28 15 nn0cnd G Mnd M 0 N 0 X B N = 0 M
29 28 addridd G Mnd M 0 N 0 X B N = 0 M + 0 = M
30 27 29 eqtrd G Mnd M 0 N 0 X B N = 0 M + N = M
31 30 oveq1d G Mnd M 0 N 0 X B N = 0 M + N · ˙ X = M · ˙ X
32 20 26 31 3eqtr4rd G Mnd M 0 N 0 X B N = 0 M + N · ˙ X = M · ˙ X + ˙ N · ˙ X
33 32 adantlr G Mnd M 0 N 0 X B M N = 0 M + N · ˙ X = M · ˙ X + ˙ N · ˙ X
34 simpr2 G Mnd M 0 N 0 X B N 0
35 elnn0 N 0 N N = 0
36 34 35 sylib G Mnd M 0 N 0 X B N N = 0
37 36 adantr G Mnd M 0 N 0 X B M N N = 0
38 12 33 37 mpjaodan G Mnd M 0 N 0 X B M M + N · ˙ X = M · ˙ X + ˙ N · ˙ X
39 simpll G Mnd M 0 N 0 X B M = 0 G Mnd
40 simplr2 G Mnd M 0 N 0 X B M = 0 N 0
41 simplr3 G Mnd M 0 N 0 X B M = 0 X B
42 1 2 39 40 41 mulgnn0cld G Mnd M 0 N 0 X B M = 0 N · ˙ X B
43 1 3 18 mndlid G Mnd N · ˙ X B 0 G + ˙ N · ˙ X = N · ˙ X
44 39 42 43 syl2anc G Mnd M 0 N 0 X B M = 0 0 G + ˙ N · ˙ X = N · ˙ X
45 simpr G Mnd M 0 N 0 X B M = 0 M = 0
46 45 oveq1d G Mnd M 0 N 0 X B M = 0 M · ˙ X = 0 · ˙ X
47 41 23 syl G Mnd M 0 N 0 X B M = 0 0 · ˙ X = 0 G
48 46 47 eqtrd G Mnd M 0 N 0 X B M = 0 M · ˙ X = 0 G
49 48 oveq1d G Mnd M 0 N 0 X B M = 0 M · ˙ X + ˙ N · ˙ X = 0 G + ˙ N · ˙ X
50 45 oveq1d G Mnd M 0 N 0 X B M = 0 M + N = 0 + N
51 40 nn0cnd G Mnd M 0 N 0 X B M = 0 N
52 51 addlidd G Mnd M 0 N 0 X B M = 0 0 + N = N
53 50 52 eqtrd G Mnd M 0 N 0 X B M = 0 M + N = N
54 53 oveq1d G Mnd M 0 N 0 X B M = 0 M + N · ˙ X = N · ˙ X
55 44 49 54 3eqtr4rd G Mnd M 0 N 0 X B M = 0 M + N · ˙ X = M · ˙ X + ˙ N · ˙ X
56 elnn0 M 0 M M = 0
57 14 56 sylib G Mnd M 0 N 0 X B M M = 0
58 38 55 57 mpjaodan G Mnd M 0 N 0 X B M + N · ˙ X = M · ˙ X + ˙ N · ˙ X