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 NA𝔼NB𝔼NC𝔼ND𝔼NABAColinearBCACCgrADBCCgrBDC=D

Proof

Step Hyp Ref Expression
1 simp2l NA𝔼NB𝔼NC𝔼ND𝔼NA𝔼N
2 simp2r NA𝔼NB𝔼NC𝔼ND𝔼NB𝔼N
3 simp3l NA𝔼NB𝔼NC𝔼ND𝔼NC𝔼N
4 1 2 3 3jca NA𝔼NB𝔼NC𝔼ND𝔼NA𝔼NB𝔼NC𝔼N
5 linecgr NA𝔼NB𝔼NC𝔼NC𝔼ND𝔼NABAColinearBCACCgrADBCCgrBDCCCgrCD
6 4 5 syld3an2 NA𝔼NB𝔼NC𝔼ND𝔼NABAColinearBCACCgrADBCCgrBDCCCgrCD
7 simp1 NA𝔼NB𝔼NC𝔼ND𝔼NN
8 simp3r NA𝔼NB𝔼NC𝔼ND𝔼ND𝔼N
9 cgrid2 NC𝔼NC𝔼ND𝔼NCCCgrCDC=D
10 7 3 3 8 9 syl13anc NA𝔼NB𝔼NC𝔼ND𝔼NCCCgrCDC=D
11 6 10 syld NA𝔼NB𝔼NC𝔼ND𝔼NABAColinearBCACCgrADBCCgrBDC=D