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 eqcomd 
 |-  ( ( p = P /\ i = I ) -> P = p )
6 5 adantr 
 |-  ( ( ( p = P /\ i = I ) /\ x e. P ) -> P = p )
7 6 difeq1d 
 |-  ( ( ( p = P /\ i = I ) /\ x e. 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 e. ( x I y ) <-> z e. ( x i y ) ) )
12 9 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( z I y ) = ( z i y ) )
13 12 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( x e. ( z I y ) <-> x e. ( z i y ) ) )
14 9 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x I z ) = ( x i z ) )
15 14 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( y e. ( x I z ) <-> y e. ( x i z ) ) )
16 11 13 15 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 ) ) ) )
17 5 16 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 ) ) } )
18 17 adantr 
 |-  ( ( ( 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 ) ) } = { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } )
19 5 7 18 mpoeq123dva 
 |-  ( ( 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 ) ) } ) )
20 19 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 ) ) } ) ) )
21 1 3 20 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 ) ) } ) ) )
22 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 ) ) } ) ) )
23 21 22 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 ) ) } ) ) )
24 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 ) ) } ) }
25 23 24 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 ) ) } ) ) )