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