Metamath Proof Explorer

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 = {Base}_{G}$
		tglng.l	$⊢ L = {Line}_{𝒢} (G)$
		tglng.i	$⊢ I = Itv (G)$
	Assertion	tglng	$⊢ G \in 𝒢_{Tarski} \to L = (x \in P, y \in (P ∖ \{x\}) ⟼ \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$

Proof

Step	Hyp	Ref	Expression
1		tglng.p	$⊢ P = {Base}_{G}$
2		tglng.l	$⊢ L = {Line}_{𝒢} (G)$
3		tglng.i	$⊢ I = Itv (G)$
4		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
5		inss2	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
6		inss2	$⊢ 𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \subseteq \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
7	5 6	sstri	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
8	4 7	eqsstri	$⊢ 𝒢_{Tarski} \subseteq \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
9	8	sseli	$⊢ G \in 𝒢_{Tarski} \to G \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
10		eqid	$⊢ dist (G) = dist (G)$
11	1 10 3	istrkgl	$⊢ G \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \leftrightarrow (G \in V \land {Line}_{𝒢} (G) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}))$
12	11	simprbi	$⊢ G \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \to {Line}_{𝒢} (G) = (x \in P, y \in (P ∖ \{x\}) ⟼ \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
13	2 12	eqtrid	$⊢ G \in \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \to L = (x \in P, y \in (P ∖ \{x\}) ⟼ \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$
14	9 13	syl	$⊢ G \in 𝒢_{Tarski} \to L = (x \in P, y \in (P ∖ \{x\}) ⟼ \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})$