Metamath Proof Explorer

Theorem selvval

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

Ref Expression
Hypotheses selvval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
selvval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
selvval.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
selvval.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
selvval.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
selvval.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
selvval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
selvval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
selvval.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
selvval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion selvval ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 selvval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 selvval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 selvval.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
4 selvval.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
5 selvval.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
6 selvval.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
7 selvval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8 selvval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
9 selvval.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
10 selvval.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
11 7 8 9 selvfval ⊢ ( 𝜑 → ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) = ( 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ↦ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
12 coeq2 ⊢ ( 𝑓 = 𝐹 → ( 𝑑 ∘ 𝑓 ) = ( 𝑑 ∘ 𝐹 ) )
13 12 fveq2d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) = ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) )
14 13 fveq1d ⊢ ( 𝑓 = 𝐹 → ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
15 14 csbeq2dv ⊢ ( 𝑓 = 𝐹 → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
16 15 csbeq2dv ⊢ ( 𝑓 = 𝐹 → ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
17 16 csbeq2dv ⊢ ( 𝑓 = 𝐹 → ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
18 17 csbeq2dv ⊢ ( 𝑓 = 𝐹 → ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝑓 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
20 1 fveq2i ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
21 2 20 eqtri ⊢ 𝐵 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
22 10 21 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
23 fvex ⊢ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ V
24 23 csbex ⊢ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ V
25 24 csbex ⊢ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ V
26 25 csbex ⊢ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ V
27 26 csbex ⊢ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ V
28 27 a1i ⊢ ( 𝜑 → ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∈ V )
29 11 19 22 28 fvmptd ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
30 ovex ⊢ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) ∈ V
31 3 eqeq2i ⊢ ( 𝑢 = 𝑈 ↔ 𝑢 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) )
32 oveq2 ⊢ ( 𝑢 = 𝑈 → ( 𝐽 mPoly 𝑢 ) = ( 𝐽 mPoly 𝑈 ) )
33 fveq2 ⊢ ( 𝑢 = 𝑈 → ( algSc ‘ 𝑢 ) = ( algSc ‘ 𝑈 ) )
34 33 coeq2d ⊢ ( 𝑢 = 𝑈 → ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) = ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) )
35 oveq2 ⊢ ( 𝑢 = 𝑈 → ( 𝐽 mVar 𝑢 ) = ( 𝐽 mVar 𝑈 ) )
36 35 fveq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) = ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) )
37 36 ifeq1d ⊢ ( 𝑢 = 𝑈 → if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) = if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
38 37 mpteq2dv ⊢ ( 𝑢 = 𝑈 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
39 38 fveq2d ⊢ ( 𝑢 = 𝑈 → ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
40 34 39 csbeq12dv ⊢ ( 𝑢 = 𝑈 → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
41 40 csbeq2dv ⊢ ( 𝑢 = 𝑈 → ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
42 32 41 csbeq12dv ⊢ ( 𝑢 = 𝑈 → ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐽 mPoly 𝑈 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
43 ovex ⊢ ( 𝐽 mPoly 𝑈 ) ∈ V
44 4 eqeq2i ⊢ ( 𝑡 = 𝑇 ↔ 𝑡 = ( 𝐽 mPoly 𝑈 ) )
45 fveq2 ⊢ ( 𝑡 = 𝑇 → ( algSc ‘ 𝑡 ) = ( algSc ‘ 𝑇 ) )
46 oveq2 ⊢ ( 𝑡 = 𝑇 → ( 𝐼 evalSub 𝑡 ) = ( 𝐼 evalSub 𝑇 ) )
47 46 fveq1d ⊢ ( 𝑡 = 𝑇 → ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) )
48 47 fveq1d ⊢ ( 𝑡 = 𝑇 → ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) = ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) )
49 48 fveq1d ⊢ ( 𝑡 = 𝑇 → ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
50 49 csbeq2dv ⊢ ( 𝑡 = 𝑇 → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
51 45 50 csbeq12dv ⊢ ( 𝑡 = 𝑇 → ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( algSc ‘ 𝑇 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
52 fvex ⊢ ( algSc ‘ 𝑇 ) ∈ V
53 5 eqeq2i ⊢ ( 𝑐 = 𝐶 ↔ 𝑐 = ( algSc ‘ 𝑇 ) )
54 coeq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) )
55 fveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) = ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) )
56 55 ifeq2d ⊢ ( 𝑐 = 𝐶 → if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) = if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
57 56 mpteq2dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
58 57 fveq2d ⊢ ( 𝑐 = 𝐶 → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
59 54 58 csbeq12dv ⊢ ( 𝑐 = 𝐶 → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
60 5 fvexi ⊢ 𝐶 ∈ V
61 fvex ⊢ ( algSc ‘ 𝑈 ) ∈ V
62 60 61 coex ⊢ ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ∈ V
63 6 eqeq2i ⊢ ( 𝑑 = 𝐷 ↔ 𝑑 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) )
64 rneq ⊢ ( 𝑑 = 𝐷 → ran 𝑑 = ran 𝐷 )
65 64 fveq2d ⊢ ( 𝑑 = 𝐷 → ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) )
66 coeq1 ⊢ ( 𝑑 = 𝐷 → ( 𝑑 ∘ 𝐹 ) = ( 𝐷 ∘ 𝐹 ) )
67 65 66 fveq12d ⊢ ( 𝑑 = 𝐷 → ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) = ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) )
68 67 fveq1d ⊢ ( 𝑑 = 𝐷 → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
69 63 68 sylbir ⊢ ( 𝑑 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) → ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
70 62 69 csbie ⊢ ⦋ ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
71 59 70 eqtrdi ⊢ ( 𝑐 = 𝐶 → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
72 53 71 sylbir ⊢ ( 𝑐 = ( algSc ‘ 𝑇 ) → ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
73 52 72 csbie ⊢ ⦋ ( algSc ‘ 𝑇 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
74 51 73 eqtrdi ⊢ ( 𝑡 = 𝑇 → ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
75 44 74 sylbir ⊢ ( 𝑡 = ( 𝐽 mPoly 𝑈 ) → ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
76 43 75 csbie ⊢ ⦋ ( 𝐽 mPoly 𝑈 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑈 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
77 42 76 eqtrdi ⊢ ( 𝑢 = 𝑈 → ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
78 31 77 sylbir ⊢ ( 𝑢 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) → ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
79 30 78 csbie ⊢ ⦋ ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 ) / 𝑢 ⦌ ⦋ ( 𝐽 mPoly 𝑢 ) / 𝑡 ⦌ ⦋ ( algSc ‘ 𝑡 ) / 𝑐 ⦌ ⦋ ( 𝑐 ∘ ( algSc ‘ 𝑢 ) ) / 𝑑 ⦌ ( ( ( ( 𝐼 evalSub 𝑡 ) ‘ ran 𝑑 ) ‘ ( 𝑑 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑢 ) ‘ 𝑥 ) , ( 𝑐 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) )
80 29 79 eqtrdi ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 ) ‘ ( 𝐷 ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )