Metamath Proof Explorer


Theorem pco1

Description: The ending point of a path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010)

Ref Expression
Hypotheses pcoval.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
pcoval.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
Assertion pco1 ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 1 ) = ( 𝐺 ‘ 1 ) )

Proof

Step Hyp Ref Expression
1 pcoval.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 pcoval.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 1 2 pcoval ( 𝜑 → ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) )
4 3 fveq1d ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 1 ) = ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ‘ 1 ) )
5 1elunit 1 ∈ ( 0 [,] 1 )
6 halflt1 ( 1 / 2 ) < 1
7 halfre ( 1 / 2 ) ∈ ℝ
8 1re 1 ∈ ℝ
9 7 8 ltnlei ( ( 1 / 2 ) < 1 ↔ ¬ 1 ≤ ( 1 / 2 ) )
10 6 9 mpbi ¬ 1 ≤ ( 1 / 2 )
11 breq1 ( 𝑥 = 1 → ( 𝑥 ≤ ( 1 / 2 ) ↔ 1 ≤ ( 1 / 2 ) ) )
12 10 11 mtbiri ( 𝑥 = 1 → ¬ 𝑥 ≤ ( 1 / 2 ) )
13 12 iffalsed ( 𝑥 = 1 → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) )
14 oveq2 ( 𝑥 = 1 → ( 2 · 𝑥 ) = ( 2 · 1 ) )
15 2t1e2 ( 2 · 1 ) = 2
16 14 15 eqtrdi ( 𝑥 = 1 → ( 2 · 𝑥 ) = 2 )
17 16 oveq1d ( 𝑥 = 1 → ( ( 2 · 𝑥 ) − 1 ) = ( 2 − 1 ) )
18 2m1e1 ( 2 − 1 ) = 1
19 17 18 eqtrdi ( 𝑥 = 1 → ( ( 2 · 𝑥 ) − 1 ) = 1 )
20 19 fveq2d ( 𝑥 = 1 → ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) = ( 𝐺 ‘ 1 ) )
21 13 20 eqtrd ( 𝑥 = 1 → if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) = ( 𝐺 ‘ 1 ) )
22 eqid ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) )
23 fvex ( 𝐺 ‘ 1 ) ∈ V
24 21 22 23 fvmpt ( 1 ∈ ( 0 [,] 1 ) → ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ‘ 1 ) = ( 𝐺 ‘ 1 ) )
25 5 24 ax-mp ( ( 𝑥 ∈ ( 0 [,] 1 ) ↦ if ( 𝑥 ≤ ( 1 / 2 ) , ( 𝐹 ‘ ( 2 · 𝑥 ) ) , ( 𝐺 ‘ ( ( 2 · 𝑥 ) − 1 ) ) ) ) ‘ 1 ) = ( 𝐺 ‘ 1 )
26 4 25 eqtrdi ( 𝜑 → ( ( 𝐹 ( *𝑝𝐽 ) 𝐺 ) ‘ 1 ) = ( 𝐺 ‘ 1 ) )