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 ⊢ φ → F ∈ II Cn J
pcoval.3 ⊢ φ → G ∈ II Cn J
Assertion pco1 ⊢ φ → F * 𝑝 ⁡ J G ⁡ 1 = G ⁡ 1

Proof

Step Hyp Ref Expression
1 pcoval.2 ⊢ φ → F ∈ II Cn J
2 pcoval.3 ⊢ φ → G ∈ II Cn J
3 1 2 pcoval ⊢ φ → F * 𝑝 ⁡ J G = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1
4 3 fveq1d ⊢ φ → F * 𝑝 ⁡ J G ⁡ 1 = x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 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 ⊢ x = 1 → x ≤ 1 2 ↔ 1 ≤ 1 2
12 10 11 mtbiri ⊢ x = 1 → ¬ x ≤ 1 2
13 12 iffalsed ⊢ x = 1 → if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 = G ⁡ 2 ⁢ x − 1
14 oveq2 ⊢ x = 1 → 2 ⁢ x = 2 ⋅ 1
15 2t1e2 ⊢ 2 ⋅ 1 = 2
16 14 15 eqtrdi ⊢ x = 1 → 2 ⁢ x = 2
17 16 oveq1d ⊢ x = 1 → 2 ⁢ x − 1 = 2 − 1
18 2m1e1 ⊢ 2 − 1 = 1
19 17 18 eqtrdi ⊢ x = 1 → 2 ⁢ x − 1 = 1
20 19 fveq2d ⊢ x = 1 → G ⁡ 2 ⁢ x − 1 = G ⁡ 1
21 13 20 eqtrd ⊢ x = 1 → if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 = G ⁡ 1
22 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
23 fvex ⊢ G ⁡ 1 ∈ V
24 21 22 23 fvmpt ⊢ 1 ∈ 0 1 → x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 ⁡ 1 = G ⁡ 1
25 5 24 ax-mp ⊢ x ∈ 0 1 ⟼ if x ≤ 1 2 F ⁡ 2 ⁢ x G ⁡ 2 ⁢ x − 1 ⁡ 1 = G ⁡ 1
26 4 25 eqtrdi ⊢ φ → F * 𝑝 ⁡ J G ⁡ 1 = G ⁡ 1