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 1	mgpbas	$$⊢S={\mathrm{Base}}_G$$
14	3	srgmgp	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$
15	5 14	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
16	13 4 15 10 6	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }A\in S$$
17	13 4 15 8 7	mulgnn0cld	$$⊢\phi \to K\underset{\dot{}}{\times }B\in S$$
18	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)$$
19	18	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)$$
20	5 12 16 17 19	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)$$
21	20	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$$
22		srgmnd	$$⊢R\in \mathrm{SRing}\to R\in \mathrm{Mnd}$$
23	5 22	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
24	1 11 23 12 16	mulgnn0cld	$$⊢\phi \to C\underset{\dot{}}{·}\left(N\underset{\dot{}}{\times }A\right)\in S$$
25	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)$$
26	5 24 17 6 25	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)$$
27	21 26	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)$$
28	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$$
29	5 17 6 28	syl3anc	$$⊢\phi \to \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\in S$$
30	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)$$
31	5 12 16 29 30	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)$$
32	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)$$
33	5 16 17 6 32	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)$$
34	33	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$$
35	34	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)$$
36	31 35	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)$$
37	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)$$
38	37	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)$$
39	27 36 38	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)$$