Metamath Proof Explorer

Theorem mulgass

Description: Product of group multiples, generalized to ZZ . (Contributed by Mario Carneiro, 13-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 mulgass.b 
 |-  B = ( Base ` G )
2 mulgass.t 
 |-  .x. = ( .g ` G )
3 simpr1 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> M e. ZZ )
4 elznn0 
 |-  ( M e. ZZ <-> ( M e. RR /\ ( M e. NN0 \/ -u M e. NN0 ) ) )
5 4 simprbi 
 |-  ( M e. ZZ -> ( M e. NN0 \/ -u M e. NN0 ) )
6 3 5 syl 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M e. NN0 \/ -u M e. NN0 ) )
7 simpr2 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> N e. ZZ )
8 elznn0 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
9 8 simprbi 
 |-  ( N e. ZZ -> ( N e. NN0 \/ -u N e. NN0 ) )
10 7 9 syl 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( N e. NN0 \/ -u N e. NN0 ) )
11 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
12 11 ad2antrr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> G e. Mnd )
13 simprl 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> M e. NN0 )
14 simprr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> N e. NN0 )
15 simplr3 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> X e. B )
16 1 2 mulgnn0ass 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
17 12 13 14 15 16 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
18 17 ex 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
19 3 zcnd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> M e. CC )
20 7 zcnd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> N e. CC )
21 19 20 mulneg1d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( -u M x. N ) = -u ( M x. N ) )
22 21 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> ( -u M x. N ) = -u ( M x. N ) )
23 22 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> ( ( -u M x. N ) .x. X ) = ( -u ( M x. N ) .x. X ) )
24 11 ad2antrr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> G e. Mnd )
25 simprl 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> -u M e. NN0 )
26 simprr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> N e. NN0 )
27 simpr3 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> X e. B )
28 27 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> X e. B )
29 1 2 mulgnn0ass 
 |-  ( ( G e. Mnd /\ ( -u M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> ( ( -u M x. N ) .x. X ) = ( -u M .x. ( N .x. X ) ) )
30 24 25 26 28 29 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> ( ( -u M x. N ) .x. X ) = ( -u M .x. ( N .x. X ) ) )
31 23 30 eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> ( -u ( M x. N ) .x. X ) = ( -u M .x. ( N .x. X ) ) )
32 fveq2 
 |-  ( ( -u ( M x. N ) .x. X ) = ( -u M .x. ( N .x. X ) ) -> ( ( invg ` G ) ` ( -u ( M x. N ) .x. X ) ) = ( ( invg ` G ) ` ( -u M .x. ( N .x. X ) ) ) )
33 simpl 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> G e. Grp )
34 3 7 zmulcld 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M x. N ) e. ZZ )
35 eqid 
 |-  ( invg ` G ) = ( invg ` G )
36 1 2 35 mulgneg 
 |-  ( ( G e. Grp /\ ( M x. N ) e. ZZ /\ X e. B ) -> ( -u ( M x. N ) .x. X ) = ( ( invg ` G ) ` ( ( M x. N ) .x. X ) ) )
37 33 34 27 36 syl3anc 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( -u ( M x. N ) .x. X ) = ( ( invg ` G ) ` ( ( M x. N ) .x. X ) ) )
38 37 fveq2d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( invg ` G ) ` ( -u ( M x. N ) .x. X ) ) = ( ( invg ` G ) ` ( ( invg ` G ) ` ( ( M x. N ) .x. X ) ) ) )
39 1 2 mulgcl 
 |-  ( ( G e. Grp /\ ( M x. N ) e. ZZ /\ X e. B ) -> ( ( M x. N ) .x. X ) e. B )
40 33 34 27 39 syl3anc 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M x. N ) .x. X ) e. B )
41 1 35 grpinvinv 
 |-  ( ( G e. Grp /\ ( ( M x. N ) .x. X ) e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( ( M x. N ) .x. X ) ) ) = ( ( M x. N ) .x. X ) )
42 40 41 syldan 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( ( M x. N ) .x. X ) ) ) = ( ( M x. N ) .x. X ) )
43 38 42 eqtrd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( invg ` G ) ` ( -u ( M x. N ) .x. X ) ) = ( ( M x. N ) .x. X ) )
44 1 2 mulgcl 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N .x. X ) e. B )
45 33 7 27 44 syl3anc 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( N .x. X ) e. B )
46 1 2 35 mulgneg 
 |-  ( ( G e. Grp /\ M e. ZZ /\ ( N .x. X ) e. B ) -> ( -u M .x. ( N .x. X ) ) = ( ( invg ` G ) ` ( M .x. ( N .x. X ) ) ) )
47 33 3 45 46 syl3anc 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( -u M .x. ( N .x. X ) ) = ( ( invg ` G ) ` ( M .x. ( N .x. X ) ) ) )
48 47 fveq2d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( invg ` G ) ` ( -u M .x. ( N .x. X ) ) ) = ( ( invg ` G ) ` ( ( invg ` G ) ` ( M .x. ( N .x. X ) ) ) ) )
49 1 2 mulgcl 
 |-  ( ( G e. Grp /\ M e. ZZ /\ ( N .x. X ) e. B ) -> ( M .x. ( N .x. X ) ) e. B )
50 33 3 45 49 syl3anc 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M .x. ( N .x. X ) ) e. B )
51 1 35 grpinvinv 
 |-  ( ( G e. Grp /\ ( M .x. ( N .x. X ) ) e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( M .x. ( N .x. X ) ) ) ) = ( M .x. ( N .x. X ) ) )
52 50 51 syldan 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( M .x. ( N .x. X ) ) ) ) = ( M .x. ( N .x. X ) ) )
53 48 52 eqtrd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( invg ` G ) ` ( -u M .x. ( N .x. X ) ) ) = ( M .x. ( N .x. X ) ) )
54 43 53 eqeq12d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( ( invg ` G ) ` ( -u ( M x. N ) .x. X ) ) = ( ( invg ` G ) ` ( -u M .x. ( N .x. X ) ) ) <-> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
55 32 54 syl5ib 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( -u ( M x. N ) .x. X ) = ( -u M .x. ( N .x. X ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
56 55 imp 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u ( M x. N ) .x. X ) = ( -u M .x. ( N .x. X ) ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
57 31 56 syldan 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ N e. NN0 ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
58 57 ex 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( -u M e. NN0 /\ N e. NN0 ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
59 11 ad2antrr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> G e. Mnd )
60 simprl 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> M e. NN0 )
61 simprr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> -u N e. NN0 )
62 27 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> X e. B )
63 1 2 mulgnn0ass 
 |-  ( ( G e. Mnd /\ ( M e. NN0 /\ -u N e. NN0 /\ X e. B ) ) -> ( ( M x. -u N ) .x. X ) = ( M .x. ( -u N .x. X ) ) )
64 59 60 61 62 63 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M x. -u N ) .x. X ) = ( M .x. ( -u N .x. X ) ) )
65 19 20 mulneg2d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M x. -u N ) = -u ( M x. N ) )
66 65 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( M x. -u N ) = -u ( M x. N ) )
67 66 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M x. -u N ) .x. X ) = ( -u ( M x. N ) .x. X ) )
68 1 2 35 mulgneg 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( ( invg ` G ) ` ( N .x. X ) ) )
69 33 7 27 68 syl3anc 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( -u N .x. X ) = ( ( invg ` G ) ` ( N .x. X ) ) )
70 69 oveq2d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M .x. ( -u N .x. X ) ) = ( M .x. ( ( invg ` G ) ` ( N .x. X ) ) ) )
71 1 2 35 mulgneg2 
 |-  ( ( G e. Grp /\ M e. ZZ /\ ( N .x. X ) e. B ) -> ( -u M .x. ( N .x. X ) ) = ( M .x. ( ( invg ` G ) ` ( N .x. X ) ) ) )
72 33 3 45 71 syl3anc 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( -u M .x. ( N .x. X ) ) = ( M .x. ( ( invg ` G ) ` ( N .x. X ) ) ) )
73 70 72 eqtr4d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( M .x. ( -u N .x. X ) ) = ( -u M .x. ( N .x. X ) ) )
74 73 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( M .x. ( -u N .x. X ) ) = ( -u M .x. ( N .x. X ) ) )
75 64 67 74 3eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( -u ( M x. N ) .x. X ) = ( -u M .x. ( N .x. X ) ) )
76 75 56 syldan 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
77 76 ex 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M e. NN0 /\ -u N e. NN0 ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
78 11 ad2antrr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> G e. Mnd )
79 simprl 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> -u M e. NN0 )
80 simprr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> -u N e. NN0 )
81 27 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> X e. B )
82 1 2 mulgnn0ass 
 |-  ( ( G e. Mnd /\ ( -u M e. NN0 /\ -u N e. NN0 /\ X e. B ) ) -> ( ( -u M x. -u N ) .x. X ) = ( -u M .x. ( -u N .x. X ) ) )
83 78 79 80 81 82 syl13anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( ( -u M x. -u N ) .x. X ) = ( -u M .x. ( -u N .x. X ) ) )
84 19 20 mul2negd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( -u M x. -u N ) = ( M x. N ) )
85 84 oveq1d 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( -u M x. -u N ) .x. X ) = ( ( M x. N ) .x. X ) )
86 85 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( ( -u M x. -u N ) .x. X ) = ( ( M x. N ) .x. X ) )
87 33 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> G e. Grp )
88 3 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> M e. ZZ )
89 nn0z 
 |-  ( -u N e. NN0 -> -u N e. ZZ )
90 89 ad2antll 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> -u N e. ZZ )
91 1 2 mulgcl 
 |-  ( ( G e. Grp /\ -u N e. ZZ /\ X e. B ) -> ( -u N .x. X ) e. B )
92 87 90 81 91 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( -u N .x. X ) e. B )
93 1 2 35 mulgneg2 
 |-  ( ( G e. Grp /\ M e. ZZ /\ ( -u N .x. X ) e. B ) -> ( -u M .x. ( -u N .x. X ) ) = ( M .x. ( ( invg ` G ) ` ( -u N .x. X ) ) ) )
94 87 88 92 93 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( -u M .x. ( -u N .x. X ) ) = ( M .x. ( ( invg ` G ) ` ( -u N .x. X ) ) ) )
95 1 2 35 mulgneg 
 |-  ( ( G e. Grp /\ -u N e. ZZ /\ X e. B ) -> ( -u -u N .x. X ) = ( ( invg ` G ) ` ( -u N .x. X ) ) )
96 87 90 81 95 syl3anc 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( -u -u N .x. X ) = ( ( invg ` G ) ` ( -u N .x. X ) ) )
97 20 negnegd 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> -u -u N = N )
98 97 adantr 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> -u -u N = N )
99 98 oveq1d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( -u -u N .x. X ) = ( N .x. X ) )
100 96 99 eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( ( invg ` G ) ` ( -u N .x. X ) ) = ( N .x. X ) )
101 100 oveq2d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( M .x. ( ( invg ` G ) ` ( -u N .x. X ) ) ) = ( M .x. ( N .x. X ) ) )
102 94 101 eqtrd 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( -u M .x. ( -u N .x. X ) ) = ( M .x. ( N .x. X ) ) )
103 83 86 102 3eqtr3d 
 |-  ( ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) /\ ( -u M e. NN0 /\ -u N e. NN0 ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )
104 103 ex 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( -u M e. NN0 /\ -u N e. NN0 ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
105 18 58 77 104 ccased 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( ( M e. NN0 \/ -u M e. NN0 ) /\ ( N e. NN0 \/ -u N e. NN0 ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) ) )
106 6 10 105 mp2and 
 |-  ( ( G e. Grp /\ ( M e. ZZ /\ N e. ZZ /\ X e. B ) ) -> ( ( M x. N ) .x. X ) = ( M .x. ( N .x. X ) ) )