Metamath Proof Explorer

Theorem tglngval

Description: The line going through points X and Y . (Contributed by Thierry Arnoux, 28-Mar-2019)

Ref Expression
Hypotheses tglngval.p 
|- P = ( Base ` G )
tglngval.l 
|- L = ( LineG ` G )
tglngval.i 
|- I = ( Itv ` G )
tglngval.g 
|- ( ph -> G e. TarskiG )
tglngval.x 
|- ( ph -> X e. P )
tglngval.y 
|- ( ph -> Y e. P )
tglngval.z 
|- ( ph -> X =/= Y )
Assertion tglngval 
|- ( ph -> ( X L Y ) = { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } )

Proof

Step Hyp Ref Expression
1 tglngval.p 
 |-  P = ( Base ` G )
2 tglngval.l 
 |-  L = ( LineG ` G )
3 tglngval.i 
 |-  I = ( Itv ` G )
4 tglngval.g 
 |-  ( ph -> G e. TarskiG )
5 tglngval.x 
 |-  ( ph -> X e. P )
6 tglngval.y 
 |-  ( ph -> Y e. P )
7 tglngval.z 
 |-  ( ph -> X =/= Y )
8 1 2 3 tglng 
 |-  ( G e. TarskiG -> L = ( 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 ) ) } ) )
9 4 8 syl 
 |-  ( ph -> L = ( 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 ) ) } ) )
10 9 oveqd 
 |-  ( ph -> ( X L Y ) = ( X ( 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 ) ) } ) Y ) )
11 7 necomd 
 |-  ( ph -> Y =/= X )
12 eldifsn 
 |-  ( Y e. ( P \ { X } ) <-> ( Y e. P /\ Y =/= X ) )
13 6 11 12 sylanbrc 
 |-  ( ph -> Y e. ( P \ { X } ) )
14 1 fvexi 
 |-  P e. _V
15 14 rabex 
 |-  { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } e. _V
16 15 a1i 
 |-  ( ph -> { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } e. _V )
17 oveq12 
 |-  ( ( x = X /\ y = Y ) -> ( x I y ) = ( X I Y ) )
18 17 eleq2d 
 |-  ( ( x = X /\ y = Y ) -> ( z e. ( x I y ) <-> z e. ( X I Y ) ) )
19 simpl 
 |-  ( ( x = X /\ y = Y ) -> x = X )
20 simpr 
 |-  ( ( x = X /\ y = Y ) -> y = Y )
21 20 oveq2d 
 |-  ( ( x = X /\ y = Y ) -> ( z I y ) = ( z I Y ) )
22 19 21 eleq12d 
 |-  ( ( x = X /\ y = Y ) -> ( x e. ( z I y ) <-> X e. ( z I Y ) ) )
23 19 oveq1d 
 |-  ( ( x = X /\ y = Y ) -> ( x I z ) = ( X I z ) )
24 20 23 eleq12d 
 |-  ( ( x = X /\ y = Y ) -> ( y e. ( x I z ) <-> Y e. ( X I z ) ) )
25 18 22 24 3orbi123d 
 |-  ( ( x = X /\ y = Y ) -> ( ( 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 ) ) ) )
26 25 rabbidv 
 |-  ( ( x = X /\ y = Y ) -> { 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 ) ) } )
27 sneq 
 |-  ( x = X -> { x } = { X } )
28 27 difeq2d 
 |-  ( x = X -> ( P \ { x } ) = ( P \ { X } ) )
29 eqid 
 |-  ( 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 ) ) } )
30 26 28 29 ovmpox 
 |-  ( ( 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 ) ) } e. _V ) -> ( X ( 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 ) ) } ) Y ) = { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } )
31 5 13 16 30 syl3anc 
 |-  ( ph -> ( X ( 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 ) ) } ) Y ) = { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } )
32 10 31 eqtrd 
 |-  ( ph -> ( X L Y ) = { z e. P | ( z e. ( X I Y ) \/ X e. ( z I Y ) \/ Y e. ( X I z ) ) } )