elntg

Description: The line definition in the Tarski structure for the Euclidean geometry. (Contributed by Thierry Arnoux, 7-Apr-2019)

	Ref	Expression
Hypotheses	elntg.1	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
	elntg.2	$⊢ I = Itv (𝔼_{𝒢} (N))$
Assertion	elntg	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = (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		elntg.1	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
2		elntg.2	$⊢ I = Itv (𝔼_{𝒢} (N))$
3		lngid	$⊢ {Line}_{𝒢} = Slot {Line}_{𝒢} (ndx)$
4		fvex	$⊢ 𝔼_{𝒢} (N) \in V$
5	4	a1i	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) \in V$
6		eengstr	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) Struct ⟨1, 17⟩$
7		structn0fun	$⊢ 𝔼_{𝒢} (N) Struct ⟨1, 17⟩ \to Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\})$
8	6 7	syl	$⊢ N \in ℕ \to Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\})$
9		structcnvcnv	$⊢ 𝔼_{𝒢} (N) Struct ⟨1, 17⟩ \to {𝔼_{𝒢} (N)}^{-1}^{-1} = 𝔼_{𝒢} (N) ∖ \{\emptyset\}$
10	6 9	syl	$⊢ N \in ℕ \to {𝔼_{𝒢} (N)}^{-1}^{-1} = 𝔼_{𝒢} (N) ∖ \{\emptyset\}$
11	10	funeqd	$⊢ N \in ℕ \to (Fun {𝔼_{𝒢} (N)}^{-1}^{-1} \leftrightarrow Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\}))$
12	8 11	mpbird	$⊢ N \in ℕ \to Fun {𝔼_{𝒢} (N)}^{-1}^{-1}$
13		opex	$⊢ ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩ \in V$
14	13	prid2	$⊢ ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩ \in \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\}$
15		elun2	$⊢ ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩ \in \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\} \to ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩ \in (\{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \cup \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\})$
16	14 15	ax-mp	$⊢ ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩ \in (\{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \cup \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\})$
17		eengv	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) = \{⟨{Base}_{ndx}, 𝔼 (N)⟩, ⟨dist (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \sum_{i = 1}^{N} {(x (i) - y (i))}^{2})⟩\} \cup \{⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩, ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩\}$
18	16 17	eleqtrrid	$⊢ N \in ℕ \to ⟨{Line}_{𝒢} (ndx), (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\})⟩ \in 𝔼_{𝒢} (N)$
19		fvex	$⊢ 𝔼 (N) \in V$
20	19	difexi	$⊢ 𝔼 (N) ∖ \{x\} \in V$
21	19 20	mpoex	$⊢ (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\}) \in V$
22	21	a1i	$⊢ N \in ℕ \to (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\}) \in V$
23	3 5 12 18 22	strfv2d	$⊢ N \in ℕ \to (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\}) = {Line}_{𝒢} (𝔼_{𝒢} (N))$
24		eengbas	$⊢ N \in ℕ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
25	24 1	eqtr4di	$⊢ N \in ℕ \to 𝔼 (N) = P$
26	25	difeq1d	$⊢ N \in ℕ \to 𝔼 (N) ∖ \{x\} = P ∖ \{x\}$
27	26	adantr	$⊢ (N \in ℕ \land x \in 𝔼 (N)) \to 𝔼 (N) ∖ \{x\} = P ∖ \{x\}$
28	25	adantr	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \to 𝔼 (N) = P$
29		simpll	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to N \in ℕ$
30		simplrl	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to x \in 𝔼 (N)$
31	29 25	syl	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to 𝔼 (N) = P$
32	30 31	eleqtrd	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to x \in P$
33		simplrr	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to y \in (𝔼 (N) ∖ \{x\})$
34	33	eldifad	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to y \in 𝔼 (N)$
35	34 31	eleqtrd	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to y \in P$
36		simpr	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to z \in 𝔼 (N)$
37	36 31	eleqtrd	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to z \in P$
38	29 1 2 32 35 37	ebtwntg	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to (z Btwn ⟨x, y⟩ \leftrightarrow z \in (x I y))$
39	29 1 2 37 35 32	ebtwntg	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to (x Btwn ⟨z, y⟩ \leftrightarrow x \in (z I y))$
40	29 1 2 32 37 35	ebtwntg	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to (y Btwn ⟨x, z⟩ \leftrightarrow y \in (x I z))$
41	38 39 40	3orbi123d	$⊢ ((N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \land z \in 𝔼 (N)) \to ((z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩) \leftrightarrow (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))$
42	28 41	rabeqbidva	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land y \in (𝔼 (N) ∖ \{x\}))) \to \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, z⟩)\} = \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}$
43	25 27 42	mpoeq123dva	$⊢ N \in ℕ \to (x \in 𝔼 (N), y \in (𝔼 (N) ∖ \{x\}) ⟼ \{z \in 𝔼 (N) \| (z Btwn ⟨x, y⟩ \lor x Btwn ⟨z, y⟩ \lor y Btwn ⟨x, 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))\})$
44	23 43	eqtr3d	$⊢ N \in ℕ \to {Line}_{𝒢} (𝔼_{𝒢} (N)) = (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))\})$

Metamath Proof Explorer

Theorem elntg

Proof