Theorem srgpcomppsc

Description: If two elements of a semiring commute, they also commute if the elements are raised to a higher power and a scalar multiplication is involved. (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$$
	srgpcomppsc.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	srgpcomppsc.c	$$⊢\phi \to C\in {\mathbb{N}}_0$$
Assertion	srgpcomppsc	$$⊢\phi \to \left(C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\right)\underset{\dot{}}{\times }A=C\underset{\dot{}}{·}\left(\left(\left(N+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\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		srgpcomppsc.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
12		srgpcomppsc.c	$$⊢\phi \to C\in {\mathbb{N}}_0$$
13	3	srgmgp	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$
14	5 13	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
15	3 1	mgpbas	$$⊢S={\mathrm{Base}}_G$$
16	15 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$$
17	14 10 6 16	syl3anc	$$⊢\phi \to N\underset{\dot{}}{\times }A\in S$$
18	15 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$$
19	14 8 7 18	syl3anc	$$⊢\phi \to K\underset{\dot{}}{\times }B\in S$$
20	1 11 2	srgmulgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(C\in {\mathbb{N}}_0\wedge N\underset{\dot{}}{\times }A\in S\wedge K\underset{\dot{}}{\times }B\in S\right)\right)\to \left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)=C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$
21	20	eqcomd	$$⊢\left(R\in \mathrm{SRing}\wedge \left(C\in {\mathbb{N}}_0\wedge N\underset{\dot{}}{\times }A\in S\wedge K\underset{\dot{}}{\times }B\in S\right)\right)\to C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)=\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$
22	5 12 17 19 21	syl13anc	$$⊢\phi \to C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)=\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$
23	22	oveq1d	$$⊢\phi \to \left(C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\right)\underset{\dot{}}{\times }A=\left(\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A$$
24		srgmnd	$$⊢R\in \mathrm{SRing}\to R\in \mathrm{Mnd}$$
25	5 24	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
26	1 11	mulgnn0cl	$$⊢\left(R\in \mathrm{Mnd}\wedge C\in {\mathbb{N}}_0\wedge N\underset{\dot{}}{\times }A\in S\right)\to C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\in S$$
27	25 12 17 26	syl3anc	$$⊢\phi \to C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\in S$$
28	1 2	srgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\in S\wedge K\underset{\dot{}}{\times }B\in S\wedge A\in S\right)\right)\to \left(\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A=\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)$$
29	5 27 19 6 28	syl13anc	$$⊢\phi \to \left(\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A=\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)$$
30	23 29	eqtrd	$$⊢\phi \to \left(C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\right)\underset{\dot{}}{\times }A=\left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)$$
31	1 2	srgcl	$$⊢\left(R\in \mathrm{SRing}\wedge K\underset{\dot{}}{\times }B\in S\wedge A\in S\right)\to \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\in S$$
32	5 19 6 31	syl3anc	$$⊢\phi \to \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\in S$$
33	1 11 2	srgmulgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(C\in {\mathbb{N}}_0\wedge N\underset{\dot{}}{\times }A\in S\wedge \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\in S\right)\right)\to \left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)=C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\right)$$
34	5 12 17 32 33	syl13anc	$$⊢\phi \to \left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)=C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\right)$$
35	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)$$
36	5 17 19 6 35	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)$$
37	36	eqcomd	$$⊢\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 }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A$$
38	37	oveq2d	$$⊢\phi \to C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\right)=C\underset{\dot{}}{·}\left(\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A\right)$$
39	34 38	eqtrd	$$⊢\phi \to \left(C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\right)\underset{\dot{}}{\times }\left(\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)=C\underset{\dot{}}{·}\left(\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A\right)$$
40	1 2 3 4 5 6 7 8 9 10	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)$$
41	40	oveq2d	$$⊢\phi \to C\underset{\dot{}}{·}\left(\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }A\right)=C\underset{\dot{}}{·}\left(\left(\left(N+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$
42	30 39 41	3eqtrd	$$⊢\phi \to \left(C\underset{\dot{}}{·}\left(\left(N\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\right)\underset{\dot{}}{\times }A=C\underset{\dot{}}{·}\left(\left(\left(N+1\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$