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

Theorem fcompt 6882
 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.)
Assertion
Ref Expression
fcompt ((𝐴:𝐷𝐸𝐵:𝐶𝐷) → (𝐴𝐵) = (𝑥𝐶 ↦ (𝐴‘(𝐵𝑥))))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐷   𝑥,𝐸

Proof of Theorem fcompt
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ffvelrn 6836 . . 3 ((𝐵:𝐶𝐷𝑥𝐶) → (𝐵𝑥) ∈ 𝐷)
21adantll 713 . 2 (((𝐴:𝐷𝐸𝐵:𝐶𝐷) ∧ 𝑥𝐶) → (𝐵𝑥) ∈ 𝐷)
3 ffn 6495 . . . 4 (𝐵:𝐶𝐷𝐵 Fn 𝐶)
43adantl 485 . . 3 ((𝐴:𝐷𝐸𝐵:𝐶𝐷) → 𝐵 Fn 𝐶)
5 dffn5 6709 . . 3 (𝐵 Fn 𝐶𝐵 = (𝑥𝐶 ↦ (𝐵𝑥)))
64, 5sylib 221 . 2 ((𝐴:𝐷𝐸𝐵:𝐶𝐷) → 𝐵 = (𝑥𝐶 ↦ (𝐵𝑥)))
7 ffn 6495 . . . 4 (𝐴:𝐷𝐸𝐴 Fn 𝐷)
87adantr 484 . . 3 ((𝐴:𝐷𝐸𝐵:𝐶𝐷) → 𝐴 Fn 𝐷)
9 dffn5 6709 . . 3 (𝐴 Fn 𝐷𝐴 = (𝑦𝐷 ↦ (𝐴𝑦)))
108, 9sylib 221 . 2 ((𝐴:𝐷𝐸𝐵:𝐶𝐷) → 𝐴 = (𝑦𝐷 ↦ (𝐴𝑦)))
11 fveq2 6655 . 2 (𝑦 = (𝐵𝑥) → (𝐴𝑦) = (𝐴‘(𝐵𝑥)))
122, 6, 10, 11fmptco 6878 1 ((𝐴:𝐷𝐸𝐵:𝐶𝐷) → (𝐴𝐵) = (𝑥𝐶 ↦ (𝐴‘(𝐵𝑥))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ↦ cmpt 5114   ∘ ccom 5527   Fn wfn 6327  ⟶wf 6328  ‘cfv 6332 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-fv 6340 This theorem is referenced by:  2fvcoidd  7041  revco  14207  repsco  14213  caucvgrlem2  15043  fucidcl  17247  fucsect  17254  prf1st  17466  prf2nd  17467  curfcl  17494  yonedalem4c  17539  yonedalem3b  17541  yonedainv  17543  frmdup3  18044  smndex1gid  18080  efginvrel1  18867  frgpup3lem  18916  frgpup3  18917  dprdfinv  19155  grpvlinv  21043  grpvrinv  21044  mhmvlin  21045  chcoeffeqlem  21531  prdstps  22275  imasdsf1olem  23021  gamcvg2lem  25688  cofmpt2  30437  meascnbl  31654  elmrsubrn  32946  mzprename  39861  mendassa  40309  fcomptss  42002  mulc1cncfg  42399  expcnfg  42401  cncficcgt0  42698  fprodsubrecnncnvlem  42717  fprodaddrecnncnvlem  42719  dvsinax  42723  dirkercncflem2  42914  fourierdlem18  42935  fourierdlem53  42969  fourierdlem93  43009  fourierdlem101  43017  fourierdlem111  43027  sge0resrnlem  43210  omeiunle  43324  ovolval3  43454  amgmwlem  45496
 Copyright terms: Public domain W3C validator