srgpcomp

Description: If two elements of a semiring commute, they also commute if one of the elements is raised to a higher power. (Contributed by AV, 23-Aug-2019)

	Ref	Expression
Hypotheses	srgpcomp.s	$⊢ S = {Base}_{R}$
	srgpcomp.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
	srgpcomp.g	$⊢ G = {mulGrp}_{R}$
	srgpcomp.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	srgpcomp.r	$⊢ φ \to R \in SRing$
	srgpcomp.a	$⊢ φ \to A \in S$
	srgpcomp.b	$⊢ φ \to B \in S$
	srgpcomp.k	$⊢ φ \to K \in ℕ_{0}$
	srgpcomp.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
Assertion	srgpcomp	$⊢ φ \to (K \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (K \underset{˙}{\times} B)$

Proof

Step	Hyp	Ref	Expression
1		srgpcomp.s	$⊢ S = {Base}_{R}$
2		srgpcomp.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
3		srgpcomp.g	$⊢ G = {mulGrp}_{R}$
4		srgpcomp.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
5		srgpcomp.r	$⊢ φ \to R \in SRing$
6		srgpcomp.a	$⊢ φ \to A \in S$
7		srgpcomp.b	$⊢ φ \to B \in S$
8		srgpcomp.k	$⊢ φ \to K \in ℕ_{0}$
9		srgpcomp.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
10		oveq1	$⊢ x = 0 \to x \underset{˙}{\times} B = 0 \underset{˙}{\times} B$
11	10	oveq1d	$⊢ x = 0 \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = (0 \underset{˙}{\times} B) \underset{˙}{\times} A$
12	10	oveq2d	$⊢ x = 0 \to A \underset{˙}{\times} (x \underset{˙}{\times} B) = A \underset{˙}{\times} (0 \underset{˙}{\times} B)$
13	11 12	eqeq12d	$⊢ x = 0 \to ((x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B) \leftrightarrow (0 \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (0 \underset{˙}{\times} B))$
14	13	imbi2d	$⊢ x = 0 \to ((φ \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B)) \leftrightarrow (φ \to (0 \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (0 \underset{˙}{\times} B)))$
15		oveq1	$⊢ x = y \to x \underset{˙}{\times} B = y \underset{˙}{\times} B$
16	15	oveq1d	$⊢ x = y \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = (y \underset{˙}{\times} B) \underset{˙}{\times} A$
17	15	oveq2d	$⊢ x = y \to A \underset{˙}{\times} (x \underset{˙}{\times} B) = A \underset{˙}{\times} (y \underset{˙}{\times} B)$
18	16 17	eqeq12d	$⊢ x = y \to ((x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B) \leftrightarrow (y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B))$
19	18	imbi2d	$⊢ x = y \to ((φ \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B)) \leftrightarrow (φ \to (y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B)))$
20		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\times} B = (y + 1) \underset{˙}{\times} B$
21	20	oveq1d	$⊢ x = y + 1 \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A$
22	20	oveq2d	$⊢ x = y + 1 \to A \underset{˙}{\times} (x \underset{˙}{\times} B) = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)$
23	21 22	eqeq12d	$⊢ x = y + 1 \to ((x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B) \leftrightarrow ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B))$
24	23	imbi2d	$⊢ x = y + 1 \to ((φ \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B)) \leftrightarrow (φ \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)))$
25		oveq1	$⊢ x = K \to x \underset{˙}{\times} B = K \underset{˙}{\times} B$
26	25	oveq1d	$⊢ x = K \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = (K \underset{˙}{\times} B) \underset{˙}{\times} A$
27	25	oveq2d	$⊢ x = K \to A \underset{˙}{\times} (x \underset{˙}{\times} B) = A \underset{˙}{\times} (K \underset{˙}{\times} B)$
28	26 27	eqeq12d	$⊢ x = K \to ((x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B) \leftrightarrow (K \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (K \underset{˙}{\times} B))$
29	28	imbi2d	$⊢ x = K \to ((φ \to (x \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (x \underset{˙}{\times} B)) \leftrightarrow (φ \to (K \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (K \underset{˙}{\times} B)))$
30	3 1	mgpbas	$⊢ S = {Base}_{G}$
31		eqid	$⊢ 1_{R} = 1_{R}$
32	3 31	ringidval	$⊢ 1_{R} = 0_{G}$
33	30 32 4	mulg0	$⊢ B \in S \to 0 \underset{˙}{\times} B = 1_{R}$
34	7 33	syl	$⊢ φ \to 0 \underset{˙}{\times} B = 1_{R}$
35	34	oveq1d	$⊢ φ \to (0 \underset{˙}{\times} B) \underset{˙}{\times} A = 1_{R} \underset{˙}{\times} A$
36	1 2 31	srgridm	$⊢ (R \in SRing \land A \in S) \to A \underset{˙}{\times} 1_{R} = A$
37	5 6 36	syl2anc	$⊢ φ \to A \underset{˙}{\times} 1_{R} = A$
38	34	oveq2d	$⊢ φ \to A \underset{˙}{\times} (0 \underset{˙}{\times} B) = A \underset{˙}{\times} 1_{R}$
39	1 2 31	srglidm	$⊢ (R \in SRing \land A \in S) \to 1_{R} \underset{˙}{\times} A = A$
40	5 6 39	syl2anc	$⊢ φ \to 1_{R} \underset{˙}{\times} A = A$
41	37 38 40	3eqtr4rd	$⊢ φ \to 1_{R} \underset{˙}{\times} A = A \underset{˙}{\times} (0 \underset{˙}{\times} B)$
42	35 41	eqtrd	$⊢ φ \to (0 \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (0 \underset{˙}{\times} B)$
43	3	srgmgp	$⊢ R \in SRing \to G \in Mnd$
44	5 43	syl	$⊢ φ \to G \in Mnd$
45	44	adantr	$⊢ (φ \land y \in ℕ_{0}) \to G \in Mnd$
46		simpr	$⊢ (φ \land y \in ℕ_{0}) \to y \in ℕ_{0}$
47	7	adantr	$⊢ (φ \land y \in ℕ_{0}) \to B \in S$
48	3 2	mgpplusg	$⊢ \underset{˙}{\times} = +_{G}$
49	30 4 48	mulgnn0p1	$⊢ (G \in Mnd \land y \in ℕ_{0} \land B \in S) \to (y + 1) \underset{˙}{\times} B = (y \underset{˙}{\times} B) \underset{˙}{\times} B$
50	45 46 47 49	syl3anc	$⊢ (φ \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{\times} B = (y \underset{˙}{\times} B) \underset{˙}{\times} B$
51	50	oveq1d	$⊢ (φ \land y \in ℕ_{0}) \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = ((y \underset{˙}{\times} B) \underset{˙}{\times} B) \underset{˙}{\times} A$
52	9	eqcomd	$⊢ φ \to B \underset{˙}{\times} A = A \underset{˙}{\times} B$
53	52	adantr	$⊢ (φ \land y \in ℕ_{0}) \to B \underset{˙}{\times} A = A \underset{˙}{\times} B$
54	53	oveq2d	$⊢ (φ \land y \in ℕ_{0}) \to (y \underset{˙}{\times} B) \underset{˙}{\times} (B \underset{˙}{\times} A) = (y \underset{˙}{\times} B) \underset{˙}{\times} (A \underset{˙}{\times} B)$
55	5	adantr	$⊢ (φ \land y \in ℕ_{0}) \to R \in SRing$
56	30 4 45 46 47	mulgnn0cld	$⊢ (φ \land y \in ℕ_{0}) \to y \underset{˙}{\times} B \in S$
57	6	adantr	$⊢ (φ \land y \in ℕ_{0}) \to A \in S$
58	1 2	srgass	$⊢ (R \in SRing \land (y \underset{˙}{\times} B \in S \land B \in S \land A \in S)) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} B) \underset{˙}{\times} A = (y \underset{˙}{\times} B) \underset{˙}{\times} (B \underset{˙}{\times} A)$
59	55 56 47 57 58	syl13anc	$⊢ (φ \land y \in ℕ_{0}) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} B) \underset{˙}{\times} A = (y \underset{˙}{\times} B) \underset{˙}{\times} (B \underset{˙}{\times} A)$
60	1 2	srgass	$⊢ (R \in SRing \land (y \underset{˙}{\times} B \in S \land A \in S \land B \in S)) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} A) \underset{˙}{\times} B = (y \underset{˙}{\times} B) \underset{˙}{\times} (A \underset{˙}{\times} B)$
61	55 56 57 47 60	syl13anc	$⊢ (φ \land y \in ℕ_{0}) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} A) \underset{˙}{\times} B = (y \underset{˙}{\times} B) \underset{˙}{\times} (A \underset{˙}{\times} B)$
62	54 59 61	3eqtr4d	$⊢ (φ \land y \in ℕ_{0}) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} B) \underset{˙}{\times} A = ((y \underset{˙}{\times} B) \underset{˙}{\times} A) \underset{˙}{\times} B$
63	51 62	eqtrd	$⊢ (φ \land y \in ℕ_{0}) \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = ((y \underset{˙}{\times} B) \underset{˙}{\times} A) \underset{˙}{\times} B$
64	63	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land (y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B)) \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = ((y \underset{˙}{\times} B) \underset{˙}{\times} A) \underset{˙}{\times} B$
65		oveq1	$⊢ (y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} A) \underset{˙}{\times} B = (A \underset{˙}{\times} (y \underset{˙}{\times} B)) \underset{˙}{\times} B$
66	1 2	srgass	$⊢ (R \in SRing \land (A \in S \land y \underset{˙}{\times} B \in S \land B \in S)) \to (A \underset{˙}{\times} (y \underset{˙}{\times} B)) \underset{˙}{\times} B = A \underset{˙}{\times} ((y \underset{˙}{\times} B) \underset{˙}{\times} B)$
67	55 57 56 47 66	syl13anc	$⊢ (φ \land y \in ℕ_{0}) \to (A \underset{˙}{\times} (y \underset{˙}{\times} B)) \underset{˙}{\times} B = A \underset{˙}{\times} ((y \underset{˙}{\times} B) \underset{˙}{\times} B)$
68	50	eqcomd	$⊢ (φ \land y \in ℕ_{0}) \to (y \underset{˙}{\times} B) \underset{˙}{\times} B = (y + 1) \underset{˙}{\times} B$
69	68	oveq2d	$⊢ (φ \land y \in ℕ_{0}) \to A \underset{˙}{\times} ((y \underset{˙}{\times} B) \underset{˙}{\times} B) = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)$
70	67 69	eqtrd	$⊢ (φ \land y \in ℕ_{0}) \to (A \underset{˙}{\times} (y \underset{˙}{\times} B)) \underset{˙}{\times} B = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)$
71	65 70	sylan9eqr	$⊢ ((φ \land y \in ℕ_{0}) \land (y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B)) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} A) \underset{˙}{\times} B = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)$
72	64 71	eqtrd	$⊢ ((φ \land y \in ℕ_{0}) \land (y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B)) \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)$
73	72	ex	$⊢ (φ \land y \in ℕ_{0}) \to ((y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B) \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B))$
74	73	expcom	$⊢ y \in ℕ_{0} \to (φ \to ((y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B) \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)))$
75	74	a2d	$⊢ y \in ℕ_{0} \to ((φ \to (y \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (y \underset{˙}{\times} B)) \to (φ \to ((y + 1) \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} ((y + 1) \underset{˙}{\times} B)))$
76	14 19 24 29 42 75	nn0ind	$⊢ K \in ℕ_{0} \to (φ \to (K \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (K \underset{˙}{\times} B))$
77	8 76	mpcom	$⊢ φ \to (K \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (K \underset{˙}{\times} B)$

Metamath Proof Explorer

Theorem srgpcomp

Proof