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 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 ) 𝐴 ) × ( 𝐾 𝐵 ) ) ) )