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 ∈ II Cn J
pcoval.3 ⊢ φ → G ∈ II Cn J
pcoval2.4 ⊢ φ → F ⁡ 1 = G ⁡ 0
copco.6 ⊢ φ → H ∈ J Cn K
Assertion copco ⊢ φ → H ∘ F * 𝑝 ⁡ J G = H ∘ F * 𝑝 ⁡ K H ∘ G

Proof

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