Metamath Proof Explorer


Theorem mulginvcom

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

Ref Expression
Hypotheses mulginvcom.b 𝐵 = ( Base ‘ 𝐺 )
mulginvcom.t · = ( .g𝐺 )
mulginvcom.i 𝐼 = ( invg𝐺 )
Assertion mulginvcom ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝑁 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulginvcom.b 𝐵 = ( Base ‘ 𝐺 )
2 mulginvcom.t · = ( .g𝐺 )
3 mulginvcom.i 𝐼 = ( invg𝐺 )
4 oveq1 ( 𝑥 = 0 → ( 𝑥 · ( 𝐼𝑋 ) ) = ( 0 · ( 𝐼𝑋 ) ) )
5 fvoveq1 ( 𝑥 = 0 → ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) = ( 𝐼 ‘ ( 0 · 𝑋 ) ) )
6 4 5 eqeq12d ( 𝑥 = 0 → ( ( 𝑥 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) ↔ ( 0 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 0 · 𝑋 ) ) ) )
7 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 · ( 𝐼𝑋 ) ) = ( 𝑦 · ( 𝐼𝑋 ) ) )
8 fvoveq1 ( 𝑥 = 𝑦 → ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) )
9 7 8 eqeq12d ( 𝑥 = 𝑦 → ( ( 𝑥 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) ↔ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) )
10 oveq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · ( 𝐼𝑋 ) ) = ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) )
11 fvoveq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) = ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) )
12 10 11 eqeq12d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) ↔ ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) ) )
13 oveq1 ( 𝑥 = - 𝑦 → ( 𝑥 · ( 𝐼𝑋 ) ) = ( - 𝑦 · ( 𝐼𝑋 ) ) )
14 fvoveq1 ( 𝑥 = - 𝑦 → ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) = ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) )
15 13 14 eqeq12d ( 𝑥 = - 𝑦 → ( ( 𝑥 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) ↔ ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) ) )
16 oveq1 ( 𝑥 = 𝑁 → ( 𝑥 · ( 𝐼𝑋 ) ) = ( 𝑁 · ( 𝐼𝑋 ) ) )
17 fvoveq1 ( 𝑥 = 𝑁 → ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )
18 16 17 eqeq12d ( 𝑥 = 𝑁 → ( ( 𝑥 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑥 · 𝑋 ) ) ↔ ( 𝑁 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) ) )
19 eqid ( 0g𝐺 ) = ( 0g𝐺 )
20 19 3 grpinvid ( 𝐺 ∈ Grp → ( 𝐼 ‘ ( 0g𝐺 ) ) = ( 0g𝐺 ) )
21 20 eqcomd ( 𝐺 ∈ Grp → ( 0g𝐺 ) = ( 𝐼 ‘ ( 0g𝐺 ) ) )
22 21 adantr ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 0g𝐺 ) = ( 𝐼 ‘ ( 0g𝐺 ) ) )
23 1 3 grpinvcl ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝐼𝑋 ) ∈ 𝐵 )
24 1 19 2 mulg0 ( ( 𝐼𝑋 ) ∈ 𝐵 → ( 0 · ( 𝐼𝑋 ) ) = ( 0g𝐺 ) )
25 23 24 syl ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 0 · ( 𝐼𝑋 ) ) = ( 0g𝐺 ) )
26 1 19 2 mulg0 ( 𝑋𝐵 → ( 0 · 𝑋 ) = ( 0g𝐺 ) )
27 26 adantl ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 0 · 𝑋 ) = ( 0g𝐺 ) )
28 27 fveq2d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝐼 ‘ ( 0 · 𝑋 ) ) = ( 𝐼 ‘ ( 0g𝐺 ) ) )
29 22 25 28 3eqtr4d ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 0 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 0 · 𝑋 ) ) )
30 oveq2 ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝑦 · ( 𝐼𝑋 ) ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) )
31 30 adantl ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝑦 · ( 𝐼𝑋 ) ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) )
32 grpmnd ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
33 32 3ad2ant1 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → 𝐺 ∈ Mnd )
34 simp2 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → 𝑦 ∈ ℕ0 )
35 23 3adant2 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( 𝐼𝑋 ) ∈ 𝐵 )
36 eqid ( +g𝐺 ) = ( +g𝐺 )
37 1 2 36 mulgnn0p1 ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ ( 𝐼𝑋 ) ∈ 𝐵 ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( ( 𝑦 · ( 𝐼𝑋 ) ) ( +g𝐺 ) ( 𝐼𝑋 ) ) )
38 33 34 35 37 syl3anc ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( ( 𝑦 · ( 𝐼𝑋 ) ) ( +g𝐺 ) ( 𝐼𝑋 ) ) )
39 simp1 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → 𝐺 ∈ Grp )
40 nn0z ( 𝑦 ∈ ℕ0𝑦 ∈ ℤ )
41 40 3ad2ant2 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → 𝑦 ∈ ℤ )
42 1 2 36 mulgaddcom ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ ( 𝐼𝑋 ) ∈ 𝐵 ) → ( ( 𝑦 · ( 𝐼𝑋 ) ) ( +g𝐺 ) ( 𝐼𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝑦 · ( 𝐼𝑋 ) ) ) )
43 39 41 35 42 syl3anc ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( ( 𝑦 · ( 𝐼𝑋 ) ) ( +g𝐺 ) ( 𝐼𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝑦 · ( 𝐼𝑋 ) ) ) )
44 38 43 eqtrd ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝑦 · ( 𝐼𝑋 ) ) ) )
45 44 adantr ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝑦 · ( 𝐼𝑋 ) ) ) )
46 1 2 36 mulgnn0p1 ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) ( +g𝐺 ) 𝑋 ) )
47 32 46 syl3an1 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( ( 𝑦 + 1 ) · 𝑋 ) = ( ( 𝑦 · 𝑋 ) ( +g𝐺 ) 𝑋 ) )
48 47 fveq2d ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) = ( 𝐼 ‘ ( ( 𝑦 · 𝑋 ) ( +g𝐺 ) 𝑋 ) ) )
49 1 2 mulgcl ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
50 40 49 syl3an2 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( 𝑦 · 𝑋 ) ∈ 𝐵 )
51 1 36 3 grpinvadd ( ( 𝐺 ∈ Grp ∧ ( 𝑦 · 𝑋 ) ∈ 𝐵𝑋𝐵 ) → ( 𝐼 ‘ ( ( 𝑦 · 𝑋 ) ( +g𝐺 ) 𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) )
52 50 51 syld3an2 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( 𝐼 ‘ ( ( 𝑦 · 𝑋 ) ( +g𝐺 ) 𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) )
53 48 52 eqtrd ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) → ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) )
54 53 adantr ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) = ( ( 𝐼𝑋 ) ( +g𝐺 ) ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) )
55 31 45 54 3eqtr4d ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) )
56 55 3exp1 ( 𝐺 ∈ Grp → ( 𝑦 ∈ ℕ0 → ( 𝑋𝐵 → ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) ) ) ) )
57 56 com23 ( 𝐺 ∈ Grp → ( 𝑋𝐵 → ( 𝑦 ∈ ℕ0 → ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) ) ) ) )
58 57 imp ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑦 ∈ ℕ0 → ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( ( 𝑦 + 1 ) · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( ( 𝑦 + 1 ) · 𝑋 ) ) ) ) )
59 nnz ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
60 23 3adant2 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝐼𝑋 ) ∈ 𝐵 )
61 1 2 3 mulgneg ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ ( 𝐼𝑋 ) ∈ 𝐵 ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · ( 𝐼𝑋 ) ) ) )
62 60 61 syld3an3 ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · ( 𝐼𝑋 ) ) ) )
63 62 adantr ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · ( 𝐼𝑋 ) ) ) )
64 1 2 3 mulgneg ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑦 · 𝑋 ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) )
65 64 adantr ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( - 𝑦 · 𝑋 ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) )
66 simpr ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) )
67 65 66 eqtr4d ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( - 𝑦 · 𝑋 ) = ( 𝑦 · ( 𝐼𝑋 ) ) )
68 67 fveq2d ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · ( 𝐼𝑋 ) ) ) )
69 63 68 eqtr4d ( ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵 ) ∧ ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) )
70 69 3exp1 ( 𝐺 ∈ Grp → ( 𝑦 ∈ ℤ → ( 𝑋𝐵 → ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) ) ) ) )
71 70 com23 ( 𝐺 ∈ Grp → ( 𝑋𝐵 → ( 𝑦 ∈ ℤ → ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) ) ) ) )
72 71 imp ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑦 ∈ ℤ → ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) ) ) )
73 59 72 syl5 ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑦 ∈ ℕ → ( ( 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑦 · 𝑋 ) ) → ( - 𝑦 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( - 𝑦 · 𝑋 ) ) ) ) )
74 6 9 12 15 18 29 58 73 zindd ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑁 ∈ ℤ → ( 𝑁 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) ) )
75 74 ex ( 𝐺 ∈ Grp → ( 𝑋𝐵 → ( 𝑁 ∈ ℤ → ( 𝑁 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) ) ) )
76 75 com23 ( 𝐺 ∈ Grp → ( 𝑁 ∈ ℤ → ( 𝑋𝐵 → ( 𝑁 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) ) ) )
77 76 3imp ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( 𝑁 · ( 𝐼𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )