ebtwntg

Description: The betweenness relation used in the Tarski structure for the Euclidean geometry is the same as Btwn . (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Hypotheses	ebtwntg.1	$⊢ φ \to N \in ℕ$
	ebtwntg.2	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
	ebtwntg.3	$⊢ I = Itv (𝔼_{𝒢} (N))$
	ebtwntg.x	$⊢ φ \to X \in P$
	ebtwntg.y	$⊢ φ \to Y \in P$
	ebtwntg.z	$⊢ φ \to Z \in P$
Assertion	ebtwntg	$⊢ φ \to (Z Btwn ⟨X, Y⟩ \leftrightarrow Z \in (X I Y))$

Proof

Step	Hyp	Ref	Expression
1		ebtwntg.1	$⊢ φ \to N \in ℕ$
2		ebtwntg.2	$⊢ P = {Base}_{𝔼_{𝒢} (N)}$
3		ebtwntg.3	$⊢ I = Itv (𝔼_{𝒢} (N))$
4		ebtwntg.x	$⊢ φ \to X \in P$
5		ebtwntg.y	$⊢ φ \to Y \in P$
6		ebtwntg.z	$⊢ φ \to Z \in P$
7		itvid	$⊢ Itv = Slot Itv (ndx)$
8		fvexd	$⊢ φ \to 𝔼_{𝒢} (N) \in V$
9		eengstr	$⊢ N \in ℕ \to 𝔼_{𝒢} (N) Struct ⟨1, 17⟩$
10	1 9	syl	$⊢ φ \to 𝔼_{𝒢} (N) Struct ⟨1, 17⟩$
11		structn0fun	$⊢ 𝔼_{𝒢} (N) Struct ⟨1, 17⟩ \to Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\})$
12	10 11	syl	$⊢ φ \to Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\})$
13		structcnvcnv	$⊢ 𝔼_{𝒢} (N) Struct ⟨1, 17⟩ \to {𝔼_{𝒢} (N)}^{-1}^{-1} = 𝔼_{𝒢} (N) ∖ \{\emptyset\}$
14	10 13	syl	$⊢ φ \to {𝔼_{𝒢} (N)}^{-1}^{-1} = 𝔼_{𝒢} (N) ∖ \{\emptyset\}$
15	14	funeqd	$⊢ φ \to (Fun {𝔼_{𝒢} (N)}^{-1}^{-1} \leftrightarrow Fun (𝔼_{𝒢} (N) ∖ \{\emptyset\}))$
16	12 15	mpbird	$⊢ φ \to Fun {𝔼_{𝒢} (N)}^{-1}^{-1}$
17		opex	$⊢ ⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩ \in V$
18	17	prid1	$⊢ ⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩ \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⟩)\})⟩\}$
19		elun2	$⊢ ⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩ \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 ⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩ \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⟩)\})⟩\})$
20	18 19	ax-mp	$⊢ ⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩ \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⟩)\})⟩\})$
21		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⟩)\})⟩\}$
22	1 21	syl	$⊢ φ \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⟩)\})⟩\}$
23	20 22	eleqtrrid	$⊢ φ \to ⟨Itv (ndx), (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})⟩ \in 𝔼_{𝒢} (N)$
24		fvex	$⊢ 𝔼 (N) \in V$
25	24 24	mpoex	$⊢ (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\}) \in V$
26	25	a1i	$⊢ φ \to (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\}) \in V$
27	7 8 16 23 26	strfv2d	$⊢ φ \to (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\}) = Itv (𝔼_{𝒢} (N))$
28	3 27	eqtr4id	$⊢ φ \to I = (x \in 𝔼 (N), y \in 𝔼 (N) ⟼ \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\})$
29		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
30		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
31	29 30	opeq12d	$⊢ (φ \land (x = X \land y = Y)) \to ⟨x, y⟩ = ⟨X, Y⟩$
32	31	breq2d	$⊢ (φ \land (x = X \land y = Y)) \to (z Btwn ⟨x, y⟩ \leftrightarrow z Btwn ⟨X, Y⟩)$
33	32	rabbidv	$⊢ (φ \land (x = X \land y = Y)) \to \{z \in 𝔼 (N) \| z Btwn ⟨x, y⟩\} = \{z \in 𝔼 (N) \| z Btwn ⟨X, Y⟩\}$
34	4 2	eleqtrdi	$⊢ φ \to X \in {Base}_{𝔼_{𝒢} (N)}$
35		eengbas	$⊢ N \in ℕ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
36	1 35	syl	$⊢ φ \to 𝔼 (N) = {Base}_{𝔼_{𝒢} (N)}$
37	34 36	eleqtrrd	$⊢ φ \to X \in 𝔼 (N)$
38	5 2	eleqtrdi	$⊢ φ \to Y \in {Base}_{𝔼_{𝒢} (N)}$
39	38 36	eleqtrrd	$⊢ φ \to Y \in 𝔼 (N)$
40	24	rabex	$⊢ \{z \in 𝔼 (N) \| z Btwn ⟨X, Y⟩\} \in V$
41	40	a1i	$⊢ φ \to \{z \in 𝔼 (N) \| z Btwn ⟨X, Y⟩\} \in V$
42	28 33 37 39 41	ovmpod	$⊢ φ \to X I Y = \{z \in 𝔼 (N) \| z Btwn ⟨X, Y⟩\}$
43	42	eleq2d	$⊢ φ \to (Z \in (X I Y) \leftrightarrow Z \in \{z \in 𝔼 (N) \| z Btwn ⟨X, Y⟩\})$
44	6 2	eleqtrdi	$⊢ φ \to Z \in {Base}_{𝔼_{𝒢} (N)}$
45	44 36	eleqtrrd	$⊢ φ \to Z \in 𝔼 (N)$
46		breq1	$⊢ z = Z \to (z Btwn ⟨X, Y⟩ \leftrightarrow Z Btwn ⟨X, Y⟩)$
47	46	elrab3	$⊢ Z \in 𝔼 (N) \to (Z \in \{z \in 𝔼 (N) \| z Btwn ⟨X, Y⟩\} \leftrightarrow Z Btwn ⟨X, Y⟩)$
48	45 47	syl	$⊢ φ \to (Z \in \{z \in 𝔼 (N) \| z Btwn ⟨X, Y⟩\} \leftrightarrow Z Btwn ⟨X, Y⟩)$
49	43 48	bitr2d	$⊢ φ \to (Z Btwn ⟨X, Y⟩ \leftrightarrow Z \in (X I Y))$

Metamath Proof Explorer

Theorem ebtwntg

Proof