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 φ F II Cn J
pcoval.3 φ G II Cn J
Assertion pco0 φ F * 𝑝 J G 0 = F 0

Proof

Step Hyp Ref Expression
1 pcoval.2 φ F II Cn J
2 pcoval.3 φ G II Cn J
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 F * 𝑝 J G 0 = F 2 0
10 8 9 mpan2 φ F * 𝑝 J G 0 = F 2 0
11 2t0e0 2 0 = 0
12 11 fveq2i F 2 0 = F 0
13 10 12 eqtrdi φ F * 𝑝 J G 0 = F 0