Metamath Proof Explorer

Theorem tglineelsb2

Description: If S lies on PQ , then PQ = PS . Theorem 6.16 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 17-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 )
tglineelsb2.3 
|- ( ph -> S e. B )
tglineelsb2.5 
|- ( ph -> S =/= P )
tglineelsb2.6 
|- ( ph -> S e. ( P L Q ) )
Assertion tglineelsb2 
|- ( ph -> ( P L Q ) = ( P L S ) )

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 tglineelsb2.3 
 |-  ( ph -> S e. B )
9 tglineelsb2.5 
 |-  ( ph -> S =/= P )
10 tglineelsb2.6 
 |-  ( ph -> S e. ( P L Q ) )
11 4 adantr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> G e. TarskiG )
12 5 adantr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> P e. B )
13 8 adantr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> S e. B )
14 9 necomd 
 |-  ( ph -> P =/= S )
15 14 adantr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> P =/= S )
16 6 adantr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> Q e. B )
17 7 necomd 
 |-  ( ph -> Q =/= P )
18 17 adantr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> Q =/= P )
19 10 adantr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> S e. ( P L Q ) )
20 1 2 3 11 16 12 13 18 19 lncom 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> S e. ( Q L P ) )
21 1 2 3 11 12 13 16 15 20 18 lnrot1 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> Q e. ( P L S ) )
22 1 3 2 4 5 6 7 tglnssp 
 |-  ( ph -> ( P L Q ) C_ B )
23 22 sselda 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> x e. B )
24 simpr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> x e. ( P L Q ) )
25 1 2 3 11 12 13 15 16 18 21 23 24 tglineeltr 
 |-  ( ( ph /\ x e. ( P L Q ) ) -> x e. ( P L S ) )
26 4 adantr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> G e. TarskiG )
27 5 adantr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> P e. B )
28 6 adantr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> Q e. B )
29 7 adantr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> P =/= Q )
30 8 adantr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> S e. B )
31 9 adantr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> S =/= P )
32 10 adantr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> S e. ( P L Q ) )
33 1 3 2 4 5 8 14 tglnssp 
 |-  ( ph -> ( P L S ) C_ B )
34 33 sselda 
 |-  ( ( ph /\ x e. ( P L S ) ) -> x e. B )
35 simpr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> x e. ( P L S ) )
36 1 2 3 26 27 28 29 30 31 32 34 35 tglineeltr 
 |-  ( ( ph /\ x e. ( P L S ) ) -> x e. ( P L Q ) )
37 25 36 impbida 
 |-  ( ph -> ( x e. ( P L Q ) <-> x e. ( P L S ) ) )
38 37 eqrdv 
 |-  ( ph -> ( P L Q ) = ( P L S ) )