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