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=BaseG
istrkg.d ⊢-˙=dist⁡G
istrkg.i ⊢I=Itv⁡G
Assertion istrkgl ⊢G∈f|[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz↔G∈V∧Line𝒢⁡G=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz

Proof

Step Hyp Ref Expression
1 istrkg.p ⊢P=BaseG
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→xiy=xIy
8 7 eleq2d ⊢p=P∧i=I→z∈xiy↔z∈xIy
9 6 oveqd ⊢p=P∧i=I→ziy=zIy
10 9 eleq2d ⊢p=P∧i=I→x∈ziy↔x∈zIy
11 6 oveqd ⊢p=P∧i=I→xiz=xIz
12 11 eleq2d ⊢p=P∧i=I→y∈xiz↔y∈xIz
13 8 10 12 3orbi123d ⊢p=P∧i=I→z∈xiy∨x∈ziy∨y∈xiz↔z∈xIy∨x∈zIy∨y∈xIz
14 4 13 rabeqbidv ⊢p=P∧i=I→z∈p|z∈xiy∨x∈ziy∨y∈xiz=z∈P|z∈xIy∨x∈zIy∨y∈xIz
15 4 5 14 mpoeq123dv ⊢p=P∧i=I→x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
16 15 eqeq2d ⊢p=P∧i=I→Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz↔Line𝒢⁡f=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
17 1 3 16 sbcie2s ⊢f=G→[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz↔Line𝒢⁡f=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
18 fveqeq2 ⊢f=G→Line𝒢⁡f=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz↔Line𝒢⁡G=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
19 17 18 bitrd ⊢f=G→[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz↔Line𝒢⁡G=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz
20 eqid ⊢f|[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz=f|[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz
21 19 20 elab4g ⊢G∈f|[˙Basef/p]˙[˙Itv⁡f/i]˙Line𝒢⁡f=x∈p,y∈p∖x⟼z∈p|z∈xiy∨x∈ziy∨y∈xiz↔G∈V∧Line𝒢⁡G=x∈P,y∈P∖x⟼z∈P|z∈xIy∨x∈zIy∨y∈xIz