Metamath Proof Explorer

Theorem selvval2

Description: Value of the "variable selection" function. Convert selvval into a simpler form by using evlsevl . (Contributed by SN, 9-Feb-2025)

Ref Expression
Hypotheses selvval2.p ⊢ P = I mPoly R
selvval2.b ⊢ B = Base P
selvval2.u ⊢ U = I ∖ J mPoly R
selvval2.t ⊢ T = J mPoly U
selvval2.c ⊢ C = algSc ⁡ T
selvval2.d ⊢ D = C ∘ algSc ⁡ U
selvval2.r ⊢ φ → R ∈ CRing
selvval2.j ⊢ φ → J ⊆ I
selvval2.f ⊢ φ → F ∈ B
Assertion selvval2 ⊢ φ → I selectVars R ⁡ J ⁡ F = I eval T ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x

Proof

Step Hyp Ref Expression
1 selvval2.p ⊢ P = I mPoly R
2 selvval2.b ⊢ B = Base P
3 selvval2.u ⊢ U = I ∖ J mPoly R
4 selvval2.t ⊢ T = J mPoly U
5 selvval2.c ⊢ C = algSc ⁡ T
6 selvval2.d ⊢ D = C ∘ algSc ⁡ U
7 selvval2.r ⊢ φ → R ∈ CRing
8 selvval2.j ⊢ φ → J ⊆ I
9 selvval2.f ⊢ φ → F ∈ B
10 1 2 mplrcl ⊢ F ∈ B → I ∈ V
11 9 10 syl ⊢ φ → I ∈ V
12 1 2 3 4 5 6 11 7 8 9 selvval ⊢ φ → I selectVars R ⁡ J ⁡ F = I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
13 eqid ⊢ I evalSub T ⁡ ran ⁡ D = I evalSub T ⁡ ran ⁡ D
14 eqid ⊢ I eval T = I eval T
15 eqid ⊢ I mPoly T ↾ 𝑠 ran ⁡ D = I mPoly T ↾ 𝑠 ran ⁡ D
16 eqid ⊢ T ↾ 𝑠 ran ⁡ D = T ↾ 𝑠 ran ⁡ D
17 eqid ⊢ Base I mPoly T ↾ 𝑠 ran ⁡ D = Base I mPoly T ↾ 𝑠 ran ⁡ D
18 11 8 ssexd ⊢ φ → J ∈ V
19 11 difexd ⊢ φ → I ∖ J ∈ V
20 3 19 7 mplcrngd ⊢ φ → U ∈ CRing
21 4 18 20 mplcrngd ⊢ φ → T ∈ CRing
22 3 4 5 6 19 18 7 selvcllem3 ⊢ φ → ran ⁡ D ∈ SubRing ⁡ T
23 1 2 3 4 5 6 16 15 17 7 8 9 selvcllem4 ⊢ φ → D ∘ F ∈ Base I mPoly T ↾ 𝑠 ran ⁡ D
24 13 14 15 16 17 11 21 22 23 evlsevl ⊢ φ → I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F = I eval T ⁡ D ∘ F
25 24 fveq1d ⊢ φ → I evalSub T ⁡ ran ⁡ D ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
26 12 25 eqtrd ⊢ φ → I selectVars R ⁡ J ⁡ F = I eval T ⁡ D ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x