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