Metamath Proof Explorer


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