Metamath Proof Explorer

Theorem lnext

Description: Extend a line with a missing point. Theorem 4.14 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-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 )
tgcolg.z 
|- ( ph -> Z e. P )
lnxfr.r 
|- .~ = ( cgrG ` G )
lnxfr.a 
|- ( ph -> A e. P )
lnxfr.b 
|- ( ph -> B e. P )
lnxfr.d 
|- .- = ( dist ` G )
lnext.1 
|- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
lnext.2 
|- ( ph -> ( X .- Y ) = ( A .- B ) )
Assertion lnext 
|- ( ph -> E. c e. P <" X Y Z "> .~ <" A B c "> )

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 tgcolg.z 
 |-  ( ph -> Z e. P )
8 lnxfr.r 
 |-  .~ = ( cgrG ` G )
9 lnxfr.a 
 |-  ( ph -> A e. P )
10 lnxfr.b 
 |-  ( ph -> B e. P )
11 lnxfr.d 
 |-  .- = ( dist ` G )
12 lnext.1 
 |-  ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
13 lnext.2 
 |-  ( ph -> ( X .- Y ) = ( A .- B ) )
14 1 11 3 4 9 10 6 7 axtgsegcon 
 |-  ( ph -> E. c e. P ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) )
15 14 adantr 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> E. c e. P ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) )
16 4 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> G e. TarskiG )
17 5 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> X e. P )
18 6 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> Y e. P )
19 7 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> Z e. P )
20 9 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> A e. P )
21 10 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> B e. P )
22 simplr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> c e. P )
23 13 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> ( X .- Y ) = ( A .- B ) )
24 simprr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> ( B .- c ) = ( Y .- Z ) )
25 24 eqcomd 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> ( Y .- Z ) = ( B .- c ) )
26 simpllr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> Y e. ( X I Z ) )
27 simprl 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> B e. ( A I c ) )
28 1 11 3 16 17 18 19 20 21 22 26 27 23 25 tgcgrextend 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> ( X .- Z ) = ( A .- c ) )
29 1 11 3 16 17 19 20 22 28 tgcgrcomlr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> ( Z .- X ) = ( c .- A ) )
30 1 11 8 16 17 18 19 20 21 22 23 25 29 trgcgr 
 |-  ( ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) /\ ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) ) -> <" X Y Z "> .~ <" A B c "> )
31 30 ex 
 |-  ( ( ( ph /\ Y e. ( X I Z ) ) /\ c e. P ) -> ( ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) -> <" X Y Z "> .~ <" A B c "> ) )
32 31 reximdva 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> ( E. c e. P ( B e. ( A I c ) /\ ( B .- c ) = ( Y .- Z ) ) -> E. c e. P <" X Y Z "> .~ <" A B c "> ) )
33 15 32 mpd 
 |-  ( ( ph /\ Y e. ( X I Z ) ) -> E. c e. P <" X Y Z "> .~ <" A B c "> )
34 1 11 3 4 10 9 5 7 axtgsegcon 
 |-  ( ph -> E. c e. P ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) )
35 34 adantr 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> E. c e. P ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) )
36 4 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> G e. TarskiG )
37 5 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> X e. P )
38 6 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> Y e. P )
39 7 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> Z e. P )
40 9 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> A e. P )
41 10 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> B e. P )
42 simplr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> c e. P )
43 13 ad3antrrr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> ( X .- Y ) = ( A .- B ) )
44 simpllr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> X e. ( Y I Z ) )
45 simprl 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> A e. ( B I c ) )
46 1 11 3 36 37 38 40 41 43 tgcgrcomlr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> ( Y .- X ) = ( B .- A ) )
47 simprr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> ( A .- c ) = ( X .- Z ) )
48 47 eqcomd 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> ( X .- Z ) = ( A .- c ) )
49 1 11 3 36 38 37 39 41 40 42 44 45 46 48 tgcgrextend 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> ( Y .- Z ) = ( B .- c ) )
50 1 11 3 36 37 39 40 42 48 tgcgrcomlr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> ( Z .- X ) = ( c .- A ) )
51 1 11 8 36 37 38 39 40 41 42 43 49 50 trgcgr 
 |-  ( ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) /\ ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) ) -> <" X Y Z "> .~ <" A B c "> )
52 51 ex 
 |-  ( ( ( ph /\ X e. ( Y I Z ) ) /\ c e. P ) -> ( ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) -> <" X Y Z "> .~ <" A B c "> ) )
53 52 reximdva 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> ( E. c e. P ( A e. ( B I c ) /\ ( A .- c ) = ( X .- Z ) ) -> E. c e. P <" X Y Z "> .~ <" A B c "> ) )
54 35 53 mpd 
 |-  ( ( ph /\ X e. ( Y I Z ) ) -> E. c e. P <" X Y Z "> .~ <" A B c "> )
55 4 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> G e. TarskiG )
56 5 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> X e. P )
57 7 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. P )
58 6 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Y e. P )
59 9 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> A e. P )
60 10 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> B e. P )
61 simpr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> Z e. ( X I Y ) )
62 13 adantr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( X .- Y ) = ( A .- B ) )
63 1 11 3 8 55 56 57 58 59 60 61 62 tgcgrxfr 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> E. c e. P ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) )
64 4 ad3antrrr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> G e. TarskiG )
65 5 ad3antrrr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> X e. P )
66 7 ad3antrrr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> Z e. P )
67 6 ad3antrrr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> Y e. P )
68 9 ad3antrrr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> A e. P )
69 simplr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> c e. P )
70 10 ad3antrrr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> B e. P )
71 simprr 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> <" X Z Y "> .~ <" A c B "> )
72 1 11 3 8 64 65 66 67 68 69 70 71 cgr3swap23 
 |-  ( ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) /\ ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) ) -> <" X Y Z "> .~ <" A B c "> )
73 72 ex 
 |-  ( ( ( ph /\ Z e. ( X I Y ) ) /\ c e. P ) -> ( ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) -> <" X Y Z "> .~ <" A B c "> ) )
74 73 reximdva 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> ( E. c e. P ( c e. ( A I B ) /\ <" X Z Y "> .~ <" A c B "> ) -> E. c e. P <" X Y Z "> .~ <" A B c "> ) )
75 63 74 mpd 
 |-  ( ( ph /\ Z e. ( X I Y ) ) -> E. c e. P <" X Y Z "> .~ <" A B c "> )
76 1 2 3 4 5 7 6 tgcolg 
 |-  ( ph -> ( ( Y e. ( X L Z ) \/ X = Z ) <-> ( Y e. ( X I Z ) \/ X e. ( Y I Z ) \/ Z e. ( X I Y ) ) ) )
77 12 76 mpbid 
 |-  ( ph -> ( Y e. ( X I Z ) \/ X e. ( Y I Z ) \/ Z e. ( X I Y ) ) )
78 33 54 75 77 mpjao3dan 
 |-  ( ph -> E. c e. P <" X Y Z "> .~ <" A B c "> )