Metamath Proof Explorer

Theorem selvcl

Description: Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024)

Ref Expression
Hypotheses selvcl.p ⊢ P = I mPoly R
selvcl.b ⊢ B = Base P
selvcl.u ⊢ U = I ∖ J mPoly R
selvcl.t ⊢ T = J mPoly U
selvcl.e ⊢ E = Base T
selvcl.i ⊢ φ → I ∈ V
selvcl.r ⊢ φ → R ∈ CRing
selvcl.j ⊢ φ → J ⊆ I
selvcl.f ⊢ φ → F ∈ B
Assertion selvcl ⊢ φ → I selectVars R ⁡ J ⁡ F ∈ E

Proof

Step Hyp Ref Expression
1 selvcl.p ⊢ P = I mPoly R
2 selvcl.b ⊢ B = Base P
3 selvcl.u ⊢ U = I ∖ J mPoly R
4 selvcl.t ⊢ T = J mPoly U
5 selvcl.e ⊢ E = Base T
6 selvcl.i ⊢ φ → I ∈ V
7 selvcl.r ⊢ φ → R ∈ CRing
8 selvcl.j ⊢ φ → J ⊆ I
9 selvcl.f ⊢ φ → F ∈ B
10 eqid ⊢ algSc ⁡ T = algSc ⁡ T
11 eqid ⊢ algSc ⁡ T ∘ algSc ⁡ U = algSc ⁡ T ∘ algSc ⁡ U
12 1 2 3 4 10 11 6 7 8 9 selvval ⊢ φ → I selectVars R ⁡ J ⁡ F = I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
13 eqid ⊢ T ↑ 𝑠 E I = T ↑ 𝑠 E I
14 eqid ⊢ Base T ↑ 𝑠 E I = Base T ↑ 𝑠 E I
15 6 8 ssexd ⊢ φ → J ∈ V
16 difexg ⊢ I ∈ V → I ∖ J ∈ V
17 6 16 syl ⊢ φ → I ∖ J ∈ V
18 3 mplcrng ⊢ I ∖ J ∈ V ∧ R ∈ CRing → U ∈ CRing
19 17 7 18 syl2anc ⊢ φ → U ∈ CRing
20 4 mplcrng ⊢ J ∈ V ∧ U ∈ CRing → T ∈ CRing
21 15 19 20 syl2anc ⊢ φ → T ∈ CRing
22 ovexd ⊢ φ → E I ∈ V
23 eqid ⊢ I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
24 eqid ⊢ I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
25 eqid ⊢ T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
26 3 4 10 11 23 24 25 13 5 6 7 8 selvval2lemn ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ∈ I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U RingHom T ↑ 𝑠 E I
27 eqid ⊢ Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
28 27 14 rhmf ⊢ I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ∈ I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U RingHom T ↑ 𝑠 E I → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U : Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⟶ Base T ↑ 𝑠 E I
29 26 28 syl ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U : Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⟶ Base T ↑ 𝑠 E I
30 1 2 3 4 10 11 25 24 27 6 7 8 9 selvval2lem4 ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ F ∈ Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
31 29 30 ffvelrnd ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ∈ Base T ↑ 𝑠 E I
32 13 5 14 21 22 31 pwselbas ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F : E I ⟶ E
33 eqid ⊢ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
34 3 4 10 5 33 6 7 8 selvval2lem5 ⊢ φ → x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ∈ E I
35 32 34 ffvelrnd ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ∈ E
36 12 35 eqeltrd ⊢ φ → I selectVars R ⁡ J ⁡ F ∈ E