Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fcores Structured version   Visualization version   GIF version

Theorem fcores 47079
Description: Every composite function (𝐺𝐹) can be written as composition of restrictions of the composed functions (to their minimum domains). (Contributed by GL and AV, 17-Sep-2024.)
Hypotheses
Ref Expression
fcores.f (𝜑𝐹:𝐴𝐵)
fcores.e 𝐸 = (ran 𝐹𝐶)
fcores.p 𝑃 = (𝐹𝐶)
fcores.x 𝑋 = (𝐹𝑃)
fcores.g (𝜑𝐺:𝐶𝐷)
fcores.y 𝑌 = (𝐺𝐸)
Assertion
Ref Expression
fcores (𝜑 → (𝐺𝐹) = (𝑌𝑋))

Proof of Theorem fcores
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fcores.g . . . . 5 (𝜑𝐺:𝐶𝐷)
2 fcores.f . . . . . 6 (𝜑𝐹:𝐴𝐵)
32ffund 6740 . . . . 5 (𝜑 → Fun 𝐹)
4 fcof 6759 . . . . 5 ((𝐺:𝐶𝐷 ∧ Fun 𝐹) → (𝐺𝐹):(𝐹𝐶)⟶𝐷)
51, 3, 4syl2anc 584 . . . 4 (𝜑 → (𝐺𝐹):(𝐹𝐶)⟶𝐷)
65ffnd 6737 . . 3 (𝜑 → (𝐺𝐹) Fn (𝐹𝐶))
7 fcores.p . . . 4 𝑃 = (𝐹𝐶)
87fneq2i 6666 . . 3 ((𝐺𝐹) Fn 𝑃 ↔ (𝐺𝐹) Fn (𝐹𝐶))
96, 8sylibr 234 . 2 (𝜑 → (𝐺𝐹) Fn 𝑃)
10 fcores.e . . 3 𝐸 = (ran 𝐹𝐶)
11 fcores.x . . 3 𝑋 = (𝐹𝑃)
12 fcores.y . . 3 𝑌 = (𝐺𝐸)
132, 10, 7, 11, 1, 12fcoreslem4 47078 . 2 (𝜑 → (𝑌𝑋) Fn 𝑃)
1411fveq1i 6907 . . . . . 6 (𝑋𝑥) = ((𝐹𝑃)‘𝑥)
15 simpr 484 . . . . . . 7 ((𝜑𝑥𝑃) → 𝑥𝑃)
1615fvresd 6926 . . . . . 6 ((𝜑𝑥𝑃) → ((𝐹𝑃)‘𝑥) = (𝐹𝑥))
1714, 16eqtrid 2789 . . . . 5 ((𝜑𝑥𝑃) → (𝑋𝑥) = (𝐹𝑥))
1817fveq2d 6910 . . . 4 ((𝜑𝑥𝑃) → (𝑌‘(𝑋𝑥)) = (𝑌‘(𝐹𝑥)))
1912fveq1i 6907 . . . . 5 (𝑌‘(𝐹𝑥)) = ((𝐺𝐸)‘(𝐹𝑥))
20 cnvimass 6100 . . . . . . . . . . 11 (𝐹𝐶) ⊆ dom 𝐹
217, 20eqsstri 4030 . . . . . . . . . 10 𝑃 ⊆ dom 𝐹
2221sseli 3979 . . . . . . . . 9 (𝑥𝑃𝑥 ∈ dom 𝐹)
23 fvelrn 7096 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ran 𝐹)
243, 22, 23syl2an 596 . . . . . . . 8 ((𝜑𝑥𝑃) → (𝐹𝑥) ∈ ran 𝐹)
257eleq2i 2833 . . . . . . . . . 10 (𝑥𝑃𝑥 ∈ (𝐹𝐶))
2625biimpi 216 . . . . . . . . 9 (𝑥𝑃𝑥 ∈ (𝐹𝐶))
27 fvimacnvi 7072 . . . . . . . . 9 ((Fun 𝐹𝑥 ∈ (𝐹𝐶)) → (𝐹𝑥) ∈ 𝐶)
283, 26, 27syl2an 596 . . . . . . . 8 ((𝜑𝑥𝑃) → (𝐹𝑥) ∈ 𝐶)
2924, 28elind 4200 . . . . . . 7 ((𝜑𝑥𝑃) → (𝐹𝑥) ∈ (ran 𝐹𝐶))
3029, 10eleqtrrdi 2852 . . . . . 6 ((𝜑𝑥𝑃) → (𝐹𝑥) ∈ 𝐸)
3130fvresd 6926 . . . . 5 ((𝜑𝑥𝑃) → ((𝐺𝐸)‘(𝐹𝑥)) = (𝐺‘(𝐹𝑥)))
3219, 31eqtrid 2789 . . . 4 ((𝜑𝑥𝑃) → (𝑌‘(𝐹𝑥)) = (𝐺‘(𝐹𝑥)))
3318, 32eqtrd 2777 . . 3 ((𝜑𝑥𝑃) → (𝑌‘(𝑋𝑥)) = (𝐺‘(𝐹𝑥)))
342, 10, 7, 11fcoreslem3 47077 . . . . . 6 (𝜑𝑋:𝑃onto𝐸)
35 fof 6820 . . . . . 6 (𝑋:𝑃onto𝐸𝑋:𝑃𝐸)
3634, 35syl 17 . . . . 5 (𝜑𝑋:𝑃𝐸)
3736adantr 480 . . . 4 ((𝜑𝑥𝑃) → 𝑋:𝑃𝐸)
3837, 15fvco3d 7009 . . 3 ((𝜑𝑥𝑃) → ((𝑌𝑋)‘𝑥) = (𝑌‘(𝑋𝑥)))
392adantr 480 . . . 4 ((𝜑𝑥𝑃) → 𝐹:𝐴𝐵)
4021a1i 11 . . . . . 6 (𝜑𝑃 ⊆ dom 𝐹)
4140sselda 3983 . . . . 5 ((𝜑𝑥𝑃) → 𝑥 ∈ dom 𝐹)
422fdmd 6746 . . . . . . . 8 (𝜑 → dom 𝐹 = 𝐴)
4342eqcomd 2743 . . . . . . 7 (𝜑𝐴 = dom 𝐹)
4443eleq2d 2827 . . . . . 6 (𝜑 → (𝑥𝐴𝑥 ∈ dom 𝐹))
4544adantr 480 . . . . 5 ((𝜑𝑥𝑃) → (𝑥𝐴𝑥 ∈ dom 𝐹))
4641, 45mpbird 257 . . . 4 ((𝜑𝑥𝑃) → 𝑥𝐴)
4739, 46fvco3d 7009 . . 3 ((𝜑𝑥𝑃) → ((𝐺𝐹)‘𝑥) = (𝐺‘(𝐹𝑥)))
4833, 38, 473eqtr4rd 2788 . 2 ((𝜑𝑥𝑃) → ((𝐺𝐹)‘𝑥) = ((𝑌𝑋)‘𝑥))
499, 13, 48eqfnfvd 7054 1 (𝜑 → (𝐺𝐹) = (𝑌𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  cin 3950  wss 3951  ccnv 5684  dom cdm 5685  ran crn 5686  cres 5687  cima 5688  ccom 5689  Fun wfun 6555   Fn wfn 6556  wf 6557  ontowfo 6559  cfv 6561
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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fo 6567  df-fv 6569
This theorem is referenced by:  fcoresf1lem  47080  fcoresf1b  47082  fcoresfo  47083  fcoresfob  47084
  Copyright terms: Public domain W3C validator