This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem selvval2

Description: Value of the "variable selection" function. Convert selvval into a simpler form by using evlsevl . (Contributed by SN, 9-Feb-2025)

Ref Expression
Hypotheses selvval2.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
selvval2.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
selvval2.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
selvval2.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
selvval2.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
selvval2.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
selvval2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
selvval2.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
selvval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion selvval2 ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 selvval2.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 selvval2.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 selvval2.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
4 selvval2.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
5 selvval2.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
6 selvval2.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
7 selvval2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
8 selvval2.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
9 selvval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10 1 2 3 4 5 6 8 9 selvval ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
11 eqid ⊢ ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 )
12 eqid ⊢ ( 𝐼 eval 𝑇 ) = ( 𝐼 eval 𝑇 )
13 eqid ⊢ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) = ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) )
14 eqid ⊢ ( 𝑇 ↾s ran 𝐷 ) = ( 𝑇 ↾s ran 𝐷 )
15 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) )
16 1 2 mplrcl ⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V )
17 9 16 syl ⊢ ( 𝜑 → 𝐼 ∈ V )
18 17 8 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
19 17 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
20 3 19 7 mplcrngd ⊢ ( 𝜑 → 𝑈 ∈ CRing )
21 4 18 20 mplcrngd ⊢ ( 𝜑 → 𝑇 ∈ CRing )
22 3 4 5 6 19 18 7 selvcllem3 ⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
23 1 2 3 4 5 6 14 13 15 7 8 9 selvcllem4 ⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) ) )
24 11 12 13 14 15 17 21 22 23 evlsevl ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) = ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ 𝐹 ) ) )
25 24 fveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
26 10 25 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )