Metamath Proof Explorer

Theorem istrkgl

Description: Building lines from the segment property. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses istrkg.p ⊢ P = Base G
istrkg.d ⊢ - ˙ = dist ⁡ G
istrkg.i ⊢ I = Itv ⁡ G
Assertion istrkgl ⊢ G ∈ f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z ↔ G ∈ V ∧ Line 𝒢 ⁡ G = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z

Proof

Step Hyp Ref Expression
1 istrkg.p ⊢ P = Base G
2 istrkg.d ⊢ - ˙ = dist ⁡ G
3 istrkg.i ⊢ I = Itv ⁡ G
4 simpl ⊢ p = P ∧ i = I → p = P
5 4 difeq1d ⊢ p = P ∧ i = I → p ∖ x = P ∖ x
6 simpr ⊢ p = P ∧ i = I → i = I
7 6 oveqd ⊢ p = P ∧ i = I → x i y = x I y
8 7 eleq2d ⊢ p = P ∧ i = I → z ∈ x i y ↔ z ∈ x I y
9 6 oveqd ⊢ p = P ∧ i = I → z i y = z I y
10 9 eleq2d ⊢ p = P ∧ i = I → x ∈ z i y ↔ x ∈ z I y
11 6 oveqd ⊢ p = P ∧ i = I → x i z = x I z
12 11 eleq2d ⊢ p = P ∧ i = I → y ∈ x i z ↔ y ∈ x I z
13 8 10 12 3orbi123d ⊢ p = P ∧ i = I → z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z ↔ z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
14 4 13 rabeqbidv ⊢ p = P ∧ i = I → z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z = z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
15 4 5 14 mpoeq123dv ⊢ p = P ∧ i = I → x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
16 15 eqeq2d ⊢ p = P ∧ i = I → Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z ↔ Line 𝒢 ⁡ f = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
17 1 3 16 sbcie2s ⊢ f = G → [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z ↔ Line 𝒢 ⁡ f = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
18 fveqeq2 ⊢ f = G → Line 𝒢 ⁡ f = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z ↔ Line 𝒢 ⁡ G = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
19 17 18 bitrd ⊢ f = G → [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z ↔ Line 𝒢 ⁡ G = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z
20 eqid ⊢ f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z = f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z
21 19 20 elab4g ⊢ G ∈ f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ Line 𝒢 ⁡ f = x ∈ p , y ∈ p ∖ x ⟼ z ∈ p | z ∈ x i y ∨ x ∈ z i y ∨ y ∈ x i z ↔ G ∈ V ∧ Line 𝒢 ⁡ G = x ∈ P , y ∈ P ∖ x ⟼ z ∈ P | z ∈ x I y ∨ x ∈ z I y ∨ y ∈ x I z