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 eqcomd ⊢ p = P ∧ i = I → P = p
6 5 adantr ⊢ p = P ∧ i = I ∧ x ∈ P → P = p
7 6 difeq1d ⊢ p = P ∧ i = I ∧ x ∈ P → P ∖ x = p ∖ x
8 simpr ⊢ p = P ∧ i = I → i = I
9 8 eqcomd ⊢ p = P ∧ i = I → I = i
10 9 oveqd ⊢ p = P ∧ i = I → x I y = x i y
11 10 eleq2d ⊢ p = P ∧ i = I → z ∈ x I y ↔ z ∈ x i y
12 9 oveqd ⊢ p = P ∧ i = I → z I y = z i y
13 12 eleq2d ⊢ p = P ∧ i = I → x ∈ z I y ↔ x ∈ z i y
14 9 oveqd ⊢ p = P ∧ i = I → x I z = x i z
15 14 eleq2d ⊢ p = P ∧ i = I → y ∈ x I z ↔ y ∈ x i z
16 11 13 15 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
17 5 16 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
18 17 adantr ⊢ p = P ∧ i = I ∧ x ∈ P ∧ y ∈ P ∖ x → 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
19 5 7 18 mpoeq123dva ⊢ 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
20 19 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
21 1 3 20 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
22 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
23 21 22 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
24 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
25 23 24 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