Theorem selvfval

Description: Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023)

	Ref	Expression
Hypotheses	selvffval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvffval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	selvfval.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
Assertion	selvfval	⊢ ( 𝜑 → ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) = ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		selvffval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
2		selvffval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
3		selvfval.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
4	1 2	selvffval	⊢ ( 𝜑 → ( 𝐼 selectVars 𝑅 ) = ( 𝑗 ∈ 𝒫 𝐼 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ) )
5		difeq2	⊢ ( 𝑗 = 𝐽 → ( 𝐼 ∖ 𝑗 ) = ( 𝐼 ∖ 𝐽 ) )
6	5	oveq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) )
7		oveq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 mPoly 𝑢 ) = ( 𝐽 mPoly 𝑢 ) )
8		eleq2	⊢ ( 𝑗 = 𝐽 → ( 𝑥 ∈ 𝑗 ↔ 𝑥 ∈ 𝐽 ) )
9		oveq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 mVar 𝑢 ) = ( 𝐽 mVar 𝑢 ) )
10	9	fveq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) = ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) )
11	5	oveq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) = ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) )
12	11	fveq1d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) = ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) )
13	12	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) = ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) )
14	8 10 13	ifbieq12d	⊢ ( 𝑗 = 𝐽 → if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) = if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
15	14	mpteq2dv	⊢ ( 𝑗 = 𝐽 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
16	15	fveq2d	⊢ ( 𝑗 = 𝐽 → ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
17	16	csbeq2dv	⊢ ( 𝑗 = 𝐽 → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
18	17	csbeq2dv	⊢ ( 𝑗 = 𝐽 → ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
19	7 18	csbeq12dv	⊢ ( 𝑗 = 𝐽 → ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
20	6 19	csbeq12dv	⊢ ( 𝑗 = 𝐽 → ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
21	20	mpteq2dv	⊢ ( 𝑗 = 𝐽 → ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) = ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
22	21	adantl	⊢ ( ( 𝜑 ∧ 𝑗 = 𝐽 ) → ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) = ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
23	1 3	sselpwd	⊢ ( 𝜑 → 𝐽 ∈ 𝒫 𝐼 )
24		fvex	⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∈ V
25		mptexg	⊢ ( ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∈ V → ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ∈ V )
26	24 25	mp1i	⊢ ( 𝜑 → ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ∈ V )
27	4 22 23 26	fvmptd	⊢ ( 𝜑 → ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) = ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )