Metamath Proof Explorer

Theorem selvcl

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

Ref Expression
Hypotheses selvcl.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
selvcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
selvcl.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
selvcl.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
selvcl.e ⊢ 𝐸 = ( Base ‘ 𝑇 )
selvcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
selvcl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
selvcl.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
selvcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion selvcl ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 selvcl.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 selvcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 selvcl.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
4 selvcl.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
5 selvcl.e ⊢ 𝐸 = ( Base ‘ 𝑇 )
6 selvcl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7 selvcl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
8 selvcl.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
9 selvcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10 eqid ⊢ ( algSc ‘ 𝑇 ) = ( algSc ‘ 𝑇 )
11 eqid ⊢ ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) = ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) )
12 1 2 3 4 10 11 6 7 8 9 selvval ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
13 eqid ⊢ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) = ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) )
14 eqid ⊢ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) )
15 6 8 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
16 6 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
17 3 mplcrng ⊢ ( ( ( 𝐼 ∖ 𝐽 ) ∈ V ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ CRing )
18 16 7 17 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
19 4 mplcrng ⊢ ( ( 𝐽 ∈ V ∧ 𝑈 ∈ CRing ) → 𝑇 ∈ CRing )
20 15 18 19 syl2anc ⊢ ( 𝜑 → 𝑇 ∈ CRing )
21 ovexd ⊢ ( 𝜑 → ( 𝐸 ↑m 𝐼 ) ∈ V )
22 eqid ⊢ ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) = ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) )
23 eqid ⊢ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) = ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) )
24 eqid ⊢ ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) = ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) )
25 3 4 10 11 22 23 24 13 5 6 7 8 selvval2lemn ⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ∈ ( ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) RingHom ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
26 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) )
27 26 14 rhmf ⊢ ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ∈ ( ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) RingHom ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) : ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) ⟶ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
28 25 27 syl ⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) : ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) ⟶ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
29 1 2 3 4 10 11 24 23 26 6 7 8 9 selvval2lem4 ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) )
30 28 29 ffvelrnd ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ∈ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
31 13 5 14 20 21 30 pwselbas ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) : ( 𝐸 ↑m 𝐼 ) ⟶ 𝐸 )
32 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
33 3 4 10 5 32 6 7 8 selvval2lem5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ∈ ( 𝐸 ↑m 𝐼 ) )
34 31 33 ffvelrnd ⊢ ( 𝜑 → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ 𝐸 )
35 12 34 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝐸 )