Metamath Proof Explorer

Theorem tglineinteq

Description: Two distinct lines intersect in at most one point. Theorem 6.21 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 6-Aug-2019)

Ref Expression
Hypotheses tglineintmo.p 
|- P = ( Base ` G )
tglineintmo.i 
|- I = ( Itv ` G )
tglineintmo.l 
|- L = ( LineG ` G )
tglineintmo.g 
|- ( ph -> G e. TarskiG )
tglineinteq.a 
|- ( ph -> A e. P )
tglineinteq.b 
|- ( ph -> B e. P )
tglineinteq.c 
|- ( ph -> C e. P )
tglineinteq.d 
|- ( ph -> D e. P )
tglineinteq.e 
|- ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
tglineinteq.1 
|- ( ph -> X e. ( A L B ) )
tglineinteq.2 
|- ( ph -> Y e. ( A L B ) )
tglineinteq.3 
|- ( ph -> X e. ( C L D ) )
tglineinteq.4 
|- ( ph -> Y e. ( C L D ) )
Assertion tglineinteq 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 tglineintmo.p 
 |-  P = ( Base ` G )
2 tglineintmo.i 
 |-  I = ( Itv ` G )
3 tglineintmo.l 
 |-  L = ( LineG ` G )
4 tglineintmo.g 
 |-  ( ph -> G e. TarskiG )
5 tglineinteq.a 
 |-  ( ph -> A e. P )
6 tglineinteq.b 
 |-  ( ph -> B e. P )
7 tglineinteq.c 
 |-  ( ph -> C e. P )
8 tglineinteq.d 
 |-  ( ph -> D e. P )
9 tglineinteq.e 
 |-  ( ph -> -. ( A e. ( B L C ) \/ B = C ) )
10 tglineinteq.1 
 |-  ( ph -> X e. ( A L B ) )
11 tglineinteq.2 
 |-  ( ph -> Y e. ( A L B ) )
12 tglineinteq.3 
 |-  ( ph -> X e. ( C L D ) )
13 tglineinteq.4 
 |-  ( ph -> Y e. ( C L D ) )
14 1 3 2 4 5 6 10 tglngne 
 |-  ( ph -> A =/= B )
15 1 2 3 4 5 6 14 tgelrnln 
 |-  ( ph -> ( A L B ) e. ran L )
16 1 3 2 4 7 8 12 tglngne 
 |-  ( ph -> C =/= D )
17 1 2 3 4 7 8 16 tgelrnln 
 |-  ( ph -> ( C L D ) e. ran L )
18 1 2 3 4 5 6 7 8 9 tglineneq 
 |-  ( ph -> ( A L B ) =/= ( C L D ) )
19 1 2 3 4 15 17 18 tglineintmo 
 |-  ( ph -> E* x ( x e. ( A L B ) /\ x e. ( C L D ) ) )
20 10 12 jca 
 |-  ( ph -> ( X e. ( A L B ) /\ X e. ( C L D ) ) )
21 11 13 jca 
 |-  ( ph -> ( Y e. ( A L B ) /\ Y e. ( C L D ) ) )
22 eleq1 
 |-  ( x = X -> ( x e. ( A L B ) <-> X e. ( A L B ) ) )
23 eleq1 
 |-  ( x = X -> ( x e. ( C L D ) <-> X e. ( C L D ) ) )
24 22 23 anbi12d 
 |-  ( x = X -> ( ( x e. ( A L B ) /\ x e. ( C L D ) ) <-> ( X e. ( A L B ) /\ X e. ( C L D ) ) ) )
25 eleq1 
 |-  ( x = Y -> ( x e. ( A L B ) <-> Y e. ( A L B ) ) )
26 eleq1 
 |-  ( x = Y -> ( x e. ( C L D ) <-> Y e. ( C L D ) ) )
27 25 26 anbi12d 
 |-  ( x = Y -> ( ( x e. ( A L B ) /\ x e. ( C L D ) ) <-> ( Y e. ( A L B ) /\ Y e. ( C L D ) ) ) )
28 24 27 moi 
 |-  ( ( ( X e. ( A L B ) /\ Y e. ( A L B ) ) /\ E* x ( x e. ( A L B ) /\ x e. ( C L D ) ) /\ ( ( X e. ( A L B ) /\ X e. ( C L D ) ) /\ ( Y e. ( A L B ) /\ Y e. ( C L D ) ) ) ) -> X = Y )
29 10 11 19 20 21 28 syl212anc 
 |-  ( ph -> X = Y )