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=BaseG
mulgass.t ·˙=G
Assertion mulgass GGrpMNXB M N·˙X=M·˙N·˙X

Proof

Step Hyp Ref Expression
1 mulgass.b B=BaseG
2 mulgass.t ·˙=G
3 simpr1 GGrpMNXBM
4 elznn0 MMM0M0
5 4 simprbi MM0M0
6 3 5 syl GGrpMNXBM0M0
7 simpr2 GGrpMNXBN
8 elznn0 NNN0N0
9 8 simprbi NN0N0
10 7 9 syl GGrpMNXBN0N0
11 grpmnd GGrpGMnd
12 11 ad2antrr GGrpMNXBM0N0GMnd
13 simprl GGrpMNXBM0N0M0
14 simprr GGrpMNXBM0N0N0
15 simplr3 GGrpMNXBM0N0XB
16 1 2 mulgnn0ass GMndM0N0XB M N·˙X=M·˙N·˙X
17 12 13 14 15 16 syl13anc GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
18 17 ex GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
19 3 zcnd GGrpMNXBM
20 7 zcnd GGrpMNXBN
21 19 20 mulneg1d GGrpMNXB- M N= M N
22 21 adantr GGrpMNXBM0N0- M N= M N
23 22 oveq1d GGrpMNXBM0N0- M N·˙X= M N·˙X
24 11 ad2antrr GGrpMNXBM0N0GMnd
25 simprl GGrpMNXBM0N0M0
26 simprr GGrpMNXBM0N0N0
27 simpr3 GGrpMNXBXB
28 27 adantr GGrpMNXBM0N0XB
29 1 2 mulgnn0ass GMndM0N0XB- M N·˙X=- M·˙N·˙X
30 24 25 26 28 29 syl13anc GGrpMNXBM0N0- M N·˙X=- M·˙N·˙X
31 23 30 eqtr3d GGrpMNXBM0N0 M N·˙X=- M·˙N·˙X
32 fveq2 M N·˙X=- M·˙N·˙XinvgG M N·˙X=invgG- M·˙N·˙X
33 simpl GGrpMNXBGGrp
34 3 7 zmulcld GGrpMNXB M N
35 eqid invgG=invgG
36 1 2 35 mulgneg GGrp M NXB M N·˙X=invgG M N·˙X
37 33 34 27 36 syl3anc GGrpMNXB M N·˙X=invgG M N·˙X
38 37 fveq2d GGrpMNXBinvgG M N·˙X=invgGinvgG M N·˙X
39 1 2 mulgcl GGrp M NXB M N·˙XB
40 33 34 27 39 syl3anc GGrpMNXB M N·˙XB
41 1 35 grpinvinv GGrp M N·˙XBinvgGinvgG M N·˙X= M N·˙X
42 40 41 syldan GGrpMNXBinvgGinvgG M N·˙X= M N·˙X
43 38 42 eqtrd GGrpMNXBinvgG M N·˙X= M N·˙X
44 1 2 mulgcl GGrpNXBN·˙XB
45 33 7 27 44 syl3anc GGrpMNXBN·˙XB
46 1 2 35 mulgneg GGrpMN·˙XB- M·˙N·˙X=invgGM·˙N·˙X
47 33 3 45 46 syl3anc GGrpMNXB- M·˙N·˙X=invgGM·˙N·˙X
48 47 fveq2d GGrpMNXBinvgG- M·˙N·˙X=invgGinvgGM·˙N·˙X
49 1 2 mulgcl GGrpMN·˙XBM·˙N·˙XB
50 33 3 45 49 syl3anc GGrpMNXBM·˙N·˙XB
51 1 35 grpinvinv GGrpM·˙N·˙XBinvgGinvgGM·˙N·˙X=M·˙N·˙X
52 50 51 syldan GGrpMNXBinvgGinvgGM·˙N·˙X=M·˙N·˙X
53 48 52 eqtrd GGrpMNXBinvgG- M·˙N·˙X=M·˙N·˙X
54 43 53 eqeq12d GGrpMNXBinvgG M N·˙X=invgG- M·˙N·˙X M N·˙X=M·˙N·˙X
55 32 54 syl5ib GGrpMNXB M N·˙X=- M·˙N·˙X M N·˙X=M·˙N·˙X
56 55 imp GGrpMNXB M N·˙X=- M·˙N·˙X M N·˙X=M·˙N·˙X
57 31 56 syldan GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
58 57 ex GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
59 11 ad2antrr GGrpMNXBM0N0GMnd
60 simprl GGrpMNXBM0N0M0
61 simprr GGrpMNXBM0N0N0
62 27 adantr GGrpMNXBM0N0XB
63 1 2 mulgnn0ass GMndM0N0XBM- N·˙X=M·˙- N·˙X
64 59 60 61 62 63 syl13anc GGrpMNXBM0N0M- N·˙X=M·˙- N·˙X
65 19 20 mulneg2d GGrpMNXBM- N= M N
66 65 adantr GGrpMNXBM0N0M- N= M N
67 66 oveq1d GGrpMNXBM0N0M- N·˙X= M N·˙X
68 1 2 35 mulgneg GGrpNXB- N·˙X=invgGN·˙X
69 33 7 27 68 syl3anc GGrpMNXB- N·˙X=invgGN·˙X
70 69 oveq2d GGrpMNXBM·˙- N·˙X=M·˙invgGN·˙X
71 1 2 35 mulgneg2 GGrpMN·˙XB- M·˙N·˙X=M·˙invgGN·˙X
72 33 3 45 71 syl3anc GGrpMNXB- M·˙N·˙X=M·˙invgGN·˙X
73 70 72 eqtr4d GGrpMNXBM·˙- N·˙X=- M·˙N·˙X
74 73 adantr GGrpMNXBM0N0M·˙- N·˙X=- M·˙N·˙X
75 64 67 74 3eqtr3d GGrpMNXBM0N0 M N·˙X=- M·˙N·˙X
76 75 56 syldan GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
77 76 ex GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
78 11 ad2antrr GGrpMNXBM0N0GMnd
79 simprl GGrpMNXBM0N0M0
80 simprr GGrpMNXBM0N0N0
81 27 adantr GGrpMNXBM0N0XB
82 1 2 mulgnn0ass GMndM0N0XB- M- N·˙X=- M·˙- N·˙X
83 78 79 80 81 82 syl13anc GGrpMNXBM0N0- M- N·˙X=- M·˙- N·˙X
84 19 20 mul2negd GGrpMNXB- M- N= M N
85 84 oveq1d GGrpMNXB- M- N·˙X= M N·˙X
86 85 adantr GGrpMNXBM0N0- M- N·˙X= M N·˙X
87 33 adantr GGrpMNXBM0N0GGrp
88 3 adantr GGrpMNXBM0N0M
89 nn0z N0N
90 89 ad2antll GGrpMNXBM0N0N
91 1 2 mulgcl GGrpNXB- N·˙XB
92 87 90 81 91 syl3anc GGrpMNXBM0N0- N·˙XB
93 1 2 35 mulgneg2 GGrpM- N·˙XB- M·˙- N·˙X=M·˙invgG- N·˙X
94 87 88 92 93 syl3anc GGrpMNXBM0N0- M·˙- N·˙X=M·˙invgG- N·˙X
95 1 2 35 mulgneg GGrpNXB- N·˙X=invgG- N·˙X
96 87 90 81 95 syl3anc GGrpMNXBM0N0- N·˙X=invgG- N·˙X
97 20 negnegd GGrpMNXB- N=N
98 97 adantr GGrpMNXBM0N0- N=N
99 98 oveq1d GGrpMNXBM0N0- N·˙X=N·˙X
100 96 99 eqtr3d GGrpMNXBM0N0invgG- N·˙X=N·˙X
101 100 oveq2d GGrpMNXBM0N0M·˙invgG- N·˙X=M·˙N·˙X
102 94 101 eqtrd GGrpMNXBM0N0- M·˙- N·˙X=M·˙N·˙X
103 83 86 102 3eqtr3d GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
104 103 ex GGrpMNXBM0N0 M N·˙X=M·˙N·˙X
105 18 58 77 104 ccased GGrpMNXBM0M0N0N0 M N·˙X=M·˙N·˙X
106 6 10 105 mp2and GGrpMNXB M N·˙X=M·˙N·˙X