Theorem lnid

Description: Identity law for points on lines. Theorem 4.18 of Schwabhauser p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019)

	Ref	Expression
Hypotheses	tglngval.p	$$⊢P={\mathrm{Base}}_G$$
	tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tglngval.x	$$⊢\phi \to X\in P$$
	tglngval.y	$$⊢\phi \to Y\in P$$
	tgcolg.z	$$⊢\phi \to Z\in P$$
	lnxfr.r	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
	lnxfr.a	$$⊢\phi \to A\in P$$
	lnxfr.b	$$⊢\phi \to B\in P$$
	lnxfr.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	lnid.1	$$⊢\phi \to X\ne Y$$
	lnid.2	$$⊢\phi \to \left(Y\in \left(XLZ\right)\vee X=Z\right)$$
	lnid.3	$$⊢\phi \to X\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}A$$
	lnid.4	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}A$$
Assertion	lnid	$$⊢\phi \to Z=A$$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$$⊢P={\mathrm{Base}}_G$$
2		tglngval.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		tglngval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tglngval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tglngval.x	$$⊢\phi \to X\in P$$
6		tglngval.y	$$⊢\phi \to Y\in P$$
7		tgcolg.z	$$⊢\phi \to Z\in P$$
8		lnxfr.r	$$⊢\underset{\dot{}}{\sim }={\sim }_{𝒢}\left(G\right)$$
9		lnxfr.a	$$⊢\phi \to A\in P$$
10		lnxfr.b	$$⊢\phi \to B\in P$$
11		lnxfr.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
12		lnid.1	$$⊢\phi \to X\ne Y$$
13		lnid.2	$$⊢\phi \to \left(Y\in \left(XLZ\right)\vee X=Z\right)$$
14		lnid.3	$$⊢\phi \to X\underset{\dot{}}{-}Z=X\underset{\dot{}}{-}A$$
15		lnid.4	$$⊢\phi \to Y\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}A$$
16	1 2 3 4 5 6 7 8 7 9 11 12 13 14 15	lncgr	$$⊢\phi \to Z\underset{\dot{}}{-}Z=Z\underset{\dot{}}{-}A$$
17	16	eqcomd	$$⊢\phi \to Z\underset{\dot{}}{-}A=Z\underset{\dot{}}{-}Z$$
18	1 11 3 4 7 9 7 17	axtgcgrid	$$⊢\phi \to Z=A$$