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.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.r ⊢ φ → R ∈ CRing
7 selvcl.j ⊢ φ → J ⊆ I
8 selvcl.f ⊢ φ → F ∈ B
9 eqid ⊢ algSc ⁡ T = algSc ⁡ T
10 eqid ⊢ algSc ⁡ T ∘ algSc ⁡ U = algSc ⁡ T ∘ algSc ⁡ U
11 1 2 3 4 9 10 7 8 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
12 eqid ⊢ T ↑ 𝑠 E I = T ↑ 𝑠 E I
13 eqid ⊢ Base T ↑ 𝑠 E I = Base T ↑ 𝑠 E I
14 1 2 mplrcl ⊢ F ∈ B → I ∈ V
15 8 14 syl ⊢ φ → I ∈ V
16 15 7 ssexd ⊢ φ → J ∈ V
17 15 difexd ⊢ φ → I ∖ J ∈ V
18 3 17 6 mplcrngd ⊢ φ → U ∈ CRing
19 4 16 18 mplcrngd ⊢ φ → T ∈ CRing
20 ovexd ⊢ φ → E I ∈ V
21 eqid ⊢ I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
22 eqid ⊢ I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
23 eqid ⊢ T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
24 3 4 9 10 21 22 23 12 5 15 6 7 selvcllemh ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ∈ I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U RingHom T ↑ 𝑠 E I
25 eqid ⊢ Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U = Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
26 25 13 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
27 24 26 syl ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U : Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⟶ Base T ↑ 𝑠 E I
28 1 2 3 4 9 10 23 22 25 6 7 8 selvcllem4 ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ F ∈ Base I mPoly T ↾ 𝑠 ran ⁡ algSc ⁡ T ∘ algSc ⁡ U
29 27 28 ffvelcdmd ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ∈ Base T ↑ 𝑠 E I
30 12 5 13 19 20 29 pwselbas ⊢ φ → I evalSub T ⁡ ran ⁡ algSc ⁡ T ∘ algSc ⁡ U ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F : E I ⟶ E
31 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
32 3 4 9 5 31 15 6 7 selvcllem5 ⊢ φ → x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ∈ E I
33 30 32 ffvelcdmd ⊢ φ → 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
34 11 33 eqeltrd ⊢ φ → I selectVars R ⁡ J ⁡ F ∈ E