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.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
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.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8 selvval2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 selvval2.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
10 selvval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
11 1 2 3 4 5 6 7 8 9 10 selvval ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
12 eqid ⊢ ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 )
13 eqid ⊢ ( 𝐼 eval 𝑇 ) = ( 𝐼 eval 𝑇 )
14 eqid ⊢ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) = ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) )
15 eqid ⊢ ( 𝑇 ↾s ran 𝐷 ) = ( 𝑇 ↾s ran 𝐷 )
16 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) )
17 7 9 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
18 7 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
19 3 18 8 mplcrngd ⊢ ( 𝜑 → 𝑈 ∈ CRing )
20 4 17 19 mplcrngd ⊢ ( 𝜑 → 𝑇 ∈ CRing )
21 3 4 5 6 18 17 8 selvcllem3 ⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
22 1 2 3 4 5 6 15 14 16 7 8 9 10 selvcllem4 ⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑇 ↾s ran 𝐷 ) ) ) )
23 12 13 14 15 16 7 20 21 22 evlsevl ⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) = ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ 𝐹 ) ) )
24 23 fveq1d ⊢ ( 𝜑 → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
25 11 24 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )