Metamath Proof Explorer

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 srgmgp ⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
14 5 13 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
15 3 1 mgpbas ⊢ 𝑆 = ( Base ‘ 𝐺 )
16 15 4 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 )
17 14 10 6 16 syl3anc ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 )
18 15 4 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐾 ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 )
19 14 8 7 18 syl3anc ⊢ ( 𝜑 → ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 )
20 1 11 2 srgmulgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐶 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ) ) → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) = ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) )
21 20 eqcomd ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐶 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ) ) → ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) )
22 5 12 17 19 21 syl13anc ⊢ ( 𝜑 → ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) )
23 22 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) × 𝐴 ) = ( ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) )
24 srgmnd ⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
25 5 24 syl ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
26 1 11 mulgnn0cl ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐶 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ) → ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) ∈ 𝑆 )
27 25 12 17 26 syl3anc ⊢ ( 𝜑 → ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) ∈ 𝑆 )
28 1 2 srgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
29 5 27 19 6 28 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
30 23 29 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) × 𝐴 ) = ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
31 1 2 srgcl ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ∈ 𝑆 )
32 5 19 6 31 syl3anc ⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ∈ 𝑆 )
33 1 11 2 srgmulgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐶 ∈ ℕ0 ∧ ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ∈ 𝑆 ) ) → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) ) )
34 5 12 17 32 33 syl13anc ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) ) )
35 1 2 srgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑁 ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝐾 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
36 5 17 19 6 35 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) )
37 36 eqcomd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) )
38 37 oveq2d ⊢ ( 𝜑 → ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) ) = ( 𝐶 · ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) ) )
39 34 38 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 · ( 𝑁 ↑ 𝐴 ) ) × ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) ) = ( 𝐶 · ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) ) )
40 1 2 3 4 5 6 7 8 9 10 srgpcompp ⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) = ( ( ( 𝑁 + 1 ) ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) )
41 40 oveq2d ⊢ ( 𝜑 → ( 𝐶 · ( ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) × 𝐴 ) ) = ( 𝐶 · ( ( ( 𝑁 + 1 ) ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) )
42 30 39 41 3eqtrd ⊢ ( 𝜑 → ( ( 𝐶 · ( ( 𝑁 ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) × 𝐴 ) = ( 𝐶 · ( ( ( 𝑁 + 1 ) ↑ 𝐴 ) × ( 𝐾 ↑ 𝐵 ) ) ) )