Metamath Proof Explorer

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

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 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 𝐵 ) = ( 0 ↑ 𝐵 ) )
11 10 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( ( 0 ↑ 𝐵 ) × 𝐴 ) )
12 10 oveq2d ⊢ ( 𝑥 = 0 → ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) = ( 𝐴 × ( 0 ↑ 𝐵 ) ) )
13 11 12 eqeq12d ⊢ ( 𝑥 = 0 → ( ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ↔ ( ( 0 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 0 ↑ 𝐵 ) ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 0 → ( ( 𝜑 → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ) ↔ ( 𝜑 → ( ( 0 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 0 ↑ 𝐵 ) ) ) ) )
15 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝐵 ) = ( 𝑦 ↑ 𝐵 ) )
16 15 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) )
17 15 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) )
18 16 17 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ↔ ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) ) )
19 18 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ) ↔ ( 𝜑 → ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) ) ) )
20 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ 𝐵 ) = ( ( 𝑦 + 1 ) ↑ 𝐵 ) )
21 20 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) )
22 20 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) )
23 21 22 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ↔ ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) ) )
24 23 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝜑 → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ) ↔ ( 𝜑 → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) ) ) )
25 oveq1 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 ↑ 𝐵 ) = ( 𝐾 ↑ 𝐵 ) )
26 25 oveq1d ⊢ ( 𝑥 = 𝐾 → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) )
27 25 oveq2d ⊢ ( 𝑥 = 𝐾 → ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) = ( 𝐴 × ( 𝐾 ↑ 𝐵 ) ) )
28 26 27 eqeq12d ⊢ ( 𝑥 = 𝐾 → ( ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ↔ ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝐾 ↑ 𝐵 ) ) ) )
29 28 imbi2d ⊢ ( 𝑥 = 𝐾 → ( ( 𝜑 → ( ( 𝑥 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑥 ↑ 𝐵 ) ) ) ↔ ( 𝜑 → ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝐾 ↑ 𝐵 ) ) ) ) )
30 3 1 mgpbas ⊢ 𝑆 = ( Base ‘ 𝐺 )
31 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
32 3 31 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝐺 )
33 30 32 4 mulg0 ⊢ ( 𝐵 ∈ 𝑆 → ( 0 ↑ 𝐵 ) = ( 1r ‘ 𝑅 ) )
34 7 33 syl ⊢ ( 𝜑 → ( 0 ↑ 𝐵 ) = ( 1r ‘ 𝑅 ) )
35 34 oveq1d ⊢ ( 𝜑 → ( ( 0 ↑ 𝐵 ) × 𝐴 ) = ( ( 1r ‘ 𝑅 ) × 𝐴 ) )
36 1 2 31 srgridm ⊢ ( ( 𝑅 ∈ SRing ∧ 𝐴 ∈ 𝑆 ) → ( 𝐴 × ( 1r ‘ 𝑅 ) ) = 𝐴 )
37 5 6 36 syl2anc ⊢ ( 𝜑 → ( 𝐴 × ( 1r ‘ 𝑅 ) ) = 𝐴 )
38 34 oveq2d ⊢ ( 𝜑 → ( 𝐴 × ( 0 ↑ 𝐵 ) ) = ( 𝐴 × ( 1r ‘ 𝑅 ) ) )
39 1 2 31 srglidm ⊢ ( ( 𝑅 ∈ SRing ∧ 𝐴 ∈ 𝑆 ) → ( ( 1r ‘ 𝑅 ) × 𝐴 ) = 𝐴 )
40 5 6 39 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) × 𝐴 ) = 𝐴 )
41 37 38 40 3eqtr4rd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) × 𝐴 ) = ( 𝐴 × ( 0 ↑ 𝐵 ) ) )
42 35 41 eqtrd ⊢ ( 𝜑 → ( ( 0 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 0 ↑ 𝐵 ) ) )
43 3 srgmgp ⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
44 5 43 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → 𝑦 ∈ ℕ0 )
47 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → 𝐵 ∈ 𝑆 )
48 3 2 mgpplusg ⊢ × = ( +g ‘ 𝐺 )
49 30 4 48 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝑦 + 1 ) ↑ 𝐵 ) = ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) )
50 45 46 47 49 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 + 1 ) ↑ 𝐵 ) = ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) )
51 50 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) × 𝐴 ) )
52 9 eqcomd ⊢ ( 𝜑 → ( 𝐵 × 𝐴 ) = ( 𝐴 × 𝐵 ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( 𝐵 × 𝐴 ) = ( 𝐴 × 𝐵 ) )
54 53 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 ↑ 𝐵 ) × ( 𝐵 × 𝐴 ) ) = ( ( 𝑦 ↑ 𝐵 ) × ( 𝐴 × 𝐵 ) ) )
55 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → 𝑅 ∈ SRing )
56 30 4 45 46 47 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑦 ↑ 𝐵 ) ∈ 𝑆 )
57 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → 𝐴 ∈ 𝑆 )
58 1 2 srgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑦 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) × 𝐴 ) = ( ( 𝑦 ↑ 𝐵 ) × ( 𝐵 × 𝐴 ) ) )
59 55 56 47 57 58 syl13anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) × 𝐴 ) = ( ( 𝑦 ↑ 𝐵 ) × ( 𝐵 × 𝐴 ) ) )
60 1 2 srgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( ( 𝑦 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) × 𝐵 ) = ( ( 𝑦 ↑ 𝐵 ) × ( 𝐴 × 𝐵 ) ) )
61 55 56 57 47 60 syl13anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) × 𝐵 ) = ( ( 𝑦 ↑ 𝐵 ) × ( 𝐴 × 𝐵 ) ) )
62 54 59 61 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) × 𝐴 ) = ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) × 𝐵 ) )
63 51 62 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) × 𝐵 ) )
64 63 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) ) → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) × 𝐵 ) )
65 oveq1 ⊢ ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) × 𝐵 ) = ( ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) × 𝐵 ) )
66 1 2 srgass ⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐴 ∈ 𝑆 ∧ ( 𝑦 ↑ 𝐵 ) ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) × 𝐵 ) = ( 𝐴 × ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) ) )
67 55 57 56 47 66 syl13anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) × 𝐵 ) = ( 𝐴 × ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) ) )
68 50 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) = ( ( 𝑦 + 1 ) ↑ 𝐵 ) )
69 68 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( 𝐴 × ( ( 𝑦 ↑ 𝐵 ) × 𝐵 ) ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) )
70 67 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) × 𝐵 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) )
71 65 70 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) × 𝐵 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) )
72 64 71 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) ) → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) )
73 72 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) ) )
74 73 expcom ⊢ ( 𝑦 ∈ ℕ0 → ( 𝜑 → ( ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) ) ) )
75 74 a2d ⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝜑 → ( ( 𝑦 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝑦 ↑ 𝐵 ) ) ) → ( 𝜑 → ( ( ( 𝑦 + 1 ) ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( ( 𝑦 + 1 ) ↑ 𝐵 ) ) ) ) )
76 14 19 24 29 42 75 nn0ind ⊢ ( 𝐾 ∈ ℕ0 → ( 𝜑 → ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝐾 ↑ 𝐵 ) ) ) )
77 8 76 mpcom ⊢ ( 𝜑 → ( ( 𝐾 ↑ 𝐵 ) × 𝐴 ) = ( 𝐴 × ( 𝐾 ↑ 𝐵 ) ) )