MPE Home 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