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