ttgitvval

Description: Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019)

	Ref	Expression
Hypotheses	ttgval.n	$⊢ G = {to𝒢}_{Tarski} (H)$
	ttgitvval.i	$⊢ I = Itv (G)$
	ttgitvval.b	$⊢ P = {Base}_{H}$
	ttgitvval.m	$⊢ \underset{˙}{-} = -_{H}$
	ttgitvval.s	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
Assertion	ttgitvval	$⊢ (H \in V \land X \in P \land Y \in P) \to X I Y = \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} X = k \underset{˙}{\cdot} (Y \underset{˙}{-} X)\}$

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$⊢ G = {to𝒢}_{Tarski} (H)$
2		ttgitvval.i	$⊢ I = Itv (G)$
3		ttgitvval.b	$⊢ P = {Base}_{H}$
4		ttgitvval.m	$⊢ \underset{˙}{-} = -_{H}$
5		ttgitvval.s	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
6	1 3 4 5 2	ttgval	$⊢ H \in V \to (G = (H sSet ⟨Itv (ndx), (x \in P, y \in P ⟼ \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in P, y \in P ⟼ \{z \in P \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})⟩ \land I = (x \in P, y \in P ⟼ \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}))$
7	6	simprd	$⊢ H \in V \to I = (x \in P, y \in P ⟼ \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})$
8	7	3ad2ant1	$⊢ (H \in V \land X \in P \land Y \in P) \to I = (x \in P, y \in P ⟼ \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})$
9		simprl	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to x = X$
10	9	oveq2d	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to z \underset{˙}{-} x = z \underset{˙}{-} X$
11		simprr	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to y = Y$
12	11 9	oveq12d	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to y \underset{˙}{-} x = Y \underset{˙}{-} X$
13	12	oveq2d	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to k \underset{˙}{\cdot} (y \underset{˙}{-} x) = k \underset{˙}{\cdot} (Y \underset{˙}{-} X)$
14	10 13	eqeq12d	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to (z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x) \leftrightarrow z \underset{˙}{-} X = k \underset{˙}{\cdot} (Y \underset{˙}{-} X))$
15	14	rexbidv	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to (\exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x) \leftrightarrow \exists k \in [0, 1] z \underset{˙}{-} X = k \underset{˙}{\cdot} (Y \underset{˙}{-} X))$
16	15	rabbidv	$⊢ ((H \in V \land X \in P \land Y \in P) \land (x = X \land y = Y)) \to \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\} = \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} X = k \underset{˙}{\cdot} (Y \underset{˙}{-} X)\}$
17		simp2	$⊢ (H \in V \land X \in P \land Y \in P) \to X \in P$
18		simp3	$⊢ (H \in V \land X \in P \land Y \in P) \to Y \in P$
19	3	fvexi	$⊢ P \in V$
20	19	rabex	$⊢ \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} X = k \underset{˙}{\cdot} (Y \underset{˙}{-} X)\} \in V$
21	20	a1i	$⊢ (H \in V \land X \in P \land Y \in P) \to \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} X = k \underset{˙}{\cdot} (Y \underset{˙}{-} X)\} \in V$
22	8 16 17 18 21	ovmpod	$⊢ (H \in V \land X \in P \land Y \in P) \to X I Y = \{z \in P \| \exists k \in [0, 1] z \underset{˙}{-} X = k \underset{˙}{\cdot} (Y \underset{˙}{-} X)\}$

Metamath Proof Explorer

Theorem ttgitvval

Proof