Metamath Proof Explorer

Theorem mulgdi

Description: Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgdi.b 
|- B = ( Base ` G )
mulgdi.m 
|- .x. = ( .g ` G )
mulgdi.p 
|- .+ = ( +g ` G )
Assertion mulgdi 
|- ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 mulgdi.b 
 |-  B = ( Base ` G )
2 mulgdi.m 
 |-  .x. = ( .g ` G )
3 mulgdi.p 
 |-  .+ = ( +g ` G )
4 ablcmn 
 |-  ( G e. Abel -> G e. CMnd )
5 4 ad2antrr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ M e. NN0 ) -> G e. CMnd )
6 simpr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ M e. NN0 ) -> M e. NN0 )
7 simplr2 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ M e. NN0 ) -> X e. B )
8 simplr3 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ M e. NN0 ) -> Y e. B )
9 1 2 3 mulgnn0di 
 |-  ( ( G e. CMnd /\ ( M e. NN0 /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
10 5 6 7 8 9 syl13anc 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ M e. NN0 ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
11 4 ad2antrr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> G e. CMnd )
12 simpr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> -u M e. NN0 )
13 simpr2 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> X e. B )
14 13 adantr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> X e. B )
15 simpr3 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> Y e. B )
16 15 adantr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> Y e. B )
17 1 2 3 mulgnn0di 
 |-  ( ( G e. CMnd /\ ( -u M e. NN0 /\ X e. B /\ Y e. B ) ) -> ( -u M .x. ( X .+ Y ) ) = ( ( -u M .x. X ) .+ ( -u M .x. Y ) ) )
18 11 12 14 16 17 syl13anc 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( -u M .x. ( X .+ Y ) ) = ( ( -u M .x. X ) .+ ( -u M .x. Y ) ) )
19 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
20 19 adantr 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> G e. Grp )
21 simpr1 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> M e. ZZ )
22 1 3 grpcl 
 |-  ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
23 20 13 15 22 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( X .+ Y ) e. B )
24 eqid 
 |-  ( invg ` G ) = ( invg ` G )
25 1 2 24 mulgneg 
 |-  ( ( G e. Grp /\ M e. ZZ /\ ( X .+ Y ) e. B ) -> ( -u M .x. ( X .+ Y ) ) = ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) )
26 20 21 23 25 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( -u M .x. ( X .+ Y ) ) = ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) )
27 26 adantr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( -u M .x. ( X .+ Y ) ) = ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) )
28 1 2 24 mulgneg 
 |-  ( ( G e. Grp /\ M e. ZZ /\ X e. B ) -> ( -u M .x. X ) = ( ( invg ` G ) ` ( M .x. X ) ) )
29 20 21 13 28 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( -u M .x. X ) = ( ( invg ` G ) ` ( M .x. X ) ) )
30 1 2 24 mulgneg 
 |-  ( ( G e. Grp /\ M e. ZZ /\ Y e. B ) -> ( -u M .x. Y ) = ( ( invg ` G ) ` ( M .x. Y ) ) )
31 20 21 15 30 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( -u M .x. Y ) = ( ( invg ` G ) ` ( M .x. Y ) ) )
32 29 31 oveq12d 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( ( -u M .x. X ) .+ ( -u M .x. Y ) ) = ( ( ( invg ` G ) ` ( M .x. X ) ) .+ ( ( invg ` G ) ` ( M .x. Y ) ) ) )
33 32 adantr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( -u M .x. X ) .+ ( -u M .x. Y ) ) = ( ( ( invg ` G ) ` ( M .x. X ) ) .+ ( ( invg ` G ) ` ( M .x. Y ) ) ) )
34 18 27 33 3eqtr3d 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) = ( ( ( invg ` G ) ` ( M .x. X ) ) .+ ( ( invg ` G ) ` ( M .x. Y ) ) ) )
35 simpl 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> G e. Abel )
36 1 2 mulgcl 
 |-  ( ( G e. Grp /\ M e. ZZ /\ X e. B ) -> ( M .x. X ) e. B )
37 20 21 13 36 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M .x. X ) e. B )
38 1 2 mulgcl 
 |-  ( ( G e. Grp /\ M e. ZZ /\ Y e. B ) -> ( M .x. Y ) e. B )
39 20 21 15 38 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M .x. Y ) e. B )
40 1 3 24 ablinvadd 
 |-  ( ( G e. Abel /\ ( M .x. X ) e. B /\ ( M .x. Y ) e. B ) -> ( ( invg ` G ) ` ( ( M .x. X ) .+ ( M .x. Y ) ) ) = ( ( ( invg ` G ) ` ( M .x. X ) ) .+ ( ( invg ` G ) ` ( M .x. Y ) ) ) )
41 35 37 39 40 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( ( invg ` G ) ` ( ( M .x. X ) .+ ( M .x. Y ) ) ) = ( ( ( invg ` G ) ` ( M .x. X ) ) .+ ( ( invg ` G ) ` ( M .x. Y ) ) ) )
42 41 adantr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( invg ` G ) ` ( ( M .x. X ) .+ ( M .x. Y ) ) ) = ( ( ( invg ` G ) ` ( M .x. X ) ) .+ ( ( invg ` G ) ` ( M .x. Y ) ) ) )
43 34 42 eqtr4d 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) = ( ( invg ` G ) ` ( ( M .x. X ) .+ ( M .x. Y ) ) ) )
44 43 fveq2d 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) ) = ( ( invg ` G ) ` ( ( invg ` G ) ` ( ( M .x. X ) .+ ( M .x. Y ) ) ) ) )
45 1 2 mulgcl 
 |-  ( ( G e. Grp /\ M e. ZZ /\ ( X .+ Y ) e. B ) -> ( M .x. ( X .+ Y ) ) e. B )
46 20 21 23 45 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) e. B )
47 46 adantr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( M .x. ( X .+ Y ) ) e. B )
48 1 24 grpinvinv 
 |-  ( ( G e. Grp /\ ( M .x. ( X .+ Y ) ) e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) ) = ( M .x. ( X .+ Y ) ) )
49 20 47 48 syl2an2r 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( M .x. ( X .+ Y ) ) ) ) = ( M .x. ( X .+ Y ) ) )
50 1 3 grpcl 
 |-  ( ( G e. Grp /\ ( M .x. X ) e. B /\ ( M .x. Y ) e. B ) -> ( ( M .x. X ) .+ ( M .x. Y ) ) e. B )
51 20 37 39 50 syl3anc 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( ( M .x. X ) .+ ( M .x. Y ) ) e. B )
52 51 adantr 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( M .x. X ) .+ ( M .x. Y ) ) e. B )
53 1 24 grpinvinv 
 |-  ( ( G e. Grp /\ ( ( M .x. X ) .+ ( M .x. Y ) ) e. B ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( ( M .x. X ) .+ ( M .x. Y ) ) ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
54 20 52 53 syl2an2r 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( ( invg ` G ) ` ( ( invg ` G ) ` ( ( M .x. X ) .+ ( M .x. Y ) ) ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
55 44 49 54 3eqtr3d 
 |-  ( ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) /\ -u M e. NN0 ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )
56 elznn0 
 |-  ( M e. ZZ <-> ( M e. RR /\ ( M e. NN0 \/ -u M e. NN0 ) ) )
57 56 simprbi 
 |-  ( M e. ZZ -> ( M e. NN0 \/ -u M e. NN0 ) )
58 21 57 syl 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M e. NN0 \/ -u M e. NN0 ) )
59 10 55 58 mpjaodan 
 |-  ( ( G e. Abel /\ ( M e. ZZ /\ X e. B /\ Y e. B ) ) -> ( M .x. ( X .+ Y ) ) = ( ( M .x. X ) .+ ( M .x. Y ) ) )