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	$⊢ B = {Base}_{G}$
	mulginvcom.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulginvcom.i	$⊢ I = {inv}_{g} (G)$
Assertion	mulginvcom	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} I (X) = I (N \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		mulginvcom.b	$⊢ B = {Base}_{G}$
2		mulginvcom.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulginvcom.i	$⊢ I = {inv}_{g} (G)$
4		oveq1	$⊢ x = 0 \to x \underset{˙}{\cdot} I (X) = 0 \underset{˙}{\cdot} I (X)$
5		fvoveq1	$⊢ x = 0 \to I (x \underset{˙}{\cdot} X) = I (0 \underset{˙}{\cdot} X)$
6	4 5	eqeq12d	$⊢ x = 0 \to (x \underset{˙}{\cdot} I (X) = I (x \underset{˙}{\cdot} X) \leftrightarrow 0 \underset{˙}{\cdot} I (X) = I (0 \underset{˙}{\cdot} X))$
7		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} I (X) = y \underset{˙}{\cdot} I (X)$
8		fvoveq1	$⊢ x = y \to I (x \underset{˙}{\cdot} X) = I (y \underset{˙}{\cdot} X)$
9	7 8	eqeq12d	$⊢ x = y \to (x \underset{˙}{\cdot} I (X) = I (x \underset{˙}{\cdot} X) \leftrightarrow y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X))$
10		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\cdot} I (X) = (y + 1) \underset{˙}{\cdot} I (X)$
11		fvoveq1	$⊢ x = y + 1 \to I (x \underset{˙}{\cdot} X) = I ((y + 1) \underset{˙}{\cdot} X)$
12	10 11	eqeq12d	$⊢ x = y + 1 \to (x \underset{˙}{\cdot} I (X) = I (x \underset{˙}{\cdot} X) \leftrightarrow (y + 1) \underset{˙}{\cdot} I (X) = I ((y + 1) \underset{˙}{\cdot} X))$
13		oveq1	$⊢ x = - y \to x \underset{˙}{\cdot} I (X) = (- y) \underset{˙}{\cdot} I (X)$
14		fvoveq1	$⊢ x = - y \to I (x \underset{˙}{\cdot} X) = I ((- y) \underset{˙}{\cdot} X)$
15	13 14	eqeq12d	$⊢ x = - y \to (x \underset{˙}{\cdot} I (X) = I (x \underset{˙}{\cdot} X) \leftrightarrow (- y) \underset{˙}{\cdot} I (X) = I ((- y) \underset{˙}{\cdot} X))$
16		oveq1	$⊢ x = N \to x \underset{˙}{\cdot} I (X) = N \underset{˙}{\cdot} I (X)$
17		fvoveq1	$⊢ x = N \to I (x \underset{˙}{\cdot} X) = I (N \underset{˙}{\cdot} X)$
18	16 17	eqeq12d	$⊢ x = N \to (x \underset{˙}{\cdot} I (X) = I (x \underset{˙}{\cdot} X) \leftrightarrow N \underset{˙}{\cdot} I (X) = I (N \underset{˙}{\cdot} X))$
19		eqid	$⊢ 0_{G} = 0_{G}$
20	19 3	grpinvid	$⊢ G \in Grp \to I (0_{G}) = 0_{G}$
21	20	eqcomd	$⊢ G \in Grp \to 0_{G} = I (0_{G})$
22	21	adantr	$⊢ (G \in Grp \land X \in B) \to 0_{G} = I (0_{G})$
23	1 3	grpinvcl	$⊢ (G \in Grp \land X \in B) \to I (X) \in B$
24	1 19 2	mulg0	$⊢ I (X) \in B \to 0 \underset{˙}{\cdot} I (X) = 0_{G}$
25	23 24	syl	$⊢ (G \in Grp \land X \in B) \to 0 \underset{˙}{\cdot} I (X) = 0_{G}$
26	1 19 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
27	26	adantl	$⊢ (G \in Grp \land X \in B) \to 0 \underset{˙}{\cdot} X = 0_{G}$
28	27	fveq2d	$⊢ (G \in Grp \land X \in B) \to I (0 \underset{˙}{\cdot} X) = I (0_{G})$
29	22 25 28	3eqtr4d	$⊢ (G \in Grp \land X \in B) \to 0 \underset{˙}{\cdot} I (X) = I (0 \underset{˙}{\cdot} X)$
30		oveq2	$⊢ y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to I (X) +_{G} (y \underset{˙}{\cdot} I (X)) = I (X) +_{G} I (y \underset{˙}{\cdot} X)$
31	30	adantl	$⊢ ((G \in Grp \land y \in ℕ_{0} \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to I (X) +_{G} (y \underset{˙}{\cdot} I (X)) = I (X) +_{G} I (y \underset{˙}{\cdot} X)$
32		grpmnd	$⊢ G \in Grp \to G \in Mnd$
33	32	3ad2ant1	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to G \in Mnd$
34		simp2	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to y \in ℕ_{0}$
35	23	3adant2	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to I (X) \in B$
36		eqid	$⊢ +_{G} = +_{G}$
37	1 2 36	mulgnn0p1	$⊢ (G \in Mnd \land y \in ℕ_{0} \land I (X) \in B) \to (y + 1) \underset{˙}{\cdot} I (X) = (y \underset{˙}{\cdot} I (X)) +_{G} I (X)$
38	33 34 35 37	syl3anc	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to (y + 1) \underset{˙}{\cdot} I (X) = (y \underset{˙}{\cdot} I (X)) +_{G} I (X)$
39		simp1	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to G \in Grp$
40		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
41	40	3ad2ant2	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to y \in ℤ$
42	1 2 36	mulgaddcom	$⊢ (G \in Grp \land y \in ℤ \land I (X) \in B) \to (y \underset{˙}{\cdot} I (X)) +_{G} I (X) = I (X) +_{G} (y \underset{˙}{\cdot} I (X))$
43	39 41 35 42	syl3anc	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to (y \underset{˙}{\cdot} I (X)) +_{G} I (X) = I (X) +_{G} (y \underset{˙}{\cdot} I (X))$
44	38 43	eqtrd	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to (y + 1) \underset{˙}{\cdot} I (X) = I (X) +_{G} (y \underset{˙}{\cdot} I (X))$
45	44	adantr	$⊢ ((G \in Grp \land y \in ℕ_{0} \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to (y + 1) \underset{˙}{\cdot} I (X) = I (X) +_{G} (y \underset{˙}{\cdot} I (X))$
46	1 2 36	mulgnn0p1	$⊢ (G \in Mnd \land y \in ℕ_{0} \land X \in B) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{G} X$
47	32 46	syl3an1	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{G} X$
48	47	fveq2d	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to I ((y + 1) \underset{˙}{\cdot} X) = I ((y \underset{˙}{\cdot} X) +_{G} X)$
49	1 2	mulgcl	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to y \underset{˙}{\cdot} X \in B$
50	40 49	syl3an2	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to y \underset{˙}{\cdot} X \in B$
51	1 36 3	grpinvadd	$⊢ (G \in Grp \land y \underset{˙}{\cdot} X \in B \land X \in B) \to I ((y \underset{˙}{\cdot} X) +_{G} X) = I (X) +_{G} I (y \underset{˙}{\cdot} X)$
52	50 51	syld3an2	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to I ((y \underset{˙}{\cdot} X) +_{G} X) = I (X) +_{G} I (y \underset{˙}{\cdot} X)$
53	48 52	eqtrd	$⊢ (G \in Grp \land y \in ℕ_{0} \land X \in B) \to I ((y + 1) \underset{˙}{\cdot} X) = I (X) +_{G} I (y \underset{˙}{\cdot} X)$
54	53	adantr	$⊢ ((G \in Grp \land y \in ℕ_{0} \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to I ((y + 1) \underset{˙}{\cdot} X) = I (X) +_{G} I (y \underset{˙}{\cdot} X)$
55	31 45 54	3eqtr4d	$⊢ ((G \in Grp \land y \in ℕ_{0} \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to (y + 1) \underset{˙}{\cdot} I (X) = I ((y + 1) \underset{˙}{\cdot} X)$
56	55	3exp1	$⊢ G \in Grp \to (y \in ℕ_{0} \to (X \in B \to (y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to (y + 1) \underset{˙}{\cdot} I (X) = I ((y + 1) \underset{˙}{\cdot} X))))$
57	56	com23	$⊢ G \in Grp \to (X \in B \to (y \in ℕ_{0} \to (y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to (y + 1) \underset{˙}{\cdot} I (X) = I ((y + 1) \underset{˙}{\cdot} X))))$
58	57	imp	$⊢ (G \in Grp \land X \in B) \to (y \in ℕ_{0} \to (y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to (y + 1) \underset{˙}{\cdot} I (X) = I ((y + 1) \underset{˙}{\cdot} X)))$
59		nnz	$⊢ y \in ℕ \to y \in ℤ$
60	23	3adant2	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to I (X) \in B$
61	1 2 3	mulgneg	$⊢ (G \in Grp \land y \in ℤ \land I (X) \in B) \to (- y) \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} I (X))$
62	60 61	syld3an3	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to (- y) \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} I (X))$
63	62	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to (- y) \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} I (X))$
64	1 2 3	mulgneg	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to (- y) \underset{˙}{\cdot} X = I (y \underset{˙}{\cdot} X)$
65	64	adantr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to (- y) \underset{˙}{\cdot} X = I (y \underset{˙}{\cdot} X)$
66		simpr	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)$
67	65 66	eqtr4d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to (- y) \underset{˙}{\cdot} X = y \underset{˙}{\cdot} I (X)$
68	67	fveq2d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to I ((- y) \underset{˙}{\cdot} X) = I (y \underset{˙}{\cdot} I (X))$
69	63 68	eqtr4d	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X)) \to (- y) \underset{˙}{\cdot} I (X) = I ((- y) \underset{˙}{\cdot} X)$
70	69	3exp1	$⊢ G \in Grp \to (y \in ℤ \to (X \in B \to (y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to (- y) \underset{˙}{\cdot} I (X) = I ((- y) \underset{˙}{\cdot} X))))$
71	70	com23	$⊢ G \in Grp \to (X \in B \to (y \in ℤ \to (y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to (- y) \underset{˙}{\cdot} I (X) = I ((- y) \underset{˙}{\cdot} X))))$
72	71	imp	$⊢ (G \in Grp \land X \in B) \to (y \in ℤ \to (y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to (- y) \underset{˙}{\cdot} I (X) = I ((- y) \underset{˙}{\cdot} X)))$
73	59 72	syl5	$⊢ (G \in Grp \land X \in B) \to (y \in ℕ \to (y \underset{˙}{\cdot} I (X) = I (y \underset{˙}{\cdot} X) \to (- y) \underset{˙}{\cdot} I (X) = I ((- y) \underset{˙}{\cdot} X)))$
74	6 9 12 15 18 29 58 73	zindd	$⊢ (G \in Grp \land X \in B) \to (N \in ℤ \to N \underset{˙}{\cdot} I (X) = I (N \underset{˙}{\cdot} X))$
75	74	ex	$⊢ G \in Grp \to (X \in B \to (N \in ℤ \to N \underset{˙}{\cdot} I (X) = I (N \underset{˙}{\cdot} X)))$
76	75	com23	$⊢ G \in Grp \to (N \in ℤ \to (X \in B \to N \underset{˙}{\cdot} I (X) = I (N \underset{˙}{\cdot} X)))$
77	76	3imp	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to N \underset{˙}{\cdot} I (X) = I (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulginvcom

Proof