Theorem tglng

Description: Lines of a Tarski Geometry. This relates to both Definition 4.10 of Schwabhauser p. 36. and Definition 6.14 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 28-Mar-2019)

	Ref	Expression
Hypotheses	tglng.p	$$⊢P={\mathrm{Base}}_G$$
	tglng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	tglng.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
Assertion	tglng	$$⊢G\in {𝒢}_{\mathrm{Tarski}}\to L=\left(x\in P,y\in \left(P\setminus \left\{x\right\}\right)⟼\left\{z\in P|\left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tglng.p	$$⊢P={\mathrm{Base}}_G$$
2		tglng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
3		tglng.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		df-trkg	$$⊢{𝒢}_{\mathrm{Tarski}}=\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)$$
5		inss2	$$⊢\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)\subseteq {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}$$
6		inss2	$$⊢{𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\subseteq \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}$$
7	5 6	sstri	$$⊢\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)\subseteq \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}$$
8	4 7	eqsstri	$$⊢{𝒢}_{\mathrm{Tarski}}\subseteq \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}$$
9	8	sseli	$$⊢G\in {𝒢}_{\mathrm{Tarski}}\to G\in \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}$$
10		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
11	1 10 3	istrkgl	$$⊢G\in \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\leftrightarrow \left(G\in \mathrm{V}\wedge {Line}_{𝒢}\left(G\right)=\left(x\in P,y\in \left(P\setminus \left\{x\right\}\right)⟼\left\{z\in P|\left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right\}\right)\right)$$
12	11	simprbi	$$⊢G\in \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\to {Line}_{𝒢}\left(G\right)=\left(x\in P,y\in \left(P\setminus \left\{x\right\}\right)⟼\left\{z\in P|\left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right\}\right)$$
13	2 12	eqtrid	$$⊢G\in \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\to L=\left(x\in P,y\in \left(P\setminus \left\{x\right\}\right)⟼\left\{z\in P|\left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right\}\right)$$
14	9 13	syl	$$⊢G\in {𝒢}_{\mathrm{Tarski}}\to L=\left(x\in P,y\in \left(P\setminus \left\{x\right\}\right)⟼\left\{z\in P|\left(z\in \left(xIy\right)\vee x\in \left(zIy\right)\vee y\in \left(xIz\right)\right)\right\}\right)$$