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 S = Base R
srgpcomp.m × ˙ = R
srgpcomp.g G = mulGrp R
srgpcomp.e × ˙ = G
srgpcomp.r φ R SRing
srgpcomp.a φ A S
srgpcomp.b φ B S
srgpcomp.k φ K 0
srgpcomp.c φ A × ˙ B = B × ˙ A
srgpcompp.n φ N 0
srgpcomppsc.t · ˙ = R
srgpcomppsc.c φ C 0
Assertion srgpcomppsc φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N + 1 × ˙ A × ˙ K × ˙ B

Proof

Step Hyp Ref Expression
1 srgpcomp.s S = Base R
2 srgpcomp.m × ˙ = R
3 srgpcomp.g G = mulGrp R
4 srgpcomp.e × ˙ = G
5 srgpcomp.r φ R SRing
6 srgpcomp.a φ A S
7 srgpcomp.b φ B S
8 srgpcomp.k φ K 0
9 srgpcomp.c φ A × ˙ B = B × ˙ A
10 srgpcompp.n φ N 0
11 srgpcomppsc.t · ˙ = R
12 srgpcomppsc.c φ C 0
13 3 1 mgpbas S = Base G
14 3 srgmgp R SRing G Mnd
15 5 14 syl φ G Mnd
16 13 4 15 10 6 mulgnn0cld φ N × ˙ A S
17 13 4 15 8 7 mulgnn0cld φ K × ˙ B S
18 1 11 2 srgmulgass R SRing C 0 N × ˙ A S K × ˙ B S C · ˙ N × ˙ A × ˙ K × ˙ B = C · ˙ N × ˙ A × ˙ K × ˙ B
19 18 eqcomd R SRing C 0 N × ˙ A S K × ˙ B S C · ˙ N × ˙ A × ˙ K × ˙ B = C · ˙ N × ˙ A × ˙ K × ˙ B
20 5 12 16 17 19 syl13anc φ C · ˙ N × ˙ A × ˙ K × ˙ B = C · ˙ N × ˙ A × ˙ K × ˙ B
21 20 oveq1d φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
22 srgmnd R SRing R Mnd
23 5 22 syl φ R Mnd
24 1 11 23 12 16 mulgnn0cld φ C · ˙ N × ˙ A S
25 1 2 srgass R SRing C · ˙ N × ˙ A S K × ˙ B S A S C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
26 5 24 17 6 25 syl13anc φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
27 21 26 eqtrd φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
28 1 2 srgcl R SRing K × ˙ B S A S K × ˙ B × ˙ A S
29 5 17 6 28 syl3anc φ K × ˙ B × ˙ A S
30 1 11 2 srgmulgass R SRing C 0 N × ˙ A S K × ˙ B × ˙ A S C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
31 5 12 16 29 30 syl13anc φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
32 1 2 srgass R SRing N × ˙ A S K × ˙ B S A S N × ˙ A × ˙ K × ˙ B × ˙ A = N × ˙ A × ˙ K × ˙ B × ˙ A
33 5 16 17 6 32 syl13anc φ N × ˙ A × ˙ K × ˙ B × ˙ A = N × ˙ A × ˙ K × ˙ B × ˙ A
34 33 eqcomd φ N × ˙ A × ˙ K × ˙ B × ˙ A = N × ˙ A × ˙ K × ˙ B × ˙ A
35 34 oveq2d φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
36 31 35 eqtrd φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A
37 1 2 3 4 5 6 7 8 9 10 srgpcompp φ N × ˙ A × ˙ K × ˙ B × ˙ A = N + 1 × ˙ A × ˙ K × ˙ B
38 37 oveq2d φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N + 1 × ˙ A × ˙ K × ˙ B
39 27 36 38 3eqtrd φ C · ˙ N × ˙ A × ˙ K × ˙ B × ˙ A = C · ˙ N + 1 × ˙ A × ˙ K × ˙ B