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.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.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 selvcl.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
8 selvcl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9 eqid ⊢ ( algSc ‘ 𝑇 ) = ( algSc ‘ 𝑇 )
10 eqid ⊢ ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) = ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) )
11 1 2 mplrcl ⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V )
12 8 11 syl ⊢ ( 𝜑 → 𝐼 ∈ V )
13 1 2 3 4 9 10 12 6 7 8 selvval ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
14 eqid ⊢ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) = ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) )
15 eqid ⊢ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) )
16 12 7 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
17 12 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
18 3 17 6 mplcrngd ⊢ ( 𝜑 → 𝑈 ∈ CRing )
19 4 16 18 mplcrngd ⊢ ( 𝜑 → 𝑇 ∈ CRing )
20 ovexd ⊢ ( 𝜑 → ( 𝐸 ↑m 𝐼 ) ∈ V )
21 eqid ⊢ ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) = ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) )
22 eqid ⊢ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) = ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) )
23 eqid ⊢ ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) = ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) )
24 3 4 9 10 21 22 23 14 5 12 6 7 selvcllemh ⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ∈ ( ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) RingHom ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
25 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) )
26 25 15 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 𝐼 ) ) ) )
27 24 26 syl ⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) : ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) ⟶ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
28 1 2 3 4 9 10 23 22 25 6 7 8 selvcllem4 ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ) ) )
29 27 28 ffvelcdmd ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ∈ ( Base ‘ ( 𝑇 ↑s ( 𝐸 ↑m 𝐼 ) ) ) )
30 14 5 15 19 20 29 pwselbas ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) : ( 𝐸 ↑m 𝐼 ) ⟶ 𝐸 )
31 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
32 3 4 9 5 31 12 6 7 selvcllem5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ∈ ( 𝐸 ↑m 𝐼 ) )
33 30 32 ffvelcdmd ⊢ ( 𝜑 → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ 𝐸 )
34 13 33 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝐸 )