Metamath Proof Explorer

Theorem mulgaddcom

Description: The group multiple operator commutes with the group operation. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by AV, 31-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 mulgaddcom.b 
 |-  B = ( Base ` G )
2 mulgaddcom.t 
 |-  .x. = ( .g ` G )
3 mulgaddcom.p 
 |-  .+ = ( +g ` G )
4 oveq1 
 |-  ( x = 0 -> ( x .x. X ) = ( 0 .x. X ) )
5 4 oveq1d 
 |-  ( x = 0 -> ( ( x .x. X ) .+ X ) = ( ( 0 .x. X ) .+ X ) )
6 4 oveq2d 
 |-  ( x = 0 -> ( X .+ ( x .x. X ) ) = ( X .+ ( 0 .x. X ) ) )
7 5 6 eqeq12d 
 |-  ( x = 0 -> ( ( ( x .x. X ) .+ X ) = ( X .+ ( x .x. X ) ) <-> ( ( 0 .x. X ) .+ X ) = ( X .+ ( 0 .x. X ) ) ) )
8 oveq1 
 |-  ( x = y -> ( x .x. X ) = ( y .x. X ) )
9 8 oveq1d 
 |-  ( x = y -> ( ( x .x. X ) .+ X ) = ( ( y .x. X ) .+ X ) )
10 8 oveq2d 
 |-  ( x = y -> ( X .+ ( x .x. X ) ) = ( X .+ ( y .x. X ) ) )
11 9 10 eqeq12d 
 |-  ( x = y -> ( ( ( x .x. X ) .+ X ) = ( X .+ ( x .x. X ) ) <-> ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) )
12 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .x. X ) = ( ( y + 1 ) .x. X ) )
13 12 oveq1d 
 |-  ( x = ( y + 1 ) -> ( ( x .x. X ) .+ X ) = ( ( ( y + 1 ) .x. X ) .+ X ) )
14 12 oveq2d 
 |-  ( x = ( y + 1 ) -> ( X .+ ( x .x. X ) ) = ( X .+ ( ( y + 1 ) .x. X ) ) )
15 13 14 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( ( x .x. X ) .+ X ) = ( X .+ ( x .x. X ) ) <-> ( ( ( y + 1 ) .x. X ) .+ X ) = ( X .+ ( ( y + 1 ) .x. X ) ) ) )
16 oveq1 
 |-  ( x = -u y -> ( x .x. X ) = ( -u y .x. X ) )
17 16 oveq1d 
 |-  ( x = -u y -> ( ( x .x. X ) .+ X ) = ( ( -u y .x. X ) .+ X ) )
18 16 oveq2d 
 |-  ( x = -u y -> ( X .+ ( x .x. X ) ) = ( X .+ ( -u y .x. X ) ) )
19 17 18 eqeq12d 
 |-  ( x = -u y -> ( ( ( x .x. X ) .+ X ) = ( X .+ ( x .x. X ) ) <-> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) ) )
20 oveq1 
 |-  ( x = N -> ( x .x. X ) = ( N .x. X ) )
21 20 oveq1d 
 |-  ( x = N -> ( ( x .x. X ) .+ X ) = ( ( N .x. X ) .+ X ) )
22 20 oveq2d 
 |-  ( x = N -> ( X .+ ( x .x. X ) ) = ( X .+ ( N .x. X ) ) )
23 21 22 eqeq12d 
 |-  ( x = N -> ( ( ( x .x. X ) .+ X ) = ( X .+ ( x .x. X ) ) <-> ( ( N .x. X ) .+ X ) = ( X .+ ( N .x. X ) ) ) )
24 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
25 1 3 24 grplid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( 0g ` G ) .+ X ) = X )
26 1 24 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
27 26 adantl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( 0 .x. X ) = ( 0g ` G ) )
28 27 oveq1d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( 0 .x. X ) .+ X ) = ( ( 0g ` G ) .+ X ) )
29 27 oveq2d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( 0 .x. X ) ) = ( X .+ ( 0g ` G ) ) )
30 1 3 24 grprid 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( 0g ` G ) ) = X )
31 29 30 eqtrd 
 |-  ( ( G e. Grp /\ X e. B ) -> ( X .+ ( 0 .x. X ) ) = X )
32 25 28 31 3eqtr4d 
 |-  ( ( G e. Grp /\ X e. B ) -> ( ( 0 .x. X ) .+ X ) = ( X .+ ( 0 .x. X ) ) )
33 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
34 simp1 
 |-  ( ( G e. Grp /\ X e. B /\ y e. ZZ ) -> G e. Grp )
35 simp2 
 |-  ( ( G e. Grp /\ X e. B /\ y e. ZZ ) -> X e. B )
36 1 2 mulgcl 
 |-  ( ( G e. Grp /\ y e. ZZ /\ X e. B ) -> ( y .x. X ) e. B )
37 36 3com23 
 |-  ( ( G e. Grp /\ X e. B /\ y e. ZZ ) -> ( y .x. X ) e. B )
38 1 3 grpass 
 |-  ( ( G e. Grp /\ ( X e. B /\ ( y .x. X ) e. B /\ X e. B ) ) -> ( ( X .+ ( y .x. X ) ) .+ X ) = ( X .+ ( ( y .x. X ) .+ X ) ) )
39 34 35 37 35 38 syl13anc 
 |-  ( ( G e. Grp /\ X e. B /\ y e. ZZ ) -> ( ( X .+ ( y .x. X ) ) .+ X ) = ( X .+ ( ( y .x. X ) .+ X ) ) )
40 33 39 syl3an3 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> ( ( X .+ ( y .x. X ) ) .+ X ) = ( X .+ ( ( y .x. X ) .+ X ) ) )
41 40 adantr 
 |-  ( ( ( G e. Grp /\ X e. B /\ y e. NN0 ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( X .+ ( y .x. X ) ) .+ X ) = ( X .+ ( ( y .x. X ) .+ X ) ) )
42 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
43 42 3ad2ant1 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> G e. Mnd )
44 simp3 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> y e. NN0 )
45 simp2 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> X e. B )
46 1 2 3 mulgnn0p1 
 |-  ( ( G e. Mnd /\ y e. NN0 /\ X e. B ) -> ( ( y + 1 ) .x. X ) = ( ( y .x. X ) .+ X ) )
47 43 44 45 46 syl3anc 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> ( ( y + 1 ) .x. X ) = ( ( y .x. X ) .+ X ) )
48 47 eqeq1d 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> ( ( ( y + 1 ) .x. X ) = ( X .+ ( y .x. X ) ) <-> ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) )
49 48 biimpar 
 |-  ( ( ( G e. Grp /\ X e. B /\ y e. NN0 ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( y + 1 ) .x. X ) = ( X .+ ( y .x. X ) ) )
50 49 oveq1d 
 |-  ( ( ( G e. Grp /\ X e. B /\ y e. NN0 ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( ( y + 1 ) .x. X ) .+ X ) = ( ( X .+ ( y .x. X ) ) .+ X ) )
51 47 oveq2d 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> ( X .+ ( ( y + 1 ) .x. X ) ) = ( X .+ ( ( y .x. X ) .+ X ) ) )
52 51 adantr 
 |-  ( ( ( G e. Grp /\ X e. B /\ y e. NN0 ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( X .+ ( ( y + 1 ) .x. X ) ) = ( X .+ ( ( y .x. X ) .+ X ) ) )
53 41 50 52 3eqtr4d 
 |-  ( ( ( G e. Grp /\ X e. B /\ y e. NN0 ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( ( y + 1 ) .x. X ) .+ X ) = ( X .+ ( ( y + 1 ) .x. X ) ) )
54 53 ex 
 |-  ( ( G e. Grp /\ X e. B /\ y e. NN0 ) -> ( ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) -> ( ( ( y + 1 ) .x. X ) .+ X ) = ( X .+ ( ( y + 1 ) .x. X ) ) ) )
55 54 3expia 
 |-  ( ( G e. Grp /\ X e. B ) -> ( y e. NN0 -> ( ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) -> ( ( ( y + 1 ) .x. X ) .+ X ) = ( X .+ ( ( y + 1 ) .x. X ) ) ) ) )
56 nnz 
 |-  ( y e. NN -> y e. ZZ )
57 1 2 3 mulgaddcomlem 
 |-  ( ( ( G e. Grp /\ y e. ZZ /\ X e. B ) /\ ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) )
58 57 3exp1 
 |-  ( G e. Grp -> ( y e. ZZ -> ( X e. B -> ( ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) ) ) ) )
59 58 com23 
 |-  ( G e. Grp -> ( X e. B -> ( y e. ZZ -> ( ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) ) ) ) )
60 59 imp 
 |-  ( ( G e. Grp /\ X e. B ) -> ( y e. ZZ -> ( ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) ) ) )
61 56 60 syl5 
 |-  ( ( G e. Grp /\ X e. B ) -> ( y e. NN -> ( ( ( y .x. X ) .+ X ) = ( X .+ ( y .x. X ) ) -> ( ( -u y .x. X ) .+ X ) = ( X .+ ( -u y .x. X ) ) ) ) )
62 7 11 15 19 23 32 55 61 zindd 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N e. ZZ -> ( ( N .x. X ) .+ X ) = ( X .+ ( N .x. X ) ) ) )
63 62 ex 
 |-  ( G e. Grp -> ( X e. B -> ( N e. ZZ -> ( ( N .x. X ) .+ X ) = ( X .+ ( N .x. X ) ) ) ) )
64 63 com23 
 |-  ( G e. Grp -> ( N e. ZZ -> ( X e. B -> ( ( N .x. X ) .+ X ) = ( X .+ ( N .x. X ) ) ) ) )
65 64 3imp 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( ( N .x. X ) .+ X ) = ( X .+ ( N .x. X ) ) )