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 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
pcoval.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
pcoval2.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
copco.6 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion copco ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ( *𝑝 ‘ 𝐾 ) ( 𝐻 ∘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2 pcoval.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3 pcoval2.4 ⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 0 ) )
4 copco.6 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐽 Cn 𝐾 ) )
5 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 5 6 cnf ⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐹 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
8 1 7 syl ⊢ ( 𝜑 → 𝐹 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
9 elii1 ⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) )
10 iihalf1 ⊢ ( 𝑥 ∈ ( 0 [,] ( 1 / 2 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
11 9 10 sylbir ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) )
12 fvco3 ⊢ ( ( 𝐹 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 ∧ ( 2 · 𝑥 ) ∈ ( 0 [,] 1 ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ ( 2 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) )
13 8 11 12 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑥 ≤ ( 1 / 2 ) ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ ( 2 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) )
14 13 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ ( 2 · 𝑥 ) ) = ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) )
15 5 6 cnf ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → 𝐺 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
16 2 15 syl ⊢ ( 𝜑 → 𝐺 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
17 elii2 ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) )
18 iihalf2 ⊢ ( 𝑥 ∈ ( ( 1 / 2 ) [,] 1 ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) )
19 17 18 syl ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) )
20 fvco3 ⊢ ( ( 𝐺 : ( 0 [,] 1 ) ⟶ ∪ 𝐽 ∧ ( ( 2 · 𝑥 ) − 1 ) ∈ ( 0 [,] 1 ) ) → ( ( 𝐻 ∘ 𝐺 ) ‘ ( ( 2 · 𝑥 ) − 1 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
21 16 19 20 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) ) → ( ( 𝐻 ∘ 𝐺 ) ‘ ( ( 2 · 𝑥 ) − 1 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
22 21 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) ∧ ¬ 𝑥 ≤ ( 1 / 2 ) ) → ( ( 𝐻 ∘ 𝐺 ) ‘ ( ( 2 · 𝑥 ) − 1 ) ) = ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
23 14 22 ifeq12da ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐻 ∘ 𝐹 ) ‘ ( 2 · 𝑥 ) ) , ( ( 𝐻 ∘ 𝐺 ) ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) , ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
24 23 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐻 ∘ 𝐹 ) ‘ ( 2 · 𝑥 ) ) , ( ( 𝐻 ∘ 𝐺 ) ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) , ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )
25 cnco ⊢ ( ( 𝐹 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐻 ∘ 𝐹 ) ∈ ( II Cn 𝐾 ) )
26 1 4 25 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( II Cn 𝐾 ) )
27 cnco ⊢ ( ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐻 ∘ 𝐺 ) ∈ ( II Cn 𝐾 ) )
28 2 4 27 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) ∈ ( II Cn 𝐾 ) )
29 26 28 pcoval ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ( *𝑝 ‘ 𝐾 ) ( 𝐻 ∘ 𝐺 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( ( 𝐻 ∘ 𝐹 ) ‘ ( 2 · 𝑥 ) ) , ( ( 𝐻 ∘ 𝐺 ) ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
30 1 2 pcoval ⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
31 1 2 3 pcocn ⊢ ( 𝜑 → ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ∈ ( II Cn 𝐽 ) )
32 30 31 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ∈ ( II Cn 𝐽 ) )
33 5 6 cnf ⊢ ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ∈ ( II Cn 𝐽 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
34 32 33 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
35 eqid ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
36 35 fmpt ⊢ ( ∀ 𝑥 ∈ ( 0 [,] 1 ) if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ∈ ∪ 𝐽 ↔ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) : ( 0 [,] 1 ) ⟶ ∪ 𝐽 )
37 34 36 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 [,] 1 ) if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ∈ ∪ 𝐽 )
38 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
39 6 38 cnf ⊢ ( 𝐻 ∈ ( 𝐽 Cn 𝐾 ) → 𝐻 : ∪ 𝐽 ⟶ ∪ 𝐾 )
40 4 39 syl ⊢ ( 𝜑 → 𝐻 : ∪ 𝐽 ⟶ ∪ 𝐾 )
41 40 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑦 ∈ ∪ 𝐽 ↦ ( 𝐻 ‘ 𝑦 ) ) )
42 fveq2 ⊢ ( 𝑦 = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
43 fvif ⊢ ( 𝐻 ‘ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) , ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
44 42 43 eqtrdi ⊢ ( 𝑦 = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) → ( 𝐻 ‘ 𝑦 ) = if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) , ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
45 37 30 41 44 fmptcof ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐻 ‘ ( 𝐹 ‘ ( 2 · 𝑥 ) ) ) , ( 𝐻 ‘ ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ) )
46 24 29 45 3eqtr4rd ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ( *𝑝 ‘ 𝐾 ) ( 𝐻 ∘ 𝐺 ) ) )