Theorem 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={\mathrm{Base}}_R$$
	srgpcomp.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	srgpcomp.g	$$⊢G={\mathrm{mulGrp}}_R$$
	srgpcomp.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	srgpcomp.r	$$⊢\phi \to R\in \mathrm{SRing}$$
	srgpcomp.a	$$⊢\phi \to A\in S$$
	srgpcomp.b	$$⊢\phi \to B\in S$$
	srgpcomp.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	srgpcomp.c	$$⊢\phi \to A\underset{\dot{}}{\times }B=B\underset{\dot{}}{\times }A$$
	srgpcompp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	srgpcompp	$$⊢\phi \to \left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A=\left(\left(N+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$

Proof

Step	Hyp	Ref	Expression
1		srgpcomp.s	$$⊢S={\mathrm{Base}}_R$$
2		srgpcomp.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
3		srgpcomp.g	$$⊢G={\mathrm{mulGrp}}_R$$
4		srgpcomp.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
5		srgpcomp.r	$$⊢\phi \to R\in \mathrm{SRing}$$
6		srgpcomp.a	$$⊢\phi \to A\in S$$
7		srgpcomp.b	$$⊢\phi \to B\in S$$
8		srgpcomp.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
9		srgpcomp.c	$$⊢\phi \to A\underset{\dot{}}{\times }B=B\underset{\dot{}}{\times }A$$
10		srgpcompp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11	3	srgmgp	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$
12	5 11	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
13	3 1	mgpbas	$$⊢S={\mathrm{Base}}_G$$
14	13 4	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge A\in S\right)\to N\underset{\dot{}}{\times }A\in S$$
15	12 10 6 14	syl3anc	$$⊢\phi \to N\underset{\dot{}}{\times }A\in S$$
16	13 4	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge K\in {\mathbb{N}}_0\wedge B\in S\right)\to K\underset{\dot{}}{\times }B\in S$$
17	12 8 7 16	syl3anc	$$⊢\phi \to K\underset{\dot{}}{\times }B\in S$$
18	1 2	srgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(N\underset{\dot{}}{\times }A\in S\wedge K\underset{\dot{}}{\times }B\in S\wedge A\in S\right)\right)\to \left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)$$
19	5 15 17 6 18	syl13anc	$$⊢\phi \to \left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)$$
20	1 2 3 4 5 6 7 8 9	srgpcomp	$$⊢\phi \to \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$
21	20	oveq2d	$$⊢\phi \to \left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$
22	1 2	srgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(N\underset{\dot{}}{\times }A\in S\wedge A\in S\wedge K\underset{\dot{}}{\times }B\in S\right)\right)\to \left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$
23	5 15 6 17 22	syl13anc	$$⊢\phi \to \left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$
24	21 23	eqtr4d	$$⊢\phi \to \left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)=\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$
25	3 2	mgpplusg	$$⊢\underset{\dot{}}{\times }={+}_G$$
26	13 4 25	mulgnn0p1	$$⊢\left(G\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge A\in S\right)\to \left(N+1\right)\underset{\dot{}}{\times }A=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A$$
27	12 10 6 26	syl3anc	$$⊢\phi \to \left(N+1\right)\underset{\dot{}}{\times }A=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A$$
28	27	eqcomd	$$⊢\phi \to \left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A=\left(N+1\right)\underset{\dot{}}{\times }A$$
29	28	oveq1d	$$⊢\phi \to \left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)=\left(\left(N+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$
30	19 24 29	3eqtrd	$$⊢\phi \to \left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A=\left(\left(N+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$