ttgvalOLD

Description: Obsolete proof of ttgval as of 9-Nov-2024. Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	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	ttgvalOLD	$⊢ 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	21	csbeq1d	$⊢ 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 ⦌ ((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))\})⟩)$
23		oveq1	$⊢ w = H \to w sSet ⟨Itv (ndx), i⟩ = H sSet ⟨Itv (ndx), i⟩$
24	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))\}$
25	9 9 24	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))\})$
26	25	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))\})⟩$
27	23 26	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))\})⟩$
28	27	csbeq2dv	$⊢ w = H \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 ⦌ ((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))\})⟩)$
29	22 28	eqtrd	$⊢ 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))\})⟩)$
30		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))\})⟩))$
31		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$
32	31	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$
33	29 30 32	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))\})⟩)$
34	7 33	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))\})⟩)$
35	2	fvexi	$⊢ B \in V$
36	35 35	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$
37	36	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$
38		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)\})$
39		oveq2	$⊢ a = x \to c \underset{˙}{-} a = c \underset{˙}{-} x$
40		oveq2	$⊢ a = x \to b \underset{˙}{-} a = b \underset{˙}{-} x$
41	40	oveq2d	$⊢ a = x \to k \underset{˙}{\cdot} (b \underset{˙}{-} a) = k \underset{˙}{\cdot} (b \underset{˙}{-} x)$
42	39 41	eqeq12d	$⊢ a = x \to (c \underset{˙}{-} a = k \underset{˙}{\cdot} (b \underset{˙}{-} a) \leftrightarrow c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x))$
43	42	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))$
44	43	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)\}$
45		oveq1	$⊢ b = y \to b \underset{˙}{-} x = y \underset{˙}{-} x$
46	45	oveq2d	$⊢ b = y \to k \underset{˙}{\cdot} (b \underset{˙}{-} x) = k \underset{˙}{\cdot} (y \underset{˙}{-} x)$
47	46	eqeq2d	$⊢ b = y \to (c \underset{˙}{-} x = k \underset{˙}{\cdot} (b \underset{˙}{-} x) \leftrightarrow c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
48	47	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))$
49	48	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)\}$
50		oveq1	$⊢ c = z \to c \underset{˙}{-} x = z \underset{˙}{-} x$
51	50	eqeq1d	$⊢ c = z \to (c \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x) \leftrightarrow z \underset{˙}{-} x = k \underset{˙}{\cdot} (y \underset{˙}{-} x))$
52	51	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))$
53	52	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)\}$
54	49 53	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)\}$
55	44 54	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)\})$
56	38 55	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)\})$
57		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)\})$
58	57 55	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)\})$
59	58	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)\})⟩$
60	59	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)\})⟩$
61	58	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$
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 (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))$
63	58	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$
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 (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))$
65	58	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$
66	65	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))$
67	62 64 66	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)))$
68	67	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))\}$
69	68	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))\})$
70	69	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))\})⟩$
71	60 70	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))\})⟩$
72	56 71	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))\})⟩$
73	37 72	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))\})⟩$
74	6 34 73	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))\})⟩$
75	74	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))\})⟩)$
76		itvid	$⊢ Itv = Slot Itv (ndx)$
77		1nn0	$⊢ 1 \in ℕ_{0}$
78		6nn	$⊢ 6 \in ℕ$
79	77 78	decnncl	$⊢ 16 \in ℕ$
80	79	nnrei	$⊢ 16 \in ℝ$
81		6nn0	$⊢ 6 \in ℕ_{0}$
82		7nn	$⊢ 7 \in ℕ$
83		6lt7	$⊢ 6 < 7$
84	77 81 82 83	declt	$⊢ 16 < 17$
85	80 84	ltneii	$⊢ 16 \neq 17$
86		itvndx	$⊢ Itv (ndx) = 16$
87		lngndx	$⊢ {Line}_{𝒢} (ndx) = 17$
88	86 87	neeq12i	$⊢ Itv (ndx) \neq {Line}_{𝒢} (ndx) \leftrightarrow 16 \neq 17$
89	85 88	mpbir	$⊢ Itv (ndx) \neq {Line}_{𝒢} (ndx)$
90	76 89	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))\})⟩)$
91	75 90	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)\})⟩)$
92	5	a1i	$⊢ H \in V \to I = Itv (G)$
93	76	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)\})⟩)$
94	36 93	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)\})⟩)$
95	91 92 94	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)\})$
96	95	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$
97	96	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))$
98	95	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$
99	98	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))$
100	95	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$
101	100	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))$
102	97 99 101	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)))$
103	102	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))\}$
104	103	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))\})$
105	104	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))\})⟩$
106	105	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))\})⟩$
107	74 106	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))\})⟩$
108	107 95	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 ttgvalOLD

Proof