This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evls1varpwval

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval . (Contributed by Thierry Arnoux, 24-Jan-2025)

Ref Expression
Hypotheses evls1varpwval.q ⊢ Q = S evalSub 1 R
evls1varpwval.u ⊢ U = S ↾ 𝑠 R
evls1varpwval.w ⊢ W = Poly 1 ⁡ U
evls1varpwval.x ⊢ X = var 1 ⁡ U
evls1varpwval.b ⊢ B = Base S
evls1varpwval.e ⊢ ∧ ˙ = ⋅ mulGrp W
evls1varpwval.f ⊢ × ˙ = ⋅ mulGrp S
evls1varpwval.s ⊢ φ → S ∈ CRing
evls1varpwval.r ⊢ φ → R ∈ SubRing ⁡ S
evls1varpwval.n ⊢ φ → N ∈ ℕ 0
evls1varpwval.c ⊢ φ → C ∈ B
Assertion evls1varpwval ⊢ φ → Q ⁡ N ∧ ˙ X ⁡ C = N × ˙ C

Proof

Step Hyp Ref Expression
1 evls1varpwval.q ⊢ Q = S evalSub 1 R
2 evls1varpwval.u ⊢ U = S ↾ 𝑠 R
3 evls1varpwval.w ⊢ W = Poly 1 ⁡ U
4 evls1varpwval.x ⊢ X = var 1 ⁡ U
5 evls1varpwval.b ⊢ B = Base S
6 evls1varpwval.e ⊢ ∧ ˙ = ⋅ mulGrp W
7 evls1varpwval.f ⊢ × ˙ = ⋅ mulGrp S
8 evls1varpwval.s ⊢ φ → S ∈ CRing
9 evls1varpwval.r ⊢ φ → R ∈ SubRing ⁡ S
10 evls1varpwval.n ⊢ φ → N ∈ ℕ 0
11 evls1varpwval.c ⊢ φ → C ∈ B
12 eqid ⊢ Base W = Base W
13 2 subrgring ⊢ R ∈ SubRing ⁡ S → U ∈ Ring
14 4 3 12 vr1cl ⊢ U ∈ Ring → X ∈ Base W
15 9 13 14 3syl ⊢ φ → X ∈ Base W
16 1 5 3 2 12 8 9 6 7 10 15 11 evls1expd ⊢ φ → Q ⁡ N ∧ ˙ X ⁡ C = N × ˙ Q ⁡ X ⁡ C
17 1 4 2 5 8 9 evls1var ⊢ φ → Q ⁡ X = I ↾ B
18 17 fveq1d ⊢ φ → Q ⁡ X ⁡ C = I ↾ B ⁡ C
19 fvresi ⊢ C ∈ B → I ↾ B ⁡ C = C
20 11 19 syl ⊢ φ → I ↾ B ⁡ C = C
21 18 20 eqtrd ⊢ φ → Q ⁡ X ⁡ C = C
22 21 oveq2d ⊢ φ → N × ˙ Q ⁡ X ⁡ C = N × ˙ C
23 16 22 eqtrd ⊢ φ → Q ⁡ N ∧ ˙ X ⁡ C = N × ˙ C