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

Theorem selvfval 20873
 Description: Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.)
Hypotheses
Ref Expression
selvffval.i (𝜑𝐼𝑉)
selvffval.r (𝜑𝑅𝑊)
selvfval.j (𝜑𝐽𝐼)
Assertion
Ref Expression
selvfval (𝜑 → ((𝐼 selectVars 𝑅)‘𝐽) = (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))))
Distinct variable groups:   𝑓,𝐼,𝑢,𝑡,𝑐,𝑑,𝑥   𝑅,𝑓,𝑢,𝑡,𝑐,𝑑,𝑥   𝑓,𝐽,𝑢,𝑡,𝑐,𝑑,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑢,𝑡,𝑓,𝑐,𝑑)   𝑉(𝑥,𝑢,𝑡,𝑓,𝑐,𝑑)   𝑊(𝑥,𝑢,𝑡,𝑓,𝑐,𝑑)

Proof of Theorem selvfval
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 selvffval.i . . 3 (𝜑𝐼𝑉)
2 selvffval.r . . 3 (𝜑𝑅𝑊)
31, 2selvffval 20872 . 2 (𝜑 → (𝐼 selectVars 𝑅) = (𝑗 ∈ 𝒫 𝐼 ↦ (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝑗) mPoly 𝑅) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥))))))))
4 difeq2 4023 . . . . . 6 (𝑗 = 𝐽 → (𝐼𝑗) = (𝐼𝐽))
54oveq1d 7166 . . . . 5 (𝑗 = 𝐽 → ((𝐼𝑗) mPoly 𝑅) = ((𝐼𝐽) mPoly 𝑅))
6 oveq1 7158 . . . . . 6 (𝑗 = 𝐽 → (𝑗 mPoly 𝑢) = (𝐽 mPoly 𝑢))
7 eleq2 2841 . . . . . . . . . . 11 (𝑗 = 𝐽 → (𝑥𝑗𝑥𝐽))
8 oveq1 7158 . . . . . . . . . . . 12 (𝑗 = 𝐽 → (𝑗 mVar 𝑢) = (𝐽 mVar 𝑢))
98fveq1d 6661 . . . . . . . . . . 11 (𝑗 = 𝐽 → ((𝑗 mVar 𝑢)‘𝑥) = ((𝐽 mVar 𝑢)‘𝑥))
104oveq1d 7166 . . . . . . . . . . . . 13 (𝑗 = 𝐽 → ((𝐼𝑗) mVar 𝑅) = ((𝐼𝐽) mVar 𝑅))
1110fveq1d 6661 . . . . . . . . . . . 12 (𝑗 = 𝐽 → (((𝐼𝑗) mVar 𝑅)‘𝑥) = (((𝐼𝐽) mVar 𝑅)‘𝑥))
1211fveq2d 6663 . . . . . . . . . . 11 (𝑗 = 𝐽 → (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥)) = (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))
137, 9, 12ifbieq12d 4449 . . . . . . . . . 10 (𝑗 = 𝐽 → if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥))) = if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))
1413mpteq2dv 5129 . . . . . . . . 9 (𝑗 = 𝐽 → (𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥)))) = (𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))
1514fveq2d 6663 . . . . . . . 8 (𝑗 = 𝐽 → ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥))))) = ((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
1615csbeq2dv 3813 . . . . . . 7 (𝑗 = 𝐽(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥))))) = (𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
1716csbeq2dv 3813 . . . . . 6 (𝑗 = 𝐽(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥))))) = (algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
186, 17csbeq12dv 3815 . . . . 5 (𝑗 = 𝐽(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥))))) = (𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
195, 18csbeq12dv 3815 . . . 4 (𝑗 = 𝐽((𝐼𝑗) mPoly 𝑅) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥))))) = ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥))))))
2019mpteq2dv 5129 . . 3 (𝑗 = 𝐽 → (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝑗) mPoly 𝑅) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥)))))) = (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))))
2120adantl 486 . 2 ((𝜑𝑗 = 𝐽) → (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝑗) mPoly 𝑅) / 𝑢(𝑗 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝑗, ((𝑗 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝑗) mVar 𝑅)‘𝑥)))))) = (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))))
22 selvfval.j . . 3 (𝜑𝐽𝐼)
231, 22sselpwd 5197 . 2 (𝜑𝐽 ∈ 𝒫 𝐼)
24 fvex 6672 . . 3 (Base‘(𝐼 mPoly 𝑅)) ∈ V
25 mptexg 6976 . . 3 ((Base‘(𝐼 mPoly 𝑅)) ∈ V → (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))) ∈ V)
2624, 25mp1i 13 . 2 (𝜑 → (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))) ∈ V)
273, 21, 23, 26fvmptd 6767 1 (𝜑 → ((𝐼 selectVars 𝑅)‘𝐽) = (𝑓 ∈ (Base‘(𝐼 mPoly 𝑅)) ↦ ((𝐼𝐽) mPoly 𝑅) / 𝑢(𝐽 mPoly 𝑢) / 𝑡(algSc‘𝑡) / 𝑐(𝑐 ∘ (algSc‘𝑢)) / 𝑑((((𝐼 evalSub 𝑡)‘ran 𝑑)‘(𝑑𝑓))‘(𝑥𝐼 ↦ if(𝑥𝐽, ((𝐽 mVar 𝑢)‘𝑥), (𝑐‘(((𝐼𝐽) mVar 𝑅)‘𝑥)))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  Vcvv 3410  ⦋csb 3806   ∖ cdif 3856   ⊆ wss 3859  ifcif 4421  𝒫 cpw 4495   ↦ cmpt 5113  ran crn 5526   ∘ ccom 5529  ‘cfv 6336  (class class class)co 7151  Basecbs 16534  algSccascl 20610   mVar cmvr 20660   mPoly cmpl 20661   evalSub ces 20826   selectVars cslv 20864 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-selv 20868 This theorem is referenced by:  selvval  20874
 Copyright terms: Public domain W3C validator