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)

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