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 1	mgpbas	$$⊢S={\mathrm{Base}}_G$$
12	3	srgmgp	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$
13	5 12	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
14	11 4 13 10 6	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }A\in S$$
15	11 4 13 8 7	mulgnn0cld	$$⊢\phi \to K\underset{\dot{}}{\times }B\in S$$
16	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)$$
17	5 14 15 6 16	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)$$
18	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)$$
19	18	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)$$
20	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)$$
21	5 14 6 15 20	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)$$
22	19 21	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)$$
23	3 2	mgpplusg	$$⊢\underset{\dot{}}{\times }={+}_G$$
24	11 4 23	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$$
25	13 10 6 24	syl3anc	$$⊢\phi \to \left(N+1\right)\underset{\dot{}}{\times }A=\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A$$
26	25	eqcomd	$$⊢\phi \to \left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }A=\left(N+1\right)\underset{\dot{}}{\times }A$$
27	26	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)$$
28	17 22 27	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)$$