Metamath Proof Explorer

Theorem mulgdirlem

Description: Lemma for mulgdir . (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgnndir.b 
|- B = ( Base ` G )
mulgnndir.t 
|- .x. = ( .g ` G )
mulgnndir.p 
|- .+ = ( +g ` G )
Assertion mulgdirlem 
|- ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulgnndir.b 
 |-  B = ( Base ` G )
2 mulgnndir.t 
 |-  .x. = ( .g ` G )
3 mulgnndir.p 
 |-  .+ = ( +g ` G )
4 simpl1 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> G e. Grp )
5 4 grpmndd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> G e. Mnd )
6 simprl 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> M e. NN0 )
7 simprr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> N e. NN0 )
8 simpl23 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> X e. B )
9 1 2 3 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
10 5 6 7 8 9 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
11 10 anassrs 
 |-  ( ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ M e. NN0 ) /\ N e. NN0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
12 simpl1 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> G e. Grp )
13 simp22 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> N e. ZZ )
14 13 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> N e. ZZ )
15 simpl23 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> X e. B )
16 eqid 
 |-  ( invg ` G ) = ( invg ` G )
17 1 2 16 mulgneg 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( ( invg ` G ) ` ( N .x. X ) ) )
18 12 14 15 17 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( -u N .x. X ) = ( ( invg ` G ) ` ( N .x. X ) ) )
19 18 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( -u N .x. X ) .+ ( N .x. X ) ) = ( ( ( invg ` G ) ` ( N .x. X ) ) .+ ( N .x. X ) ) )
20 1 2 mulgcl 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )
21 12 14 15 20 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( N .x. X ) e. B )
22 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
23 1 3 22 16 grplinv 
 |-  ( ( G e. Grp /\ ( N .x. X ) e. B ) -> ( ( ( invg ` G ) ` ( N .x. X ) ) .+ ( N .x. X ) ) = ( 0g ` G ) )
24 12 21 23 syl2anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( invg ` G ) ` ( N .x. X ) ) .+ ( N .x. X ) ) = ( 0g ` G ) )
25 19 24 eqtrd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( -u N .x. X ) .+ ( N .x. X ) ) = ( 0g ` G ) )
26 25 oveq2d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( M + N ) .x. X ) .+ ( ( -u N .x. X ) .+ ( N .x. X ) ) ) = ( ( ( M + N ) .x. X ) .+ ( 0g ` G ) ) )
27 simpl3 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( M + N ) e. NN0 )
28 nn0z 
 |-  ( ( M + N ) e. NN0 -> ( M + N ) e. ZZ )
29 27 28 syl 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( M + N ) e. ZZ )
30 1 2 mulgcl 
 |-  ( ( G e. Grp /\ ( M + N ) e. ZZ /\ X e. B ) -> ( ( M + N ) .x. X ) e. B )
31 12 29 15 30 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M + N ) .x. X ) e. B )
32 1 3 22 grprid 
 |-  ( ( G e. Grp /\ ( ( M + N ) .x. X ) e. B ) -> ( ( ( M + N ) .x. X ) .+ ( 0g ` G ) ) = ( ( M + N ) .x. X ) )
33 12 31 32 syl2anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( M + N ) .x. X ) .+ ( 0g ` G ) ) = ( ( M + N ) .x. X ) )
34 26 33 eqtrd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( M + N ) .x. X ) .+ ( ( -u N .x. X ) .+ ( N .x. X ) ) ) = ( ( M + N ) .x. X ) )
35 nn0z 
 |-  ( -u N e. NN0 -> -u N e. ZZ )
36 35 ad2antll 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> -u N e. ZZ )
37 1 2 mulgcl 
 |-  ( ( G e. Grp /\ -u N e. ZZ /\ X e. B ) -> ( -u N .x. X ) e. B )
38 12 36 15 37 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( -u N .x. X ) e. B )
39 1 3 grpass 
 |-  ( ( G e. Grp /\ ( ( ( M + N ) .x. X ) e. B /\ ( -u N .x. X ) e. B /\ ( N .x. X ) e. B ) ) -> ( ( ( ( M + N ) .x. X ) .+ ( -u N .x. X ) ) .+ ( N .x. X ) ) = ( ( ( M + N ) .x. X ) .+ ( ( -u N .x. X ) .+ ( N .x. X ) ) ) )
40 12 31 38 21 39 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( ( M + N ) .x. X ) .+ ( -u N .x. X ) ) .+ ( N .x. X ) ) = ( ( ( M + N ) .x. X ) .+ ( ( -u N .x. X ) .+ ( N .x. X ) ) ) )
41 12 grpmndd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> G e. Mnd )
42 simprr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> -u N e. NN0 )
43 1 2 3 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( ( M + N ) e. NN0 /\ -u N e. NN0 /\ X e. B ) ) -> ( ( ( M + N ) + -u N ) .x. X ) = ( ( ( M + N ) .x. X ) .+ ( -u N .x. X ) ) )
44 41 27 42 15 43 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( M + N ) + -u N ) .x. X ) = ( ( ( M + N ) .x. X ) .+ ( -u N .x. X ) ) )
45 simp21 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> M e. ZZ )
46 45 zcnd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> M e. CC )
47 13 zcnd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> N e. CC )
48 46 47 addcld 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> ( M + N ) e. CC )
49 48 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( M + N ) e. CC )
50 47 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> N e. CC )
51 49 50 negsubd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M + N ) + -u N ) = ( ( M + N ) - N ) )
52 46 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> M e. CC )
53 52 50 pncand 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M + N ) - N ) = M )
54 51 53 eqtrd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M + N ) + -u N ) = M )
55 54 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( M + N ) + -u N ) .x. X ) = ( M .x. X ) )
56 44 55 eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( M + N ) .x. X ) .+ ( -u N .x. X ) ) = ( M .x. X ) )
57 56 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( ( M + N ) .x. X ) .+ ( -u N .x. X ) ) .+ ( N .x. X ) ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
58 40 57 eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( ( M + N ) .x. X ) .+ ( ( -u N .x. X ) .+ ( N .x. X ) ) ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
59 34 58 eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
60 59 anassrs 
 |-  ( ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ M e. NN0 ) /\ -u N e. NN0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
61 elznn0 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
62 61 simprbi 
 |-  ( N e. ZZ -> ( N e. NN0 \/ -u N e. NN0 ) )
63 13 62 syl 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> ( N e. NN0 \/ -u N e. NN0 ) )
64 63 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ M e. NN0 ) -> ( N e. NN0 \/ -u N e. NN0 ) )
65 11 60 64 mpjaodan 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ M e. NN0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
66 simpl1 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> G e. Grp )
67 45 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> M e. ZZ )
68 simpl23 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> X e. B )
69 1 2 mulgcl 
 |-  ( ( G e. Grp /\ M e. ZZ /\ X e. B ) -> ( M .x. X ) e. B )
70 66 67 68 69 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( M .x. X ) e. B )
71 67 znegcld 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> -u M e. ZZ )
72 1 2 mulgcl 
 |-  ( ( G e. Grp /\ -u M e. ZZ /\ X e. B ) -> ( -u M .x. X ) e. B )
73 66 71 68 72 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( -u M .x. X ) e. B )
74 28 3ad2ant3 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> ( M + N ) e. ZZ )
75 74 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( M + N ) e. ZZ )
76 66 75 68 30 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M + N ) .x. X ) e. B )
77 1 3 grpass 
 |-  ( ( G e. Grp /\ ( ( M .x. X ) e. B /\ ( -u M .x. X ) e. B /\ ( ( M + N ) .x. X ) e. B ) ) -> ( ( ( M .x. X ) .+ ( -u M .x. X ) ) .+ ( ( M + N ) .x. X ) ) = ( ( M .x. X ) .+ ( ( -u M .x. X ) .+ ( ( M + N ) .x. X ) ) ) )
78 66 70 73 76 77 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( ( M .x. X ) .+ ( -u M .x. X ) ) .+ ( ( M + N ) .x. X ) ) = ( ( M .x. X ) .+ ( ( -u M .x. X ) .+ ( ( M + N ) .x. X ) ) ) )
79 1 2 16 mulgneg 
 |-  ( ( G e. Grp /\ M e. ZZ /\ X e. B ) -> ( -u M .x. X ) = ( ( invg ` G ) ` ( M .x. X ) ) )
80 66 67 68 79 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( -u M .x. X ) = ( ( invg ` G ) ` ( M .x. X ) ) )
81 80 oveq2d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M .x. X ) .+ ( -u M .x. X ) ) = ( ( M .x. X ) .+ ( ( invg ` G ) ` ( M .x. X ) ) ) )
82 1 3 22 16 grprinv 
 |-  ( ( G e. Grp /\ ( M .x. X ) e. B ) -> ( ( M .x. X ) .+ ( ( invg ` G ) ` ( M .x. X ) ) ) = ( 0g ` G ) )
83 66 70 82 syl2anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M .x. X ) .+ ( ( invg ` G ) ` ( M .x. X ) ) ) = ( 0g ` G ) )
84 81 83 eqtrd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M .x. X ) .+ ( -u M .x. X ) ) = ( 0g ` G ) )
85 84 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( ( M .x. X ) .+ ( -u M .x. X ) ) .+ ( ( M + N ) .x. X ) ) = ( ( 0g ` G ) .+ ( ( M + N ) .x. X ) ) )
86 1 3 22 grplid 
 |-  ( ( G e. Grp /\ ( ( M + N ) .x. X ) e. B ) -> ( ( 0g ` G ) .+ ( ( M + N ) .x. X ) ) = ( ( M + N ) .x. X ) )
87 66 76 86 syl2anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( 0g ` G ) .+ ( ( M + N ) .x. X ) ) = ( ( M + N ) .x. X ) )
88 85 87 eqtrd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( ( M .x. X ) .+ ( -u M .x. X ) ) .+ ( ( M + N ) .x. X ) ) = ( ( M + N ) .x. X ) )
89 66 grpmndd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> G e. Mnd )
90 simpr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> -u M e. NN0 )
91 simpl3 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( M + N ) e. NN0 )
92 1 2 3 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( -u M e. NN0 /\ ( M + N ) e. NN0 /\ X e. B ) ) -> ( ( -u M + ( M + N ) ) .x. X ) = ( ( -u M .x. X ) .+ ( ( M + N ) .x. X ) ) )
93 89 90 91 68 92 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( -u M + ( M + N ) ) .x. X ) = ( ( -u M .x. X ) .+ ( ( M + N ) .x. X ) ) )
94 46 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> M e. CC )
95 94 negcld 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> -u M e. CC )
96 48 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( M + N ) e. CC )
97 95 96 addcomd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( -u M + ( M + N ) ) = ( ( M + N ) + -u M ) )
98 96 94 negsubd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M + N ) + -u M ) = ( ( M + N ) - M ) )
99 47 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> N e. CC )
100 94 99 pncan2d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M + N ) - M ) = N )
101 97 98 100 3eqtrd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( -u M + ( M + N ) ) = N )
102 101 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( -u M + ( M + N ) ) .x. X ) = ( N .x. X ) )
103 93 102 eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( -u M .x. X ) .+ ( ( M + N ) .x. X ) ) = ( N .x. X ) )
104 103 oveq2d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M .x. X ) .+ ( ( -u M .x. X ) .+ ( ( M + N ) .x. X ) ) ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
105 78 88 104 3eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) /\ -u M e. NN0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )
106 elznn0 
 |-  ( M e. ZZ <-> ( M e. RR /\ ( M e. NN0 \/ -u M e. NN0 ) ) )
107 106 simprbi 
 |-  ( M e. ZZ -> ( M e. NN0 \/ -u M e. NN0 ) )
108 45 107 syl 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> ( M e. NN0 \/ -u M e. NN0 ) )
109 65 105 108 mpjaodan 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) /\ ( M + N ) e. NN0 ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )