ttgval

Description: Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019) (Proof shortened by AV, 9-Nov-2024)

	Ref	Expression
Hypotheses	ttgval.n	$⊢ G = {to𝒢}_{Tarski} (H)$
	ttgval.b	$⊢ B = {Base}_{H}$
	ttgval.m	$⊢ \underset{˙}{-} = -_{H}$
	ttgval.s	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
	ttgval.i	$⊢ I = Itv (G)$
Assertion	ttgval	$⊢ H \in V \to (G = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})⟩ \land I = (x \in B, y \in B ⟼ \{z \in B \| \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		ttgval.b	$⊢ B = {Base}_{H}$
3		ttgval.m	$⊢ \underset{˙}{-} = -_{H}$
4		ttgval.s	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
5		ttgval.i	$⊢ I = Itv (G)$
6	1	a1i	$⊢ H \in V \to G = {to𝒢}_{Tarski} (H)$
7		elex	$⊢ H \in V \to H \in V$
8		fveq2	$⊢ w = H \to {Base}_{w} = {Base}_{H}$
9	8 2	eqtr4di	$⊢ w = H \to {Base}_{w} = B$
10		fveq2	$⊢ w = H \to -_{w} = -_{H}$
11	10 3	eqtr4di	$⊢ w = H \to -_{w} = \underset{˙}{-}$
12	11	oveqd	$⊢ w = H \to z -_{w} x = z \underset{˙}{-} x$
13		fveq2	$⊢ w = H \to \cdot_{w} = \cdot_{H}$
14	13 4	eqtr4di	$⊢ w = H \to \cdot_{w} = \underset{˙}{\cdot}$
15		eqidd	$⊢ w = H \to k = k$
16	11	oveqd	$⊢ w = H \to y -_{w} x = y \underset{˙}{-} x$
17	14 15 16	oveq123d	$⊢ w = H \to k \cdot_{w} (y -_{w} x) = k \underset{˙}{\cdot} (y \underset{˙}{-} x)$
18	12 17	eqeq12d	$⊢ w = H \to (z -_{w} x = k \cdot_{w} (y -_{w} x) \leftrightarrow z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
19	18	rexbidv	$⊢ w = H \to (\exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x) \leftrightarrow \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
20	9 19	rabeqbidv	$⊢ w = H \to \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\} = \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}$
21	9 9 20	mpoeq123dv	$⊢ w = H \to (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}) = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})$
22		oveq1	$⊢ w = H \to w sSet ⟨Itv (ndx), i⟩ = H sSet ⟨Itv (ndx), i⟩$
23	9	rabeqdv	$⊢ w = H \to \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\} = \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\}$
24	9 9 23	mpoeq123dv	$⊢ w = H \to (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\}) = (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})$
25	24	opeq2d	$⊢ w = H \to ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩ = ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩$
26	22 25	oveq12d	$⊢ w = H \to (w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩ = (H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩$
27	21 26	csbeq12dv	$⊢ w = H \to ⦋ (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}) / i ⦌ ((w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩) = ⦋ (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) / i ⦌ ((H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩)$
28		df-ttg	$⊢ {to𝒢}_{Tarski} = (w \in V ⟼ ⦋ (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| \exists k \in [0, 1] z -_{w} x = k \cdot_{w} (y -_{w} x)\}) / i ⦌ ((w sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in {Base}_{w}, y \in {Base}_{w} ⟼ \{z \in {Base}_{w} \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩))$
29		ovex	$⊢ (H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩ \in V$
30	29	csbex	$⊢ ⦋ (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) / i ⦌ ((H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩) \in V$
31	27 28 30	fvmpt	$⊢ H \in V \to {to𝒢}_{Tarski} (H) = ⦋ (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) / i ⦌ ((H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩)$
32	7 31	syl	$⊢ H \in V \to {to𝒢}_{Tarski} (H) = ⦋ (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) / i ⦌ ((H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩)$
33	2	fvexi	$⊢ B \in V$
34	33 33	mpoex	$⊢ (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) \in V$
35	34	a1i	$⊢ H \in V \to (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) \in V$
36		simpr	$⊢ (H \in V \land i = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})) \to i = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})$
37		oveq2	$⊢ a = x \to c \underset{˙}{-} a = c \underset{˙}{-} x$
38		oveq2	$⊢ a = x \to b \underset{˙}{-} a = b \underset{˙}{-} x$
39	38	oveq2d	$⊢ a = x \to k \underset{˙}{\cdot} (b \underset{˙}{-} a) = k \underset{˙}{\cdot} (b \underset{˙}{-} x)$
40	37 39	eqeq12d	$⊢ a = x \to (c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a) \leftrightarrow c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x))$
41	40	rexbidv	$⊢ a = x \to (\exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a) \leftrightarrow \exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x))$
42	41	rabbidv	$⊢ a = x \to \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\} = \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x)\}$
43		oveq1	$⊢ b = y \to b \underset{˙}{-} x = y \underset{˙}{-} x$
44	43	oveq2d	$⊢ b = y \to k \underset{˙}{\cdot} (b \underset{˙}{-} x) = k \underset{˙}{\cdot} (y \underset{˙}{-} x)$
45	44	eqeq2d	$⊢ b = y \to (c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x) \leftrightarrow c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
46	45	rexbidv	$⊢ b = y \to (\exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x) \leftrightarrow \exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
47	46	rabbidv	$⊢ b = y \to \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x)\} = \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}$
48		oveq1	$⊢ c = z \to c \underset{˙}{-} x = z \underset{˙}{-} x$
49	48	eqeq1d	$⊢ c = z \to (c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x) \leftrightarrow z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
50	49	rexbidv	$⊢ c = z \to (\exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x) \leftrightarrow \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
51	50	cbvrabv	$⊢ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\} = \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}$
52	47 51	eqtrdi	$⊢ b = y \to \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x)\} = \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}$
53	42 52	cbvmpov	$⊢ (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\}) = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})$
54	36 53	eqtr4di	$⊢ (H \in V \land i = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})) \to i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})$
55		simpr	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})$
56	55 53	eqtrdi	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to i = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})$
57	56	opeq2d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to ⟨Itv (ndx), i⟩ = ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩$
58	57	oveq2d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to H sSet ⟨Itv (ndx), i⟩ = H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩$
59	56	oveqd	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to x i y = x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y$
60	59	eleq2d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to (z \in (x i y) \leftrightarrow z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y))$
61	56	oveqd	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to z i y = z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y$
62	61	eleq2d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to (x \in (z i y) \leftrightarrow x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y))$
63	56	oveqd	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to x i z = x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z$
64	63	eleq2d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to (y \in (x i z) \leftrightarrow y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))$
65	60 62 64	3orbi123d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to ((z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \leftrightarrow (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z)))$
66	65	rabbidv	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\} = \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\}$
67	66	mpoeq3dv	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\}) = (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})$
68	67	opeq2d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩ = ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩$
69	58 68	oveq12d	$⊢ (H \in V \land i = (a \in B, b \in B ⟼ \{c \in B \| \exists k \in [0, 1] c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a)\})) \to (H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩ = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩$
70	54 69	syldan	$⊢ (H \in V \land i = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})) \to (H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩ = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩$
71	35 70	csbied	$⊢ H \in V \to ⦋ (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) / i ⦌ ((H sSet ⟨Itv (ndx), i⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})⟩) = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩$
72	6 32 71	3eqtrd	$⊢ H \in V \to G = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩$
73	72	fveq2d	$⊢ H \in V \to Itv (G) = Itv ((H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩)$
74		itvid	$⊢ Itv = Slot Itv (ndx)$
75		lngndxnitvndx	$⊢ {Line}_{𝒢} (ndx) \neq Itv (ndx)$
76	75	necomi	$⊢ Itv (ndx) \neq {Line}_{𝒢} (ndx)$
77	74 76	setsnid	$⊢ Itv (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) = Itv ((H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩)$
78	73 77	eqtr4di	$⊢ H \in V \to Itv (G) = Itv (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩)$
79	5	a1i	$⊢ H \in V \to I = Itv (G)$
80	74	setsid	$⊢ (H \in V \land (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) \in V) \to (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) = Itv (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩)$
81	34 80	mpan2	$⊢ H \in V \to (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) = Itv (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩)$
82	78 79 81	3eqtr4d	$⊢ H \in V \to I = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})$
83	82	oveqd	$⊢ H \in V \to x I y = x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y$
84	83	eleq2d	$⊢ H \in V \to (z \in (x I y) \leftrightarrow z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y))$
85	82	oveqd	$⊢ H \in V \to z I y = z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y$
86	85	eleq2d	$⊢ H \in V \to (x \in (z I y) \leftrightarrow x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y))$
87	82	oveqd	$⊢ H \in V \to x I z = x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z$
88	87	eleq2d	$⊢ H \in V \to (y \in (x I z) \leftrightarrow y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))$
89	84 86 88	3orbi123d	$⊢ H \in V \to ((z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z)))$
90	89	rabbidv	$⊢ H \in V \to \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\} = \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\}$
91	90	mpoeq3dv	$⊢ H \in V \to (x \in B, y \in B ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\}) = (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})$
92	91	opeq2d	$⊢ H \in V \to ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})⟩ = ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩$
93	92	oveq2d	$⊢ H \in V \to (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})⟩ = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor x \in (z (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) y) \lor y \in (x (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}) z))\})⟩$
94	72 93	eqtr4d	$⊢ H \in V \to G = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})⟩$
95	94 82	jca	$⊢ H \in V \to (G = (H sSet ⟨Itv (ndx), (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\})⟩) sSet ⟨{Line}_{𝒢} (ndx), (x \in B, y \in B ⟼ \{z \in B \| (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))\})⟩ \land I = (x \in B, y \in B ⟼ \{z \in B \| \exists k \in [0, 1] z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x)\}))$

Metamath Proof Explorer

Theorem ttgval

Proof