Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fcompt | Structured version Visualization version GIF version |
Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |
Ref | Expression |
---|---|
fcompt | ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffvelcdm 7015 | . . 3 ⊢ ((𝐵:𝐶⟶𝐷 ∧ 𝑥 ∈ 𝐶) → (𝐵‘𝑥) ∈ 𝐷) | |
2 | 1 | adantll 711 | . 2 ⊢ (((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) ∧ 𝑥 ∈ 𝐶) → (𝐵‘𝑥) ∈ 𝐷) |
3 | ffn 6651 | . . . 4 ⊢ (𝐵:𝐶⟶𝐷 → 𝐵 Fn 𝐶) | |
4 | 3 | adantl 482 | . . 3 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐵 Fn 𝐶) |
5 | dffn5 6884 | . . 3 ⊢ (𝐵 Fn 𝐶 ↔ 𝐵 = (𝑥 ∈ 𝐶 ↦ (𝐵‘𝑥))) | |
6 | 4, 5 | sylib 217 | . 2 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐵 = (𝑥 ∈ 𝐶 ↦ (𝐵‘𝑥))) |
7 | ffn 6651 | . . . 4 ⊢ (𝐴:𝐷⟶𝐸 → 𝐴 Fn 𝐷) | |
8 | 7 | adantr 481 | . . 3 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐴 Fn 𝐷) |
9 | dffn5 6884 | . . 3 ⊢ (𝐴 Fn 𝐷 ↔ 𝐴 = (𝑦 ∈ 𝐷 ↦ (𝐴‘𝑦))) | |
10 | 8, 9 | sylib 217 | . 2 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → 𝐴 = (𝑦 ∈ 𝐷 ↦ (𝐴‘𝑦))) |
11 | fveq2 6825 | . 2 ⊢ (𝑦 = (𝐵‘𝑥) → (𝐴‘𝑦) = (𝐴‘(𝐵‘𝑥))) | |
12 | 2, 6, 10, 11 | fmptco 7057 | 1 ⊢ ((𝐴:𝐷⟶𝐸 ∧ 𝐵:𝐶⟶𝐷) → (𝐴 ∘ 𝐵) = (𝑥 ∈ 𝐶 ↦ (𝐴‘(𝐵‘𝑥)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ↦ cmpt 5175 ∘ ccom 5624 Fn wfn 6474 ⟶wf 6475 ‘cfv 6479 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5243 ax-nul 5250 ax-pr 5372 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-fv 6487 |
This theorem is referenced by: 2fvcoidd 7225 revco 14646 repsco 14652 caucvgrlem2 15485 fucidcl 17780 fucsect 17787 dfinito3 17817 dftermo3 17818 prf1st 18018 prf2nd 18019 curfcl 18047 yonedalem4c 18092 yonedalem3b 18094 yonedainv 18096 frmdup3 18602 smndex1gid 18638 efginvrel1 19429 frgpup3lem 19478 frgpup3 19479 dprdfinv 19717 grpvlinv 21650 grpvrinv 21651 mhmvlin 21652 chcoeffeqlem 22140 prdstps 22886 imasdsf1olem 23632 gamcvg2lem 26314 cofmpt2 31256 meascnbl 32485 elmrsubrn 33781 mzprename 40841 mendassa 41290 fcomptss 43078 mulc1cncfg 43474 expcnfg 43476 cncficcgt0 43773 fprodsubrecnncnvlem 43792 fprodaddrecnncnvlem 43794 dvsinax 43798 dirkercncflem2 43989 fourierdlem18 44010 fourierdlem53 44044 fourierdlem93 44084 fourierdlem101 44092 fourierdlem111 44102 sge0resrnlem 44286 omeiunle 44400 ovolval3 44530 amgmwlem 46865 |
Copyright terms: Public domain | W3C validator |