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 ) ) )