Metamath Proof Explorer

Theorem 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 ⊢ - ˙ = - H
ttgval.s ⊢ · ˙ = ⋅ H
ttgval.i ⊢ I = Itv ⁡ G
Assertion ttgval ⊢ H ∈ V → G = H sSet Itv ⁡ ndx x ∈ B , y ∈ B ⟼ z ∈ B | ∃ k ∈ 0 1 z - ˙ x = k · ˙ y - ˙ x sSet Line 𝒢 ⁡ ndx x ∈ B , y ∈ B ⟼ z ∈ B | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ∧ I = x ∈ B , y ∈ B ⟼ z ∈ B | ∃ k ∈ 0 1 z - ˙ x = k · ˙ y - ˙ x

Proof

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