tglngval

Description: The line going through points X and Y . (Contributed by Thierry Arnoux, 28-Mar-2019)

	Ref	Expression
Hypotheses	tglngval.p	$⊢ P = {Base}_{G}$
	tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
	tglngval.i	$⊢ I = Itv (G)$
	tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglngval.x	$⊢ φ \to X \in P$
	tglngval.y	$⊢ φ \to Y \in P$
	tglngval.z	$⊢ φ \to X \neq Y$
Assertion	tglngval	$⊢ φ \to X L Y = \{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		tglngval.p	$⊢ P = {Base}_{G}$
2		tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
3		tglngval.i	$⊢ I = Itv (G)$
4		tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglngval.x	$⊢ φ \to X \in P$
6		tglngval.y	$⊢ φ \to Y \in P$
7		tglngval.z	$⊢ φ \to X \neq Y$
8	1 2 3	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))\})$
9	4 8	syl	$⊢ φ \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))\})$
10	9	oveqd	$⊢ φ \to X L Y = X (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))\}) Y$
11	7	necomd	$⊢ φ \to Y \neq X$
12		eldifsn	$⊢ Y \in (P ∖ \{X\}) \leftrightarrow (Y \in P \land Y \neq X)$
13	6 11 12	sylanbrc	$⊢ φ \to Y \in (P ∖ \{X\})$
14	1	fvexi	$⊢ P \in V$
15	14	rabex	$⊢ \{z \in P \| (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))\} \in V$
16	15	a1i	$⊢ φ \to \{z \in P \| (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))\} \in V$
17		oveq12	$⊢ (x = X \land y = Y) \to x I y = X I Y$
18	17	eleq2d	$⊢ (x = X \land y = Y) \to (z \in (x I y) \leftrightarrow z \in (X I Y))$
19		simpl	$⊢ (x = X \land y = Y) \to x = X$
20		simpr	$⊢ (x = X \land y = Y) \to y = Y$
21	20	oveq2d	$⊢ (x = X \land y = Y) \to z I y = z I Y$
22	19 21	eleq12d	$⊢ (x = X \land y = Y) \to (x \in (z I y) \leftrightarrow X \in (z I Y))$
23	19	oveq1d	$⊢ (x = X \land y = Y) \to x I z = X I z$
24	20 23	eleq12d	$⊢ (x = X \land y = Y) \to (y \in (x I z) \leftrightarrow Y \in (X I z))$
25	18 22 24	3orbi123d	$⊢ (x = X \land y = Y) \to ((z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z)))$
26	25	rabbidv	$⊢ (x = X \land y = Y) \to \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} = \{z \in P \| (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))\}$
27		sneq	$⊢ x = X \to \{x\} = \{X\}$
28	27	difeq2d	$⊢ x = X \to P ∖ \{x\} = P ∖ \{X\}$
29		eqid	$⊢ (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))\}) = (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))\})$
30	26 28 29	ovmpox	$⊢ (X \in P \land Y \in (P ∖ \{X\}) \land \{z \in P \| (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))\} \in V) \to X (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))\}) Y = \{z \in P \| (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))\}$
31	5 13 16 30	syl3anc	$⊢ φ \to X (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))\}) Y = \{z \in P \| (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))\}$
32	10 31	eqtrd	$⊢ φ \to X L Y = \{z \in P \| (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))\}$

Metamath Proof Explorer

Theorem tglngval

Proof