Theorem pco0

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

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

Proof

Step	Hyp	Ref	Expression
1		pcoval.2	⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2		pcoval.3	⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3		0re	⊢ 0 ∈ ℝ
4		0le0	⊢ 0 ≤ 0
5		halfge0	⊢ 0 ≤ ( 1 / 2 )
6		halfre	⊢ ( 1 / 2 ) ∈ ℝ
7	3 6	elicc2i	⊢ ( 0 ∈ ( 0 [,] ( 1 / 2 ) ) ↔ ( 0 ∈ ℝ ∧ 0 ≤ 0 ∧ 0 ≤ ( 1 / 2 ) ) )
8	3 4 5 7	mpbir3an	⊢ 0 ∈ ( 0 [,] ( 1 / 2 ) )
9	1 2	pcoval1	⊢ ( ( 𝜑 ∧ 0 ∈ ( 0 [,] ( 1 / 2 ) ) ) → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) = ( 𝐹 ‘ ( 2 · 0 ) ) )
10	8 9	mpan2	⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) = ( 𝐹 ‘ ( 2 · 0 ) ) )
11		2t0e0	⊢ ( 2 · 0 ) = 0
12	11	fveq2i	⊢ ( 𝐹 ‘ ( 2 · 0 ) ) = ( 𝐹 ‘ 0 )
13	10 12	eqtrdi	⊢ ( 𝜑 → ( ( 𝐹 ( *𝑝 ‘ 𝐽 ) 𝐺 ) ‘ 0 ) = ( 𝐹 ‘ 0 ) )