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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgaddcom.t ⊢ · = ( .g ‘ 𝐺 )
mulgaddcom.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulgaddcom ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgaddcom.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgaddcom.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgaddcom.p ⊢ + = ( +g ‘ 𝐺 )
4 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 · 𝑋 ) = ( 0 · 𝑋 ) )
5 4 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( ( 0 · 𝑋 ) + 𝑋 ) )
6 4 oveq2d ⊢ ( 𝑥 = 0 → ( 𝑋 + ( 𝑥 · 𝑋 ) ) = ( 𝑋 + ( 0 · 𝑋 ) ) )
7 5 6 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑥 · 𝑋 ) ) ↔ ( ( 0 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 0 · 𝑋 ) ) ) )
8 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝑋 ) = ( 𝑦 · 𝑋 ) )
9 8 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( ( 𝑦 · 𝑋 ) + 𝑋 ) )
10 8 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑋 + ( 𝑥 · 𝑋 ) ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑥 · 𝑋 ) ) ↔ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) )
12 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · 𝑋 ) = ( ( 𝑦 + 1 ) · 𝑋 ) )
13 12 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( ( ( 𝑦 + 1 ) · 𝑋 ) + 𝑋 ) )
14 12 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑋 + ( 𝑥 · 𝑋 ) ) = ( 𝑋 + ( ( 𝑦 + 1 ) · 𝑋 ) ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑥 · 𝑋 ) ) ↔ ( ( ( 𝑦 + 1 ) · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 + 1 ) · 𝑋 ) ) ) )
16 oveq1 ⊢ ( 𝑥 = - 𝑦 → ( 𝑥 · 𝑋 ) = ( - 𝑦 · 𝑋 ) )
17 16 oveq1d ⊢ ( 𝑥 = - 𝑦 → ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( ( - 𝑦 · 𝑋 ) + 𝑋 ) )
18 16 oveq2d ⊢ ( 𝑥 = - 𝑦 → ( 𝑋 + ( 𝑥 · 𝑋 ) ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) )
19 17 18 eqeq12d ⊢ ( 𝑥 = - 𝑦 → ( ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑥 · 𝑋 ) ) ↔ ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ) )
20 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
21 20 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( ( 𝑁 · 𝑋 ) + 𝑋 ) )
22 20 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑋 + ( 𝑥 · 𝑋 ) ) = ( 𝑋 + ( 𝑁 · 𝑋 ) ) )
23 21 22 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝑥 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑥 · 𝑋 ) ) ↔ ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑁 · 𝑋 ) ) ) )
24 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
25 1 3 24 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝐺 ) + 𝑋 ) = 𝑋 )
26 1 24 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
27 26 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
28 27 oveq1d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 · 𝑋 ) + 𝑋 ) = ( ( 0g ‘ 𝐺 ) + 𝑋 ) )
29 27 oveq2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 0 · 𝑋 ) ) = ( 𝑋 + ( 0g ‘ 𝐺 ) ) )
30 1 3 24 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 0g ‘ 𝐺 ) ) = 𝑋 )
31 29 30 eqtrd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 + ( 0 · 𝑋 ) ) = 𝑋 )
32 25 28 31 3eqtr4d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( 0 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 0 · 𝑋 ) ) )
33 nn0z ⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ )
34 simp1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℤ ) → 𝐺 ∈ Grp )
35 simp2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℤ ) → 𝑋 ∈ 𝐵 )
36 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
37 36 3com23 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℤ ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
38 1 3 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑦 · 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 + ( 𝑦 · 𝑋 ) ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) )
39 34 35 37 35 38 syl13anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℤ ) → ( ( 𝑋 + ( 𝑦 · 𝑋 ) ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) )
40 33 39 syl3an3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑋 + ( 𝑦 · 𝑋 ) ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) )
41 40 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( 𝑋 + ( 𝑦 · 𝑋 ) ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) )
42 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
43 42 3ad2ant1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
44 simp3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
45 simp2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
46 1 2 3 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) + 𝑋 ) )
47 43 44 45 46 syl3anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) + 𝑋 ) )
48 47 eqeq1d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ↔ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) )
49 48 biimpar ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) )
50 49 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) + 𝑋 ) = ( ( 𝑋 + ( 𝑦 · 𝑋 ) ) + 𝑋 ) )
51 47 oveq2d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑋 + ( ( 𝑦 + 1 ) · 𝑋 ) ) = ( 𝑋 + ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) )
52 51 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( 𝑋 + ( ( 𝑦 + 1 ) · 𝑋 ) ) = ( 𝑋 + ( ( 𝑦 · 𝑋 ) + 𝑋 ) ) )
53 41 50 52 3eqtr4d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 + 1 ) · 𝑋 ) ) )
54 53 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 + 1 ) · 𝑋 ) ) ) )
55 54 3expia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ ℕ0 → ( ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) → ( ( ( 𝑦 + 1 ) · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( ( 𝑦 + 1 ) · 𝑋 ) ) ) ) )
56 nnz ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
57 1 2 3 mulgaddcomlem ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) ) → ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) )
58 57 3exp1 ⊢ ( 𝐺 ∈ Grp → ( 𝑦 ∈ ℤ → ( 𝑋 ∈ 𝐵 → ( ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) → ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ) ) ) )
59 58 com23 ⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐵 → ( 𝑦 ∈ ℤ → ( ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) → ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ) ) ) )
60 59 imp ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ ℤ → ( ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) → ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ) ) )
61 56 60 syl5 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ∈ ℕ → ( ( ( 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑦 · 𝑋 ) ) → ( ( - 𝑦 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( - 𝑦 · 𝑋 ) ) ) ) )
62 7 11 15 19 23 32 55 61 zindd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ∈ ℤ → ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑁 · 𝑋 ) ) ) )
63 62 ex ⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ ℤ → ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑁 · 𝑋 ) ) ) ) )
64 63 com23 ⊢ ( 𝐺 ∈ Grp → ( 𝑁 ∈ ℤ → ( 𝑋 ∈ 𝐵 → ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑁 · 𝑋 ) ) ) ) )
65 64 3imp ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 · 𝑋 ) + 𝑋 ) = ( 𝑋 + ( 𝑁 · 𝑋 ) ) )