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

Theorem phtpyco2 23595
 Description: Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.)
Hypotheses
Ref Expression
phtpyco2.f (𝜑𝐹 ∈ (II Cn 𝐽))
phtpyco2.g (𝜑𝐺 ∈ (II Cn 𝐽))
phtpyco2.p (𝜑𝑃 ∈ (𝐽 Cn 𝐾))
phtpyco2.h (𝜑𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))
Assertion
Ref Expression
phtpyco2 (𝜑 → (𝑃𝐻) ∈ ((𝑃𝐹)(PHtpy‘𝐾)(𝑃𝐺)))

Proof of Theorem phtpyco2
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 phtpyco2.f . . 3 (𝜑𝐹 ∈ (II Cn 𝐽))
2 phtpyco2.p . . 3 (𝜑𝑃 ∈ (𝐽 Cn 𝐾))
3 cnco 21871 . . 3 ((𝐹 ∈ (II Cn 𝐽) ∧ 𝑃 ∈ (𝐽 Cn 𝐾)) → (𝑃𝐹) ∈ (II Cn 𝐾))
41, 2, 3syl2anc 587 . 2 (𝜑 → (𝑃𝐹) ∈ (II Cn 𝐾))
5 phtpyco2.g . . 3 (𝜑𝐺 ∈ (II Cn 𝐽))
6 cnco 21871 . . 3 ((𝐺 ∈ (II Cn 𝐽) ∧ 𝑃 ∈ (𝐽 Cn 𝐾)) → (𝑃𝐺) ∈ (II Cn 𝐾))
75, 2, 6syl2anc 587 . 2 (𝜑 → (𝑃𝐺) ∈ (II Cn 𝐾))
81, 5phtpyhtpy 23587 . . . 4 (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺))
9 phtpyco2.h . . . 4 (𝜑𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺))
108, 9sseldd 3916 . . 3 (𝜑𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺))
111, 5, 2, 10htpyco2 23584 . 2 (𝜑 → (𝑃𝐻) ∈ ((𝑃𝐹)(II Htpy 𝐾)(𝑃𝐺)))
121, 5, 9phtpyi 23589 . . . . 5 ((𝜑𝑠 ∈ (0[,]1)) → ((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1)))
1312simpld 498 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘0))
1413fveq2d 6649 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (𝑃‘(0𝐻𝑠)) = (𝑃‘(𝐹‘0)))
15 iitopon 23484 . . . . . . 7 II ∈ (TopOn‘(0[,]1))
16 txtopon 22196 . . . . . . 7 ((II ∈ (TopOn‘(0[,]1)) ∧ II ∈ (TopOn‘(0[,]1))) → (II ×t II) ∈ (TopOn‘((0[,]1) × (0[,]1))))
1715, 15, 16mp2an 691 . . . . . 6 (II ×t II) ∈ (TopOn‘((0[,]1) × (0[,]1)))
18 cntop2 21846 . . . . . . . 8 (𝐹 ∈ (II Cn 𝐽) → 𝐽 ∈ Top)
191, 18syl 17 . . . . . . 7 (𝜑𝐽 ∈ Top)
20 toptopon2 21523 . . . . . . 7 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
2119, 20sylib 221 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘ 𝐽))
221, 5phtpycn 23588 . . . . . . 7 (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ ((II ×t II) Cn 𝐽))
2322, 9sseldd 3916 . . . . . 6 (𝜑𝐻 ∈ ((II ×t II) Cn 𝐽))
24 cnf2 21854 . . . . . 6 (((II ×t II) ∈ (TopOn‘((0[,]1) × (0[,]1))) ∧ 𝐽 ∈ (TopOn‘ 𝐽) ∧ 𝐻 ∈ ((II ×t II) Cn 𝐽)) → 𝐻:((0[,]1) × (0[,]1))⟶ 𝐽)
2517, 21, 23, 24mp3an2i 1463 . . . . 5 (𝜑𝐻:((0[,]1) × (0[,]1))⟶ 𝐽)
26 0elunit 12847 . . . . . 6 0 ∈ (0[,]1)
27 simpr 488 . . . . . 6 ((𝜑𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1))
28 opelxpi 5556 . . . . . 6 ((0 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ⟨0, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
2926, 27, 28sylancr 590 . . . . 5 ((𝜑𝑠 ∈ (0[,]1)) → ⟨0, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
30 fvco3 6737 . . . . 5 ((𝐻:((0[,]1) × (0[,]1))⟶ 𝐽 ∧ ⟨0, 𝑠⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝑃𝐻)‘⟨0, 𝑠⟩) = (𝑃‘(𝐻‘⟨0, 𝑠⟩)))
3125, 29, 30syl2an2r 684 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → ((𝑃𝐻)‘⟨0, 𝑠⟩) = (𝑃‘(𝐻‘⟨0, 𝑠⟩)))
32 df-ov 7138 . . . 4 (0(𝑃𝐻)𝑠) = ((𝑃𝐻)‘⟨0, 𝑠⟩)
33 df-ov 7138 . . . . 5 (0𝐻𝑠) = (𝐻‘⟨0, 𝑠⟩)
3433fveq2i 6648 . . . 4 (𝑃‘(0𝐻𝑠)) = (𝑃‘(𝐻‘⟨0, 𝑠⟩))
3531, 32, 343eqtr4g 2858 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (0(𝑃𝐻)𝑠) = (𝑃‘(0𝐻𝑠)))
36 iiuni 23486 . . . . . . 7 (0[,]1) = II
37 eqid 2798 . . . . . . 7 𝐽 = 𝐽
3836, 37cnf 21851 . . . . . 6 (𝐹 ∈ (II Cn 𝐽) → 𝐹:(0[,]1)⟶ 𝐽)
391, 38syl 17 . . . . 5 (𝜑𝐹:(0[,]1)⟶ 𝐽)
4039adantr 484 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → 𝐹:(0[,]1)⟶ 𝐽)
41 fvco3 6737 . . . 4 ((𝐹:(0[,]1)⟶ 𝐽 ∧ 0 ∈ (0[,]1)) → ((𝑃𝐹)‘0) = (𝑃‘(𝐹‘0)))
4240, 26, 41sylancl 589 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → ((𝑃𝐹)‘0) = (𝑃‘(𝐹‘0)))
4314, 35, 423eqtr4d 2843 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (0(𝑃𝐻)𝑠) = ((𝑃𝐹)‘0))
4412simprd 499 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘1))
4544fveq2d 6649 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (𝑃‘(1𝐻𝑠)) = (𝑃‘(𝐹‘1)))
46 1elunit 12848 . . . . . 6 1 ∈ (0[,]1)
47 opelxpi 5556 . . . . . 6 ((1 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ⟨1, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
4846, 27, 47sylancr 590 . . . . 5 ((𝜑𝑠 ∈ (0[,]1)) → ⟨1, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
49 fvco3 6737 . . . . 5 ((𝐻:((0[,]1) × (0[,]1))⟶ 𝐽 ∧ ⟨1, 𝑠⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝑃𝐻)‘⟨1, 𝑠⟩) = (𝑃‘(𝐻‘⟨1, 𝑠⟩)))
5025, 48, 49syl2an2r 684 . . . 4 ((𝜑𝑠 ∈ (0[,]1)) → ((𝑃𝐻)‘⟨1, 𝑠⟩) = (𝑃‘(𝐻‘⟨1, 𝑠⟩)))
51 df-ov 7138 . . . 4 (1(𝑃𝐻)𝑠) = ((𝑃𝐻)‘⟨1, 𝑠⟩)
52 df-ov 7138 . . . . 5 (1𝐻𝑠) = (𝐻‘⟨1, 𝑠⟩)
5352fveq2i 6648 . . . 4 (𝑃‘(1𝐻𝑠)) = (𝑃‘(𝐻‘⟨1, 𝑠⟩))
5450, 51, 533eqtr4g 2858 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → (1(𝑃𝐻)𝑠) = (𝑃‘(1𝐻𝑠)))
55 fvco3 6737 . . . 4 ((𝐹:(0[,]1)⟶ 𝐽 ∧ 1 ∈ (0[,]1)) → ((𝑃𝐹)‘1) = (𝑃‘(𝐹‘1)))
5640, 46, 55sylancl 589 . . 3 ((𝜑𝑠 ∈ (0[,]1)) → ((𝑃𝐹)‘1) = (𝑃‘(𝐹‘1)))
5745, 54, 563eqtr4d 2843 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (1(𝑃𝐻)𝑠) = ((𝑃𝐹)‘1))
584, 7, 11, 43, 57isphtpyd 23591 1 (𝜑 → (𝑃𝐻) ∈ ((𝑃𝐹)(PHtpy‘𝐾)(𝑃𝐺)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ⟨cop 4531  ∪ cuni 4800   × cxp 5517   ∘ ccom 5523  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  0cc0 10526  1c1 10527  [,]cicc 12729  Topctop 21498  TopOnctopon 21515   Cn ccn 21829   ×t ctx 22165  IIcii 23480   Htpy chtpy 23572  PHtpycphtpy 23573 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-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  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-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-sup 8890  df-inf 8891  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-icc 12733  df-seq 13365  df-exp 13426  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-topgen 16709  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-top 21499  df-topon 21516  df-bases 21551  df-cn 21832  df-tx 22167  df-ii 23482  df-htpy 23575  df-phtpy 23576 This theorem is referenced by:  phtpcco2  23604
 Copyright terms: Public domain W3C validator