Metamath Proof Explorer

Theorem copco

Description: The composition of a concatenation of paths with a continuous function. (Contributed by Mario Carneiro, 9-Jul-2015)

Ref Expression
Hypotheses pcoval.2 ⊢φ→F∈IICnJ
pcoval.3 ⊢φ→G∈IICnJ
pcoval2.4 ⊢φ→F⁡1=G⁡0
copco.6 ⊢φ→H∈JCnK
Assertion copco ⊢φ→H∘F*𝑝⁡JG=H∘F*𝑝⁡KH∘G

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢φ→F∈IICnJ
2 pcoval.3 ⊢φ→G∈IICnJ
3 pcoval2.4 ⊢φ→F⁡1=G⁡0
4 copco.6 ⊢φ→H∈JCnK
5 iiuni ⊢01=⋃II
6 eqid ⊢⋃J=⋃J
7 5 6 cnf ⊢F∈IICnJ→F:01⟶⋃J
8 1 7 syl ⊢φ→F:01⟶⋃J
9 elii1 ⊢x∈012↔x∈01∧x≤12
10 iihalf1 ⊢x∈012→2⁢x∈01
11 9 10 sylbir ⊢x∈01∧x≤12→2⁢x∈01
12 fvco3 ⊢F:01⟶⋃J∧2⁢x∈01→H∘F⁡2⁢x=H⁡F⁡2⁢x
13 8 11 12 syl2an ⊢φ∧x∈01∧x≤12→H∘F⁡2⁢x=H⁡F⁡2⁢x
14 13 anassrs ⊢φ∧x∈01∧x≤12→H∘F⁡2⁢x=H⁡F⁡2⁢x
15 5 6 cnf ⊢G∈IICnJ→G:01⟶⋃J
16 2 15 syl ⊢φ→G:01⟶⋃J
17 elii2 ⊢x∈01∧¬x≤12→x∈121
18 iihalf2 ⊢x∈121→2⁢x−1∈01
19 17 18 syl ⊢x∈01∧¬x≤12→2⁢x−1∈01
20 fvco3 ⊢G:01⟶⋃J∧2⁢x−1∈01→H∘G⁡2⁢x−1=H⁡G⁡2⁢x−1
21 16 19 20 syl2an ⊢φ∧x∈01∧¬x≤12→H∘G⁡2⁢x−1=H⁡G⁡2⁢x−1
22 21 anassrs ⊢φ∧x∈01∧¬x≤12→H∘G⁡2⁢x−1=H⁡G⁡2⁢x−1
23 14 22 ifeq12da ⊢φ∧x∈01→ifx≤12H∘F⁡2⁢xH∘G⁡2⁢x−1=ifx≤12H⁡F⁡2⁢xH⁡G⁡2⁢x−1
24 23 mpteq2dva ⊢φ→x∈01⟼ifx≤12H∘F⁡2⁢xH∘G⁡2⁢x−1=x∈01⟼ifx≤12H⁡F⁡2⁢xH⁡G⁡2⁢x−1
25 cnco ⊢F∈IICnJ∧H∈JCnK→H∘F∈IICnK
26 1 4 25 syl2anc ⊢φ→H∘F∈IICnK
27 cnco ⊢G∈IICnJ∧H∈JCnK→H∘G∈IICnK
28 2 4 27 syl2anc ⊢φ→H∘G∈IICnK
29 26 28 pcoval ⊢φ→H∘F*𝑝⁡KH∘G=x∈01⟼ifx≤12H∘F⁡2⁢xH∘G⁡2⁢x−1
30 1 2 pcoval ⊢φ→F*𝑝⁡JG=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1
31 1 2 3 pcocn ⊢φ→F*𝑝⁡JG∈IICnJ
32 30 31 eqeltrrd ⊢φ→x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1∈IICnJ
33 5 6 cnf ⊢x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1∈IICnJ→x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1:01⟶⋃J
34 32 33 syl ⊢φ→x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1:01⟶⋃J
35 eqid ⊢x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1=x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1
36 35 fmpt ⊢∀x∈01ifx≤12F⁡2⁢xG⁡2⁢x−1∈⋃J↔x∈01⟼ifx≤12F⁡2⁢xG⁡2⁢x−1:01⟶⋃J
37 34 36 sylibr ⊢φ→∀x∈01ifx≤12F⁡2⁢xG⁡2⁢x−1∈⋃J
38 eqid ⊢⋃K=⋃K
39 6 38 cnf ⊢H∈JCnK→H:⋃J⟶⋃K
40 4 39 syl ⊢φ→H:⋃J⟶⋃K
41 40 feqmptd ⊢φ→H=y∈⋃J⟼H⁡y
42 fveq2 ⊢y=ifx≤12F⁡2⁢xG⁡2⁢x−1→H⁡y=H⁡ifx≤12F⁡2⁢xG⁡2⁢x−1
43 fvif ⊢H⁡ifx≤12F⁡2⁢xG⁡2⁢x−1=ifx≤12H⁡F⁡2⁢xH⁡G⁡2⁢x−1
44 42 43 eqtrdi ⊢y=ifx≤12F⁡2⁢xG⁡2⁢x−1→H⁡y=ifx≤12H⁡F⁡2⁢xH⁡G⁡2⁢x−1
45 37 30 41 44 fmptcof ⊢φ→H∘F*𝑝⁡JG=x∈01⟼ifx≤12H⁡F⁡2⁢xH⁡G⁡2⁢x−1
46 24 29 45 3eqtr4rd ⊢φ→H∘F*𝑝⁡JG=H∘F*𝑝⁡KH∘G