Metamath Proof Explorer

Theorem selvffval

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

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

Proof

Step Hyp Ref Expression
1 selvffval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
2 selvffval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
3 df-selv ⊢ selectVars = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ⦋ ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) ) ) )
4 3 a1i ⊢ ( 𝜑 → selectVars = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ⦋ ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) ) ) ) )
5 pweq ⊢ ( 𝑖 = 𝐼 → 𝒫 𝑖 = 𝒫 𝐼 )
6 5 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝒫 𝑖 = 𝒫 𝐼 )
7 oveq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPoly 𝑟 ) = ( 𝐼 mPoly 𝑅 ) )
8 7 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
9 difeq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∖ 𝑗 ) = ( 𝐼 ∖ 𝑗 ) )
10 9 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 ∖ 𝑗 ) = ( 𝐼 ∖ 𝑗 ) )
11 simpr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
12 10 11 oveq12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) = ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) )
13 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 evalSub 𝑡 ) = ( 𝐼 evalSub 𝑡 ) )
14 13 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 evalSub 𝑡 ) = ( 𝐼 evalSub 𝑡 ) )
15 14 fveq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) = ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) )
16 15 fveq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) = ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) )
17 simpl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → 𝑖 = 𝐼 )
18 10 11 oveq12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) = ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) )
19 18 fveq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) = ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) )
20 19 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) = ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) )
21 20 ifeq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) = if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
22 17 21 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
23 16 22 fveq12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
24 23 csbeq2dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
25 24 csbeq2dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
26 25 csbeq2dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
27 12 26 csbeq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ⦋ ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
28 8 27 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ⦋ ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) ) = ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
29 6 28 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ⦋ ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) ) ) = ( 𝑗 ∈ 𝒫 𝐼 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) ) → ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ↦ ⦋ ( ( 𝑖 ∖ 𝑗 ) mPoly 𝑟 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝑖 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝑖 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝑖 ∖ 𝑗 ) mVar 𝑟 ) ‘ 𝑥 ) ) ) ) ) ) ) = ( 𝑗 ∈ 𝒫 𝐼 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ) )
31 1 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
32 2 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
33 1 pwexd ⊢ ( 𝜑 → 𝒫 𝐼 ∈ V )
34 33 mptexd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝒫 𝐼 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ) ∈ V )
35 4 30 31 32 34 ovmpod ⊢ ( 𝜑 → ( 𝐼 selectVars 𝑅 ) = ( 𝑗 ∈ 𝒫 𝐼 ↦ ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝑗 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝑗 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑗 , ( ( 𝑗 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝑗 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ) )