srgpcompp

Description: If two elements of a semiring commute, they also commute if the elements are 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$
	srgpcompp.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	srgpcompp	$⊢ φ \to ((N \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B)) \underset{˙}{\times} A = ((N + 1) \underset{˙}{\times} 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		srgpcompp.n	$⊢ φ \to N \in ℕ_{0}$
11	3 1	mgpbas	$⊢ S = {Base}_{G}$
12	3	srgmgp	$⊢ R \in SRing \to G \in Mnd$
13	5 12	syl	$⊢ φ \to G \in Mnd$
14	11 4 13 10 6	mulgnn0cld	$⊢ φ \to N \underset{˙}{\times} A \in S$
15	11 4 13 8 7	mulgnn0cld	$⊢ φ \to K \underset{˙}{\times} B \in S$
16	1 2	srgass	$⊢ (R \in SRing \land (N \underset{˙}{\times} A \in S \land K \underset{˙}{\times} B \in S \land A \in S)) \to ((N \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B)) \underset{˙}{\times} A = (N \underset{˙}{\times} A) \underset{˙}{\times} ((K \underset{˙}{\times} B) \underset{˙}{\times} A)$
17	5 14 15 6 16	syl13anc	$⊢ φ \to ((N \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B)) \underset{˙}{\times} A = (N \underset{˙}{\times} A) \underset{˙}{\times} ((K \underset{˙}{\times} B) \underset{˙}{\times} A)$
18	1 2 3 4 5 6 7 8 9	srgpcomp	$⊢ φ \to (K \underset{˙}{\times} B) \underset{˙}{\times} A = A \underset{˙}{\times} (K \underset{˙}{\times} B)$
19	18	oveq2d	$⊢ φ \to (N \underset{˙}{\times} A) \underset{˙}{\times} ((K \underset{˙}{\times} B) \underset{˙}{\times} A) = (N \underset{˙}{\times} A) \underset{˙}{\times} (A \underset{˙}{\times} (K \underset{˙}{\times} B))$
20	1 2	srgass	$⊢ (R \in SRing \land (N \underset{˙}{\times} A \in S \land A \in S \land K \underset{˙}{\times} B \in S)) \to ((N \underset{˙}{\times} A) \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B) = (N \underset{˙}{\times} A) \underset{˙}{\times} (A \underset{˙}{\times} (K \underset{˙}{\times} B))$
21	5 14 6 15 20	syl13anc	$⊢ φ \to ((N \underset{˙}{\times} A) \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B) = (N \underset{˙}{\times} A) \underset{˙}{\times} (A \underset{˙}{\times} (K \underset{˙}{\times} B))$
22	19 21	eqtr4d	$⊢ φ \to (N \underset{˙}{\times} A) \underset{˙}{\times} ((K \underset{˙}{\times} B) \underset{˙}{\times} A) = ((N \underset{˙}{\times} A) \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B)$
23	3 2	mgpplusg	$⊢ \underset{˙}{\times} = +_{G}$
24	11 4 23	mulgnn0p1	$⊢ (G \in Mnd \land N \in ℕ_{0} \land A \in S) \to (N + 1) \underset{˙}{\times} A = (N \underset{˙}{\times} A) \underset{˙}{\times} A$
25	13 10 6 24	syl3anc	$⊢ φ \to (N + 1) \underset{˙}{\times} A = (N \underset{˙}{\times} A) \underset{˙}{\times} A$
26	25	eqcomd	$⊢ φ \to (N \underset{˙}{\times} A) \underset{˙}{\times} A = (N + 1) \underset{˙}{\times} A$
27	26	oveq1d	$⊢ φ \to ((N \underset{˙}{\times} A) \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B) = ((N + 1) \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B)$
28	17 22 27	3eqtrd	$⊢ φ \to ((N \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B)) \underset{˙}{\times} A = ((N + 1) \underset{˙}{\times} A) \underset{˙}{\times} (K \underset{˙}{\times} B)$

Metamath Proof Explorer

Theorem srgpcompp

Proof