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 difexg ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 ∖ 𝐽 ) ∈ V )
17 6 16 syl ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
18 3 mplcrng ⊢ ( ( ( 𝐼 ∖ 𝐽 ) ∈ V ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ CRing )
19 17 7 18 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
20 4 mplcrng ⊢ ( ( 𝐽 ∈ V ∧ 𝑈 ∈ CRing ) → 𝑇 ∈ CRing )
21 15 19 20 syl2anc ⊢ ( 𝜑 → 𝑇 ∈ CRing )
22 ovexd ⊢ ( 𝜑 → ( 𝐸 ↑m 𝐼 ) ∈ V )
23 eqid ⊢ ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) = ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) )
24 eqid ⊢ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) = ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) )
25 eqid ⊢ ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) = ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) )
26 3 4 10 11 23 24 25 13 5 6 7 8 selvval2lemn ⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ∈ ( ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) RingHom ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
27 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) )
28 27 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 𝐼 ) ) ) )
29 26 28 syl ⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) : ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) ⟶ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
30 1 2 3 4 10 11 25 24 27 6 7 8 9 selvval2lem4 ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) )
31 29 30 ffvelrnd ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ∈ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
32 13 5 14 21 22 31 pwselbas ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) : ( 𝐸 ↑m 𝐼 ) ⟶ 𝐸 )
33 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
34 3 4 10 5 33 6 7 8 selvval2lem5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ∈ ( 𝐸 ↑m 𝐼 ) )
35 32 34 ffvelrnd ⊢ ( 𝜑 → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ 𝐸 )
36 12 35 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝐸 )