This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )