Metamath Proof Explorer

Theorem tglinethru

Description: If A is a line containing two distinct points P and Q , then A is the line through P and Q . Theorem 6.18 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 25-May-2019)

Ref Expression
Hypotheses tglineelsb2.p 
|- B = ( Base ` G )
tglineelsb2.i 
|- I = ( Itv ` G )
tglineelsb2.l 
|- L = ( LineG ` G )
tglineelsb2.g 
|- ( ph -> G e. TarskiG )
tglineelsb2.1 
|- ( ph -> P e. B )
tglineelsb2.2 
|- ( ph -> Q e. B )
tglineelsb2.4 
|- ( ph -> P =/= Q )
tglinethru.0 
|- ( ph -> P =/= Q )
tglinethru.1 
|- ( ph -> A e. ran L )
tglinethru.2 
|- ( ph -> P e. A )
tglinethru.3 
|- ( ph -> Q e. A )
Assertion tglinethru 
|- ( ph -> A = ( P L Q ) )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p 
 |-  B = ( Base ` G )
2 tglineelsb2.i 
 |-  I = ( Itv ` G )
3 tglineelsb2.l 
 |-  L = ( LineG ` G )
4 tglineelsb2.g 
 |-  ( ph -> G e. TarskiG )
5 tglineelsb2.1 
 |-  ( ph -> P e. B )
6 tglineelsb2.2 
 |-  ( ph -> Q e. B )
7 tglineelsb2.4 
 |-  ( ph -> P =/= Q )
8 tglinethru.0 
 |-  ( ph -> P =/= Q )
9 tglinethru.1 
 |-  ( ph -> A e. ran L )
10 tglinethru.2 
 |-  ( ph -> P e. A )
11 tglinethru.3 
 |-  ( ph -> Q e. A )
12 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> G e. TarskiG )
13 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> x e. B )
14 simpllr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> y e. B )
15 simplrr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> x =/= y )
16 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> Q e. B )
17 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> P =/= Q )
18 17 necomd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> Q =/= P )
19 simpr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> P = x )
20 18 19 neeqtrd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> Q =/= x )
21 11 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> Q e. A )
22 simplrl 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> A = ( x L y ) )
23 21 22 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> Q e. ( x L y ) )
24 1 2 3 12 13 14 15 16 20 23 tglineelsb2 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> ( x L y ) = ( x L Q ) )
25 19 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> ( P L Q ) = ( x L Q ) )
26 24 22 25 3eqtr4d 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P = x ) -> A = ( P L Q ) )
27 simplrl 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> A = ( x L y ) )
28 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> G e. TarskiG )
29 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> x e. B )
30 simpllr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> y e. B )
31 simplrr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> x =/= y )
32 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> P e. B )
33 simpr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> P =/= x )
34 10 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> P e. A )
35 34 27 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> P e. ( x L y ) )
36 1 2 3 28 29 30 31 32 33 35 tglineelsb2 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> ( x L y ) = ( x L P ) )
37 33 necomd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> x =/= P )
38 1 2 3 28 29 32 37 tglinecom 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> ( x L P ) = ( P L x ) )
39 27 36 38 3eqtrd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> A = ( P L x ) )
40 6 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> Q e. B )
41 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> P =/= Q )
42 41 necomd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> Q =/= P )
43 11 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> Q e. A )
44 43 39 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> Q e. ( P L x ) )
45 1 2 3 28 32 29 33 40 42 44 tglineelsb2 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> ( P L x ) = ( P L Q ) )
46 39 45 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) /\ P =/= x ) -> A = ( P L Q ) )
47 26 46 pm2.61dane 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ ( A = ( x L y ) /\ x =/= y ) ) -> A = ( P L Q ) )
48 1 2 3 4 9 tgisline 
 |-  ( ph -> E. x e. B E. y e. B ( A = ( x L y ) /\ x =/= y ) )
49 47 48 r19.29vva 
 |-  ( ph -> A = ( P L Q ) )