Metamath Proof Explorer

Theorem ttglem

Description: Lemma for ttgbas , ttgvsca etc. (Contributed by Thierry Arnoux, 15-Apr-2019) (Revised by AV, 29-Oct-2024)

Ref Expression
Hypotheses ttgval.n ⊢ G = to𝒢 Tarski ⁡ H
ttglem.e ⊢ E = Slot E ⁡ ndx
ttglem.l ⊢ E ⁡ ndx ≠ Line 𝒢 ⁡ ndx
ttglem.i ⊢ E ⁡ ndx ≠ Itv ⁡ ndx
Assertion ttglem ⊢ E ⁡ H = E ⁡ G

Proof

Step Hyp Ref Expression
1 ttgval.n ⊢ G = to𝒢 Tarski ⁡ H
2 ttglem.e ⊢ E = Slot E ⁡ ndx
3 ttglem.l ⊢ E ⁡ ndx ≠ Line 𝒢 ⁡ ndx
4 ttglem.i ⊢ E ⁡ ndx ≠ Itv ⁡ ndx
5 2 4 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
6 2 3 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
7 5 6 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
8 eqid ⊢ Base H = Base H
9 eqid ⊢ - H = - H
10 eqid ⊢ ⋅ H = ⋅ H
11 eqid ⊢ Itv ⁡ G = Itv ⁡ G
12 1 8 9 10 11 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
13 12 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
14 13 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
15 7 14 eqtr4id ⊢ H ∈ V → E ⁡ H = E ⁡ G
16 2 str0 ⊢ ∅ = E ⁡ ∅
17 16 eqcomi ⊢ E ⁡ ∅ = ∅
18 17 1 fveqprc ⊢ ¬ H ∈ V → E ⁡ H = E ⁡ G
19 15 18 pm2.61i ⊢ E ⁡ H = E ⁡ G