Metamath Proof Explorer

Theorem ttglem

Description: Lemma for ttgbas and ttgvsca . (Contributed by Thierry Arnoux, 15-Apr-2019)

Ref Expression
Hypotheses ttgval.n ⊢ G = to𝒢 Tarski ⁡ H
ttglem.2 ⊢ E = Slot N
ttglem.3 ⊢ N ∈ ℕ
ttglem.4 ⊢ N < 16
Assertion ttglem ⊢ E ⁡ H = E ⁡ G

Proof

Step Hyp Ref Expression
1 ttgval.n ⊢ G = to𝒢 Tarski ⁡ H
2 ttglem.2 ⊢ E = Slot N
3 ttglem.3 ⊢ N ∈ ℕ
4 ttglem.4 ⊢ N < 16
5 2 3 ndxid ⊢ E = Slot E ⁡ ndx
6 3 nnrei ⊢ N ∈ ℝ
7 6 4 ltneii ⊢ N ≠ 16
8 2 3 ndxarg ⊢ E ⁡ ndx = N
9 itvndx ⊢ Itv ⁡ ndx = 16
10 8 9 neeq12i ⊢ E ⁡ ndx ≠ Itv ⁡ ndx ↔ N ≠ 16
11 7 10 mpbir ⊢ E ⁡ ndx ≠ Itv ⁡ ndx
12 5 11 setsnid ⊢ E ⁡ H = E ⁡ H sSet Itv ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x
13 1nn0 ⊢ 1 ∈ ℕ 0
14 6nn0 ⊢ 6 ∈ ℕ 0
15 7nn ⊢ 7 ∈ ℕ
16 6lt7 ⊢ 6 < 7
17 13 14 15 16 declt ⊢ 16 < 17
18 6nn ⊢ 6 ∈ ℕ
19 13 18 decnncl ⊢ 16 ∈ ℕ
20 19 nnrei ⊢ 16 ∈ ℝ
21 13 15 decnncl ⊢ 17 ∈ ℕ
22 21 nnrei ⊢ 17 ∈ ℝ
23 6 20 22 lttri ⊢ N < 16 ∧ 16 < 17 → N < 17
24 4 17 23 mp2an ⊢ N < 17
25 6 24 ltneii ⊢ N ≠ 17
26 lngndx ⊢ Line 𝒢 ⁡ ndx = 17
27 8 26 neeq12i ⊢ E ⁡ ndx ≠ Line 𝒢 ⁡ ndx ↔ N ≠ 17
28 25 27 mpbir ⊢ E ⁡ ndx ≠ Line 𝒢 ⁡ ndx
29 5 28 setsnid ⊢ E ⁡ H sSet Itv ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x = E ⁡ H sSet Itv ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x sSet Line 𝒢 ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | z ∈ x Itv ⁡ G y ∨ x ∈ z Itv ⁡ G y ∨ y ∈ x Itv ⁡ G z
30 12 29 eqtri ⊢ E ⁡ H = E ⁡ H sSet Itv ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x sSet Line 𝒢 ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | z ∈ x Itv ⁡ G y ∨ x ∈ z Itv ⁡ G y ∨ y ∈ x Itv ⁡ G z
31 eqid ⊢ Base H = Base H
32 eqid ⊢ - H = - H
33 eqid ⊢ ⋅ H = ⋅ H
34 eqid ⊢ Itv ⁡ G = Itv ⁡ G
35 1 31 32 33 34 ttgval ⊢ H ∈ V → G = H sSet Itv ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x sSet Line 𝒢 ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | z ∈ x Itv ⁡ G y ∨ x ∈ z Itv ⁡ G y ∨ y ∈ x Itv ⁡ G z ∧ Itv ⁡ G = x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x
36 35 simpld ⊢ H ∈ V → G = H sSet Itv ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x sSet Line 𝒢 ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | z ∈ x Itv ⁡ G y ∨ x ∈ z Itv ⁡ G y ∨ y ∈ x Itv ⁡ G z
37 36 fveq2d ⊢ H ∈ V → E ⁡ G = E ⁡ H sSet Itv ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | ∃ k ∈ 0 1 z - H x = k ⋅ H y - H x sSet Line 𝒢 ⁡ ndx x ∈ Base H , y ∈ Base H ⟼ z ∈ Base H | z ∈ x Itv ⁡ G y ∨ x ∈ z Itv ⁡ G y ∨ y ∈ x Itv ⁡ G z
38 30 37 eqtr4id ⊢ H ∈ V → E ⁡ H = E ⁡ G
39 2 str0 ⊢ ∅ = E ⁡ ∅
40 fvprc ⊢ ¬ H ∈ V → E ⁡ H = ∅
41 fvprc ⊢ ¬ H ∈ V → to𝒢 Tarski ⁡ H = ∅
42 1 41 syl5eq ⊢ ¬ H ∈ V → G = ∅
43 42 fveq2d ⊢ ¬ H ∈ V → E ⁡ G = E ⁡ ∅
44 39 40 43 3eqtr4a ⊢ ¬ H ∈ V → E ⁡ H = E ⁡ G
45 38 44 pm2.61i ⊢ E ⁡ H = E ⁡ G