Metamath Proof Explorer


Theorem pco0

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

Ref Expression
Hypotheses pcoval.2 φFIICnJ
pcoval.3 φGIICnJ
Assertion pco0 φF*𝑝JG0=F0

Proof

Step Hyp Ref Expression
1 pcoval.2 φFIICnJ
2 pcoval.3 φGIICnJ
3 0re 0
4 0le0 00
5 halfge0 012
6 halfre 12
7 3 6 elicc2i 0012000012
8 3 4 5 7 mpbir3an 0012
9 1 2 pcoval1 φ0012F*𝑝JG0=F20
10 8 9 mpan2 φF*𝑝JG0=F20
11 2t0e0 20=0
12 11 fveq2i F20=F0
13 10 12 eqtrdi φF*𝑝JG0=F0