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	⊢ 𝑆 = ( Base ‘ 𝑅 )
	srgpcomp.m	⊢ × = ( .r ‘ 𝑅 )
	srgpcomp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	srgpcomp.e	⊢ ↑ = ( .g ‘ 𝐺 )
	srgpcomp.r	⊢ ( 𝜑 → 𝑅 ∈ SRing )
	srgpcomp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	srgpcomp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	srgpcomp.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
	srgpcomp.c	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
	srgpcompp.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	srgpcomppsc.t	⊢ · = ( .g ‘ 𝑅 )
	srgpcomppsc.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
Assertion	srgpcomppsc	⊢ ( 𝜑 → ( ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) × 𝐴 ) = ( 𝐶 · ( ( ( 𝑁 + 1 ) ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		srgpcomp.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
2		srgpcomp.m	⊢ × = ( .r ‘ 𝑅 )
3		srgpcomp.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
4		srgpcomp.e	⊢ ↑ = ( .g ‘ 𝐺 )
5		srgpcomp.r	⊢ ( 𝜑 → 𝑅 ∈ SRing )
6		srgpcomp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
7		srgpcomp.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
8		srgpcomp.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
9		srgpcomp.c	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
10		srgpcompp.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11		srgpcomppsc.t	⊢ · = ( .g ‘ 𝑅 )
12		srgpcomppsc.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
13	3 1	mgpbas	⊢ 𝑆 = ( Base ‘ 𝐺 )
14	3	srgmgp	⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
15	5 14	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
16	13 4 15 10 6	mulgnn0cld	⊢ ( 𝜑 → ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 )
17	13 4 15 8 7	mulgnn0cld	⊢ ( 𝜑 → ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 )
18	1 11 2	srgmulgass	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐶 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ) ) → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) = ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) )
19	18	eqcomd	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐶 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ) ) → ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) )
20	5 12 16 17 19	syl13anc	⊢ ( 𝜑 → ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) )
21	20	oveq1d	⊢ ( 𝜑 → ( ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) × 𝐴 ) = ( ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) )
22		srgmnd	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
23	5 22	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
24	1 11 23 12 16	mulgnn0cld	⊢ ( 𝜑 → ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) ∈ 𝑆 )
25	1 2	srgass	⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
26	5 24 17 6 25	syl13anc	⊢ ( 𝜑 → ( ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
27	21 26	eqtrd	⊢ ( 𝜑 → ( ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) × 𝐴 ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
28	1 2	srgcl	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ∈ 𝑆 )
29	5 17 6 28	syl3anc	⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ∈ 𝑆 )
30	1 11 2	srgmulgass	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐶 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ∈ 𝑆 ) ) → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) ) )
31	5 12 16 29 30	syl13anc	⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) ) )
32	1 2	srgass	⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
33	5 16 17 6 32	syl13anc	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
34	33	eqcomd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) )
35	34	oveq2d	⊢ ( 𝜑 → ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) ) = ( 𝐶 · ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) ) )
36	31 35	eqtrd	⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( 𝐶 · ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) ) )
37	1 2 3 4 5 6 7 8 9 10	srgpcompp	⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( ( 𝑁 + 1 ) ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) )
38	37	oveq2d	⊢ ( 𝜑 → ( 𝐶 · ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) ) = ( 𝐶 · ( ( ( 𝑁 + 1 ) ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) )
39	27 36 38	3eqtrd	⊢ ( 𝜑 → ( ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) × 𝐴 ) = ( 𝐶 · ( ( ( 𝑁 + 1 ) ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) )