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 ) )