Theorem srgpcomp

Description: If two elements of a semiring commute, they also commute if one of the elements is 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$$
Assertion	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)$$

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		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }B=0\underset{\dot{}}{\times }B$$
11	10	oveq1d	$$⊢x=0\to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(0\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A$$
12	10	oveq2d	$$⊢x=0\to A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)=A\underset{\dot{}}{\times }\left(0\underset{\dot{}}{\times }B\right)$$
13	11 12	eqeq12d	$$⊢x=0\to \left(\left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\leftrightarrow \left(0\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(0\underset{\dot{}}{\times }B\right)\right)$$
14	13	imbi2d	$$⊢x=0\to \left(\left(\phi \to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\right)\leftrightarrow \left(\phi \to \left(0\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(0\underset{\dot{}}{\times }B\right)\right)\right)$$
15		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }B=y\underset{\dot{}}{\times }B$$
16	15	oveq1d	$$⊢x=y\to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A$$
17	15	oveq2d	$$⊢x=y\to A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)$$
18	16 17	eqeq12d	$$⊢x=y\to \left(\left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\leftrightarrow \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)$$
19	18	imbi2d	$$⊢x=y\to \left(\left(\phi \to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\right)\leftrightarrow \left(\phi \to \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\right)$$
20		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }B=\left(y+1\right)\underset{\dot{}}{\times }B$$
21	20	oveq1d	$$⊢x=y+1\to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A$$
22	20	oveq2d	$$⊢x=y+1\to A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)$$
23	21 22	eqeq12d	$$⊢x=y+1\to \left(\left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\leftrightarrow \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\right)$$
24	23	imbi2d	$$⊢x=y+1\to \left(\left(\phi \to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\right)\leftrightarrow \left(\phi \to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\right)\right)$$
25		oveq1	$$⊢x=K\to x\underset{\dot{}}{\times }B=K\underset{\dot{}}{\times }B$$
26	25	oveq1d	$$⊢x=K\to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A$$
27	25	oveq2d	$$⊢x=K\to A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)=A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$
28	26 27	eqeq12d	$$⊢x=K\to \left(\left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\leftrightarrow \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$
29	28	imbi2d	$$⊢x=K\to \left(\left(\phi \to \left(x\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(x\underset{\dot{}}{\times }B\right)\right)\leftrightarrow \left(\phi \to \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)\right)$$
30	3 1	mgpbas	$$⊢S={\mathrm{Base}}_G$$
31		eqid	$$⊢1_R=1_R$$
32	3 31	ringidval	$$⊢1_R=0_G$$
33	30 32 4	mulg0	$$⊢B\in S\to 0\underset{\dot{}}{\times }B=1_R$$
34	7 33	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }B=1_R$$
35	34	oveq1d	$$⊢\phi \to \left(0\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=1_R\underset{\dot{}}{\times }A$$
36	1 2 31	srgridm	$$⊢\left(R\in \mathrm{SRing}\wedge A\in S\right)\to A\underset{\dot{}}{\times }{1}_R=A$$
37	5 6 36	syl2anc	$$⊢\phi \to A\underset{\dot{}}{\times }{1}_R=A$$
38	34	oveq2d	$$⊢\phi \to A\underset{\dot{}}{\times }\left(0\underset{\dot{}}{\times }B\right)=A\underset{\dot{}}{\times }{1}_R$$
39	1 2 31	srglidm	$$⊢\left(R\in \mathrm{SRing}\wedge A\in S\right)\to 1_R\underset{\dot{}}{\times }A=A$$
40	5 6 39	syl2anc	$$⊢\phi \to 1_R\underset{\dot{}}{\times }A=A$$
41	37 38 40	3eqtr4rd	$$⊢\phi \to 1_R\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(0\underset{\dot{}}{\times }B\right)$$
42	35 41	eqtrd	$$⊢\phi \to \left(0\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(0\underset{\dot{}}{\times }B\right)$$
43	3	srgmgp	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$
44	5 43	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
45	44	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to G\in \mathrm{Mnd}$$
46		simpr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to y\in {\mathbb{N}}_0$$
47	7	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to B\in S$$
48	3 2	mgpplusg	$$⊢\underset{\dot{}}{\times }={+}_G$$
49	30 4 48	mulgnn0p1	$$⊢\left(G\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge B\in S\right)\to \left(y+1\right)\underset{\dot{}}{\times }B=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B$$
50	45 46 47 49	syl3anc	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(y+1\right)\underset{\dot{}}{\times }B=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B$$
51	50	oveq1d	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A$$
52	9	eqcomd	$$⊢\phi \to B\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }B$$
53	52	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to B\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }B$$
54	53	oveq2d	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }\left(B\underset{\dot{}}{\times }A\right)=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }\left(A\underset{\dot{}}{\times }B\right)$$
55	5	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to R\in \mathrm{SRing}$$
56	30 4 45 46 47	mulgnn0cld	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to y\underset{\dot{}}{\times }B\in S$$
57	6	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to A\in S$$
58	1 2	srgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(y\underset{\dot{}}{\times }B\in S\wedge B\in S\wedge A\in S\right)\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }\left(B\underset{\dot{}}{\times }A\right)$$
59	55 56 47 57 58	syl13anc	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }\left(B\underset{\dot{}}{\times }A\right)$$
60	1 2	srgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(y\underset{\dot{}}{\times }B\in S\wedge A\in S\wedge B\in S\right)\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }B=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }\left(A\underset{\dot{}}{\times }B\right)$$
61	55 56 57 47 60	syl13anc	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }B=\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }\left(A\underset{\dot{}}{\times }B\right)$$
62	54 59 61	3eqtr4d	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }B$$
63	51 62	eqtrd	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }B$$
64	63	adantr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=\left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }B$$
65		oveq1	$$⊢\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }B=\left(A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }B$$
66	1 2	srgass	$$⊢\left(R\in \mathrm{SRing}\wedge \left(A\in S\wedge y\underset{\dot{}}{\times }B\in S\wedge B\in S\right)\right)\to \left(A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }B=A\underset{\dot{}}{\times }\left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B\right)$$
67	55 57 56 47 66	syl13anc	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }B=A\underset{\dot{}}{\times }\left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B\right)$$
68	50	eqcomd	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B=\left(y+1\right)\underset{\dot{}}{\times }B$$
69	68	oveq2d	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to A\underset{\dot{}}{\times }\left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }B\right)=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)$$
70	67 69	eqtrd	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\underset{\dot{}}{\times }B=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)$$
71	65 70	sylan9eqr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }B=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)$$
72	64 71	eqtrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)$$
73	72	ex	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\right)$$
74	73	expcom	$$⊢y\in {\mathbb{N}}_0\to \left(\phi \to \left(\left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\right)\right)$$
75	74	a2d	$$⊢y\in {\mathbb{N}}_0\to \left(\left(\phi \to \left(y\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(y\underset{\dot{}}{\times }B\right)\right)\to \left(\phi \to \left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(\left(y+1\right)\underset{\dot{}}{\times }B\right)\right)\right)$$
76	14 19 24 29 42 75	nn0ind	$$⊢K\in {\mathbb{N}}_0\to \left(\phi \to \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)\right)$$
77	8 76	mpcom	$$⊢\phi \to \left(K\underset{\dot{}}{\times }B\right)\underset{\dot{}}{\times }A=A\underset{\dot{}}{\times }\left(K\underset{\dot{}}{\times }B\right)$$