Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ofval | Structured version Visualization version GIF version |
Description: Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) |
Ref | Expression |
---|---|
offval.1 | ⊢ (𝜑 → 𝐹 Fn 𝐴) |
offval.2 | ⊢ (𝜑 → 𝐺 Fn 𝐵) |
offval.3 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
offval.4 | ⊢ (𝜑 → 𝐵 ∈ 𝑊) |
offval.5 | ⊢ (𝐴 ∩ 𝐵) = 𝑆 |
ofval.6 | ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) |
ofval.7 | ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) |
Ref | Expression |
---|---|
ofval | ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | offval.1 | . . . . 5 ⊢ (𝜑 → 𝐹 Fn 𝐴) | |
2 | offval.2 | . . . . 5 ⊢ (𝜑 → 𝐺 Fn 𝐵) | |
3 | offval.3 | . . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
4 | offval.4 | . . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
5 | offval.5 | . . . . 5 ⊢ (𝐴 ∩ 𝐵) = 𝑆 | |
6 | eqidd 2825 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) | |
7 | eqidd 2825 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐺‘𝑥) = (𝐺‘𝑥)) | |
8 | 1, 2, 3, 4, 5, 6, 7 | offval 7419 | . . . 4 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))) |
9 | 8 | fveq1d 6675 | . . 3 ⊢ (𝜑 → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋)) |
10 | 9 | adantr 483 | . 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋)) |
11 | fveq2 6673 | . . . . 5 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) | |
12 | fveq2 6673 | . . . . 5 ⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋)) | |
13 | 11, 12 | oveq12d 7177 | . . . 4 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥)𝑅(𝐺‘𝑥)) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) |
14 | eqid 2824 | . . . 4 ⊢ (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥))) | |
15 | ovex 7192 | . . . 4 ⊢ ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) ∈ V | |
16 | 13, 14, 15 | fvmpt 6771 | . . 3 ⊢ (𝑋 ∈ 𝑆 → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) |
17 | 16 | adantl 484 | . 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑥)𝑅(𝐺‘𝑥)))‘𝑋) = ((𝐹‘𝑋)𝑅(𝐺‘𝑋))) |
18 | inss1 4208 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
19 | 5, 18 | eqsstrri 4005 | . . . . 5 ⊢ 𝑆 ⊆ 𝐴 |
20 | 19 | sseli 3966 | . . . 4 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐴) |
21 | ofval.6 | . . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐶) | |
22 | 20, 21 | sylan2 594 | . . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) = 𝐶) |
23 | inss2 4209 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | |
24 | 5, 23 | eqsstrri 4005 | . . . . 5 ⊢ 𝑆 ⊆ 𝐵 |
25 | 24 | sseli 3966 | . . . 4 ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵) |
26 | ofval.7 | . . . 4 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (𝐺‘𝑋) = 𝐷) | |
27 | 25, 26 | sylan2 594 | . . 3 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝐺‘𝑋) = 𝐷) |
28 | 22, 27 | oveq12d 7177 | . 2 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹‘𝑋)𝑅(𝐺‘𝑋)) = (𝐶𝑅𝐷)) |
29 | 10, 17, 28 | 3eqtrd 2863 | 1 ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → ((𝐹 ∘f 𝑅𝐺)‘𝑋) = (𝐶𝑅𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1536 ∈ wcel 2113 ∩ cin 3938 ↦ cmpt 5149 Fn wfn 6353 ‘cfv 6358 (class class class)co 7159 ∘f cof 7410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pr 5333 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-ral 3146 df-rex 3147 df-reu 3148 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-id 5463 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-ov 7162 df-oprab 7163 df-mpo 7164 df-of 7412 |
This theorem is referenced by: fnfvof 7426 offveq 7433 ofc1 7435 ofc2 7436 suppofss1d 7871 suppofss2d 7872 ofsubeq0 11638 ofnegsub 11639 ofsubge0 11640 seqof 13430 o1of2 14972 gsumzaddlem 19044 psrbagcon 20154 psrbagconf1o 20157 psrdi 20189 psrdir 20190 mplsubglem 20217 matplusgcell 21045 matsubgcell 21046 rrxcph 23998 mbfaddlem 24264 i1faddlem 24297 i1fmullem 24298 itg1lea 24316 mbfi1flimlem 24326 itg2split 24353 itg2monolem1 24354 itg2addlem 24362 dvaddbr 24538 dvmulbr 24539 plyaddlem1 24806 coeeulem 24817 coeaddlem 24842 dgradd2 24861 dgrcolem2 24867 ofmulrt 24874 plydivlem3 24887 plydivlem4 24888 plydiveu 24890 plyrem 24897 vieta1lem2 24903 elqaalem3 24913 qaa 24915 basellem7 25667 basellem9 25669 circlemethhgt 31918 poimirlem1 34897 poimirlem2 34898 poimirlem6 34902 poimirlem7 34903 poimirlem10 34906 poimirlem11 34907 poimirlem12 34908 poimirlem17 34913 poimirlem20 34916 poimirlem23 34919 poimirlem29 34925 poimirlem31 34927 poimirlem32 34928 broucube 34930 itg2addnclem3 34949 itg2addnc 34950 ftc1anclem5 34975 lfladdcl 36211 ldualvaddval 36271 dgrsub2 39741 mpaaeu 39756 caofcan 40661 ofmul12 40663 ofdivrec 40664 ofdivcan4 40665 ofdivdiv2 40666 binomcxplemrat 40688 binomcxplemnotnn0 40694 mndpsuppss 44426 amgmwlem 44910 |
Copyright terms: Public domain | W3C validator |