Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  selvval Structured version   Visualization version   GIF version

Theorem selvval 20324
 Description: Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
Hypotheses
Ref Expression
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
Ref Expression
selvval (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
Distinct variable groups:   𝑥,𝐼   𝑥,𝑅   𝑥,𝐽   𝑥,𝑈   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐷(𝑥)   𝑃(𝑥)   𝑇(𝑥)   𝐹(𝑥)   𝑉(𝑥)   𝑊(𝑥)

Proof of Theorem selvval
Dummy variables 𝑓 𝑢 𝑡 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 selvval.i . . . 4 (𝜑𝐼𝑉)
2 selvval.r . . . 4 (𝜑𝑅𝑊)
3 selvval.j . . . 4 (𝜑𝐽𝐼)
41, 2, 3selvfval 20323 . . 3 (𝜑 → ((𝐼 selectVars 𝑅)‘𝐽) = (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))))
5 coeq2 5716 . . . . . . . . . 10 (𝑓 = 𝐹 → (𝑑𝑓) = (𝑑𝐹))
65fveq2d 6662 . . . . . . . . 9 (𝑓 = 𝐹 → (((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓)) = (((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹)))
76fveq1d 6660 . . . . . . . 8 (𝑓 = 𝐹 → ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
87csbeq2dv 3873 . . . . . . 7 (𝑓 = 𝐹(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
98csbeq2dv 3873 . . . . . 6 (𝑓 = 𝐹(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
109csbeq2dv 3873 . . . . 5 (𝑓 = 𝐹(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
1110csbeq2dv 3873 . . . 4 (𝑓 = 𝐹((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
1211adantl 485 . . 3 ((𝜑𝑓 = 𝐹) → ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
13 selvval.f . . . 4 (𝜑𝐹𝐵)
14 selvval.b . . . . 5 𝐵 = (Base‘𝑃)
15 selvval.p . . . . . 6 𝑃 = (𝐼 mPoly 𝑅)
1615fveq2i 6661 . . . . 5 (Base‘𝑃) = (Base‘(𝐼 mPoly 𝑅))
1714, 16eqtri 2847 . . . 4 𝐵 = (Base‘(𝐼 mPoly 𝑅))
1813, 17eleqtrdi 2926 . . 3 (𝜑𝐹 ∈ (Base‘(𝐼 mPoly 𝑅)))
19 fvex 6671 . . . . . . . 8 ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) ∈ V
2019csbex 5201 . . . . . . 7 (𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) ∈ V
2120csbex 5201 . . . . . 6 (algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) ∈ V
2221csbex 5201 . . . . 5 (𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) ∈ V
2322csbex 5201 . . . 4 ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) ∈ V
2423a1i 11 . . 3 (𝜑((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) ∈ V)
254, 12, 18, 24fvmptd 6763 . 2 (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
26 ovex 7178 . . 3 ((𝐼𝐽) mPoly 𝑅) ∈ V
27 selvval.u . . . . 5 𝑈 = ((𝐼𝐽) mPoly 𝑅)
2827eqeq2i 2837 . . . 4 (𝑢 = 𝑈𝑢 = ((𝐼𝐽) mPoly 𝑅))
29 oveq2 7153 . . . . . 6 (𝑢 = 𝑈 → (𝐽 mPoly 𝑢) = (𝐽 mPoly 𝑈))
30 fveq2 6658 . . . . . . . . 9 (𝑢 = 𝑈 → (algSc‘𝑢) = (algSc‘𝑈))
3130coeq2d 5720 . . . . . . . 8 (𝑢 = 𝑈 → (𝑐 ∘ (algSc‘𝑢)) = (𝑐 ∘ (algSc‘𝑈)))
32 oveq2 7153 . . . . . . . . . . . 12 (𝑢 = 𝑈 → (𝐽 mVar 𝑢) = (𝐽 mVar 𝑈))
3332fveq1d 6660 . . . . . . . . . . 11 (𝑢 = 𝑈 → ((𝐽 mVar 𝑢)‘𝑥) = ((𝐽 mVar 𝑈)‘𝑥))
3433ifeq1d 4467 . . . . . . . . . 10 (𝑢 = 𝑈 → if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))) = if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))
3534mpteq2dv 5148 . . . . . . . . 9 (𝑢 = 𝑈 → (𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))) = (𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))
3635fveq2d 6662 . . . . . . . 8 (𝑢 = 𝑈 → ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
3731, 36csbeq12dv 3875 . . . . . . 7 (𝑢 = 𝑈(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
3837csbeq2dv 3873 . . . . . 6 (𝑢 = 𝑈(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
3929, 38csbeq12dv 3875 . . . . 5 (𝑢 = 𝑈(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (𝐽 mPoly 𝑈) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
40 ovex 7178 . . . . . 6 (𝐽 mPoly 𝑈) ∈ V
41 selvval.t . . . . . . . 8 𝑇 = (𝐽 mPoly 𝑈)
4241eqeq2i 2837 . . . . . . 7 (𝑡 = 𝑇𝑡 = (𝐽 mPoly 𝑈))
43 fveq2 6658 . . . . . . . . 9 (𝑡 = 𝑇 → (algSc‘𝑡) = (algSc‘𝑇))
44 oveq2 7153 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (𝐼 evalSub 𝑡) = (𝐼 evalSub 𝑇))
4544fveq1d 6660 . . . . . . . . . . . 12 (𝑡 = 𝑇 → ((𝐼 evalSub 𝑡)‘ran 𝑑) = ((𝐼 evalSub 𝑇)‘ran 𝑑))
4645fveq1d 6660 . . . . . . . . . . 11 (𝑡 = 𝑇 → (((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹)) = (((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹)))
4746fveq1d 6660 . . . . . . . . . 10 (𝑡 = 𝑇 → ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
4847csbeq2dv 3873 . . . . . . . . 9 (𝑡 = 𝑇(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
4943, 48csbeq12dv 3875 . . . . . . . 8 (𝑡 = 𝑇(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (algSc‘𝑇) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
50 fvex 6671 . . . . . . . . 9 (algSc‘𝑇) ∈ V
51 selvval.c . . . . . . . . . . 11 𝐶 = (algSc‘𝑇)
5251eqeq2i 2837 . . . . . . . . . 10 (𝑐 = 𝐶𝑐 = (algSc‘𝑇))
53 coeq1 5715 . . . . . . . . . . . 12 (𝑐 = 𝐶 → (𝑐 ∘ (algSc‘𝑈)) = (𝐶 ∘ (algSc‘𝑈)))
54 fveq1 6657 . . . . . . . . . . . . . . 15 (𝑐 = 𝐶 → (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)) = (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))
5554ifeq2d 4468 . . . . . . . . . . . . . 14 (𝑐 = 𝐶 → if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))) = if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))
5655mpteq2dv 5148 . . . . . . . . . . . . 13 (𝑐 = 𝐶 → (𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))) = (𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))
5756fveq2d 6662 . . . . . . . . . . . 12 (𝑐 = 𝐶 → ((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
5853, 57csbeq12dv 3875 . . . . . . . . . . 11 (𝑐 = 𝐶(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = (𝐶 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
5951fvexi 6672 . . . . . . . . . . . . 13 𝐶 ∈ V
60 fvex 6671 . . . . . . . . . . . . 13 (algSc‘𝑈) ∈ V
6159, 60coex 7625 . . . . . . . . . . . 12 (𝐶 ∘ (algSc‘𝑈)) ∈ V
62 selvval.d . . . . . . . . . . . . . 14 𝐷 = (𝐶 ∘ (algSc‘𝑈))
6362eqeq2i 2837 . . . . . . . . . . . . 13 (𝑑 = 𝐷𝑑 = (𝐶 ∘ (algSc‘𝑈)))
64 rneq 5793 . . . . . . . . . . . . . . . 16 (𝑑 = 𝐷 → ran 𝑑 = ran 𝐷)
6564fveq2d 6662 . . . . . . . . . . . . . . 15 (𝑑 = 𝐷 → ((𝐼 evalSub 𝑇)‘ran 𝑑) = ((𝐼 evalSub 𝑇)‘ran 𝐷))
66 coeq1 5715 . . . . . . . . . . . . . . 15 (𝑑 = 𝐷 → (𝑑𝐹) = (𝐷𝐹))
6765, 66fveq12d 6665 . . . . . . . . . . . . . 14 (𝑑 = 𝐷 → (((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹)) = (((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹)))
6867fveq1d 6660 . . . . . . . . . . . . 13 (𝑑 = 𝐷 → ((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
6963, 68sylbir 238 . . . . . . . . . . . 12 (𝑑 = (𝐶 ∘ (algSc‘𝑈)) → ((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
7061, 69csbie 3901 . . . . . . . . . . 11 (𝐶 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))
7158, 70syl6eq 2875 . . . . . . . . . 10 (𝑐 = 𝐶(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
7252, 71sylbir 238 . . . . . . . . 9 (𝑐 = (algSc‘𝑇) → (𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
7350, 72csbie 3901 . . . . . . . 8 (algSc‘𝑇) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑇)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))
7449, 73syl6eq 2875 . . . . . . 7 (𝑡 = 𝑇(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
7542, 74sylbir 238 . . . . . 6 (𝑡 = (𝐽 mPoly 𝑈) → (algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
7640, 75csbie 3901 . . . . 5 (𝐽 mPoly 𝑈) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑈)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))
7739, 76syl6eq 2875 . . . 4 (𝑢 = 𝑈(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
7828, 77sylbir 238 . . 3 (𝑢 = ((𝐼𝐽) mPoly 𝑅) → (𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
7926, 78csbie 3901 . 2 ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))
8025, 79syl6eq 2875 1 (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = ((((𝐼 evalSub 𝑇)‘ran 𝐷)‘(𝐷𝐹))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑈)‘𝑥), (𝐶‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2115  Vcvv 3480  ⦋csb 3866   ∖ cdif 3916   ⊆ wss 3919  ifcif 4449   ↦ cmpt 5132  ran crn 5543   ∘ ccom 5546  ‘cfv 6343  (class class class)co 7145  Basecbs 16479  algSccascl 20077   mVar cmvr 20125   mPoly cmpl 20126   evalSub ces 20277   selectVars cslv 20314 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-ov 7148  df-oprab 7149  df-mpo 7150  df-selv 20318 This theorem is referenced by:  selvcl  39310
 Copyright terms: Public domain W3C validator