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 𝑅 ) ‘ 𝑥 ) ) ) ) ) )