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

Proof

Step	Hyp	Ref	Expression
1		mulgaddcom.b	$⊢ B = {Base}_{G}$
2		mulgaddcom.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgaddcom.p	$⊢ \underset{˙}{+} = +_{G}$
4		oveq1	$⊢ x = 0 \to x \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
5	4	oveq1d	$⊢ x = 0 \to (x \underset{˙}{\cdot} X) \underset{˙}{+} X = (0 \underset{˙}{\cdot} X) \underset{˙}{+} X$
6	4	oveq2d	$⊢ x = 0 \to X \underset{˙}{+} (x \underset{˙}{\cdot} X) = X \underset{˙}{+} (0 \underset{˙}{\cdot} X)$
7	5 6	eqeq12d	$⊢ x = 0 \to ((x \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (x \underset{˙}{\cdot} X) \leftrightarrow (0 \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (0 \underset{˙}{\cdot} X))$
8		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} X = y \underset{˙}{\cdot} X$
9	8	oveq1d	$⊢ x = y \to (x \underset{˙}{\cdot} X) \underset{˙}{+} X = (y \underset{˙}{\cdot} X) \underset{˙}{+} X$
10	8	oveq2d	$⊢ x = y \to X \underset{˙}{+} (x \underset{˙}{\cdot} X) = X \underset{˙}{+} (y \underset{˙}{\cdot} X)$
11	9 10	eqeq12d	$⊢ x = y \to ((x \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (x \underset{˙}{\cdot} X) \leftrightarrow (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X))$
12		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\cdot} X = (y + 1) \underset{˙}{\cdot} X$
13	12	oveq1d	$⊢ x = y + 1 \to (x \underset{˙}{\cdot} X) \underset{˙}{+} X = ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{+} X$
14	12	oveq2d	$⊢ x = y + 1 \to X \underset{˙}{+} (x \underset{˙}{\cdot} X) = X \underset{˙}{+} ((y + 1) \underset{˙}{\cdot} X)$
15	13 14	eqeq12d	$⊢ x = y + 1 \to ((x \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (x \underset{˙}{\cdot} X) \leftrightarrow ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((y + 1) \underset{˙}{\cdot} X))$
16		oveq1	$⊢ x = - y \to x \underset{˙}{\cdot} X = (- y) \underset{˙}{\cdot} X$
17	16	oveq1d	$⊢ x = - y \to (x \underset{˙}{\cdot} X) \underset{˙}{+} X = ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X$
18	16	oveq2d	$⊢ x = - y \to X \underset{˙}{+} (x \underset{˙}{\cdot} X) = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$
19	17 18	eqeq12d	$⊢ x = - y \to ((x \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (x \underset{˙}{\cdot} X) \leftrightarrow ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X))$
20		oveq1	$⊢ x = N \to x \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
21	20	oveq1d	$⊢ x = N \to (x \underset{˙}{\cdot} X) \underset{˙}{+} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$
22	20	oveq2d	$⊢ x = N \to X \underset{˙}{+} (x \underset{˙}{\cdot} X) = X \underset{˙}{+} (N \underset{˙}{\cdot} X)$
23	21 22	eqeq12d	$⊢ x = N \to ((x \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (x \underset{˙}{\cdot} X) \leftrightarrow (N \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (N \underset{˙}{\cdot} X))$
24		eqid	$⊢ 0_{G} = 0_{G}$
25	1 3 24	grplid	$⊢ (G \in Grp \land X \in B) \to 0_{G} \underset{˙}{+} X = X$
26	1 24 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	oveq1d	$⊢ (G \in Grp \land X \in B) \to (0 \underset{˙}{\cdot} X) \underset{˙}{+} X = 0_{G} \underset{˙}{+} X$
29	27	oveq2d	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} (0 \underset{˙}{\cdot} X) = X \underset{˙}{+} 0_{G}$
30	1 3 24	grprid	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} 0_{G} = X$
31	29 30	eqtrd	$⊢ (G \in Grp \land X \in B) \to X \underset{˙}{+} (0 \underset{˙}{\cdot} X) = X$
32	25 28 31	3eqtr4d	$⊢ (G \in Grp \land X \in B) \to (0 \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (0 \underset{˙}{\cdot} X)$
33		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
34		simp1	$⊢ (G \in Grp \land X \in B \land y \in ℤ) \to G \in Grp$
35		simp2	$⊢ (G \in Grp \land X \in B \land y \in ℤ) \to X \in B$
36	1 2	mulgcl	$⊢ (G \in Grp \land y \in ℤ \land X \in B) \to y \underset{˙}{\cdot} X \in B$
37	36	3com23	$⊢ (G \in Grp \land X \in B \land y \in ℤ) \to y \underset{˙}{\cdot} X \in B$
38	1 3	grpass	$⊢ (G \in Grp \land (X \in B \land y \underset{˙}{\cdot} X \in B \land X \in B)) \to (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \underset{˙}{+} X = X \underset{˙}{+} ((y \underset{˙}{\cdot} X) \underset{˙}{+} X)$
39	34 35 37 35 38	syl13anc	$⊢ (G \in Grp \land X \in B \land y \in ℤ) \to (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \underset{˙}{+} X = X \underset{˙}{+} ((y \underset{˙}{\cdot} X) \underset{˙}{+} X)$
40	33 39	syl3an3	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \underset{˙}{+} X = X \underset{˙}{+} ((y \underset{˙}{\cdot} X) \underset{˙}{+} X)$
41	40	adantr	$⊢ ((G \in Grp \land X \in B \land y \in ℕ_{0}) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \underset{˙}{+} X = X \underset{˙}{+} ((y \underset{˙}{\cdot} X) \underset{˙}{+} X)$
42		grpmnd	$⊢ G \in Grp \to G \in Mnd$
43	42	3ad2ant1	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to G \in Mnd$
44		simp3	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to y \in ℕ_{0}$
45		simp2	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to X \in B$
46	1 2 3	mulgnn0p1	$⊢ (G \in Mnd \land y \in ℕ_{0} \land X \in B) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) \underset{˙}{+} X$
47	43 44 45 46	syl3anc	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) \underset{˙}{+} X$
48	47	eqeq1d	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to ((y + 1) \underset{˙}{\cdot} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \leftrightarrow (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X))$
49	48	biimpar	$⊢ ((G \in Grp \land X \in B \land y \in ℕ_{0}) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to (y + 1) \underset{˙}{\cdot} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)$
50	49	oveq1d	$⊢ ((G \in Grp \land X \in B \land y \in ℕ_{0}) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{+} X = (X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \underset{˙}{+} X$
51	47	oveq2d	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to X \underset{˙}{+} ((y + 1) \underset{˙}{\cdot} X) = X \underset{˙}{+} ((y \underset{˙}{\cdot} X) \underset{˙}{+} X)$
52	51	adantr	$⊢ ((G \in Grp \land X \in B \land y \in ℕ_{0}) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to X \underset{˙}{+} ((y + 1) \underset{˙}{\cdot} X) = X \underset{˙}{+} ((y \underset{˙}{\cdot} X) \underset{˙}{+} X)$
53	41 50 52	3eqtr4d	$⊢ ((G \in Grp \land X \in B \land y \in ℕ_{0}) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((y + 1) \underset{˙}{\cdot} X)$
54	53	ex	$⊢ (G \in Grp \land X \in B \land y \in ℕ_{0}) \to ((y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((y + 1) \underset{˙}{\cdot} X))$
55	54	3expia	$⊢ (G \in Grp \land X \in B) \to (y \in ℕ_{0} \to ((y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \to ((y + 1) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((y + 1) \underset{˙}{\cdot} X)))$
56		nnz	$⊢ y \in ℕ \to y \in ℤ$
57	1 2 3	mulgaddcomlem	$⊢ ((G \in Grp \land y \in ℤ \land X \in B) \land (y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X)) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)$
58	57	3exp1	$⊢ G \in Grp \to (y \in ℤ \to (X \in B \to ((y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X))))$
59	58	com23	$⊢ G \in Grp \to (X \in B \to (y \in ℤ \to ((y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X))))$
60	59	imp	$⊢ (G \in Grp \land X \in B) \to (y \in ℤ \to ((y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)))$
61	56 60	syl5	$⊢ (G \in Grp \land X \in B) \to (y \in ℕ \to ((y \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (y \underset{˙}{\cdot} X) \to ((- y) \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} ((- y) \underset{˙}{\cdot} X)))$
62	7 11 15 19 23 32 55 61	zindd	$⊢ (G \in Grp \land X \in B) \to (N \in ℤ \to (N \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (N \underset{˙}{\cdot} X))$
63	62	ex	$⊢ G \in Grp \to (X \in B \to (N \in ℤ \to (N \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (N \underset{˙}{\cdot} X)))$
64	63	com23	$⊢ G \in Grp \to (N \in ℤ \to (X \in B \to (N \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (N \underset{˙}{\cdot} X)))$
65	64	3imp	$⊢ (G \in Grp \land N \in ℤ \land X \in B) \to (N \underset{˙}{\cdot} X) \underset{˙}{+} X = X \underset{˙}{+} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgaddcom

Proof