Metamath Proof Explorer


Theorem lineid

Description: Identity law for points on lines. Theorem 4.18 of Schwabhauser p. 38. (Contributed by Scott Fenton, 7-Oct-2013)

Ref Expression
Assertion lineid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B A Colinear B C A C Cgr A D B C Cgr B D C = D

Proof

Step Hyp Ref Expression
1 simp2l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A 𝔼 N
2 simp2r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N B 𝔼 N
3 simp3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N C 𝔼 N
4 1 2 3 3jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A 𝔼 N B 𝔼 N C 𝔼 N
5 linecgr N A 𝔼 N B 𝔼 N C 𝔼 N C 𝔼 N D 𝔼 N A B A Colinear B C A C Cgr A D B C Cgr B D C C Cgr C D
6 4 5 syld3an2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B A Colinear B C A C Cgr A D B C Cgr B D C C Cgr C D
7 simp1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N N
8 simp3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N D 𝔼 N
9 cgrid2 N C 𝔼 N C 𝔼 N D 𝔼 N C C Cgr C D C = D
10 7 3 3 8 9 syl13anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N C C Cgr C D C = D
11 6 10 syld N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B A Colinear B C A C Cgr A D B C Cgr B D C = D