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 e. { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } <-> ( G e. _V /\ ( LineG ` G ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( 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 e. ( x i y ) <-> z e. ( x I y ) ) )
9 6 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( z i y ) = ( z I y ) )
10 9 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( x e. ( z i y ) <-> x e. ( z I y ) ) )
11 6 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x i z ) = ( x I z ) )
12 11 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( y e. ( x i z ) <-> y e. ( x I z ) ) )
13 8 10 12 3orbi123d 
 |-  ( ( p = P /\ i = I ) -> ( ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) <-> ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) ) )
14 4 13 rabeqbidv 
 |-  ( ( p = P /\ i = I ) -> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } = { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } )
15 4 5 14 mpoeq123dv 
 |-  ( ( p = P /\ i = I ) -> ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) )
16 15 eqeq2d 
 |-  ( ( p = P /\ i = I ) -> ( ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) <-> ( LineG ` f ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) ) )
17 1 3 16 sbcie2s 
 |-  ( f = G -> ( [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) <-> ( LineG ` f ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) ) )
18 fveqeq2 
 |-  ( f = G -> ( ( LineG ` f ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) <-> ( LineG ` G ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) ) )
19 17 18 bitrd 
 |-  ( f = G -> ( [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) <-> ( LineG ` G ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) ) )
20 eqid 
 |-  { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } = { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) }
21 19 20 elab4g 
 |-  ( G e. { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } <-> ( G e. _V /\ ( LineG ` G ) = ( x e. P , y e. ( P \ { x } ) |-> { z e. P | ( z e. ( x I y ) \/ x e. ( z I y ) \/ y e. ( x I z ) ) } ) ) )