Metamath Proof Explorer

Theorem tgcgrxfr

Description: A line segment can be divided at the same place as a congruent line segment is divided. Theorem 4.5 of Schwabhauser p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019)

Ref Expression
Hypotheses tgcgrxfr.p 
|- P = ( Base ` G )
tgcgrxfr.m 
|- .- = ( dist ` G )
tgcgrxfr.i 
|- I = ( Itv ` G )
tgcgrxfr.r 
|- .~ = ( cgrG ` G )
tgcgrxfr.g 
|- ( ph -> G e. TarskiG )
tgcgrxfr.a 
|- ( ph -> A e. P )
tgcgrxfr.b 
|- ( ph -> B e. P )
tgcgrxfr.c 
|- ( ph -> C e. P )
tgcgrxfr.d 
|- ( ph -> D e. P )
tgcgrxfr.f 
|- ( ph -> F e. P )
tgcgrxfr.1 
|- ( ph -> B e. ( A I C ) )
tgcgrxfr.2 
|- ( ph -> ( A .- C ) = ( D .- F ) )
Assertion tgcgrxfr 
|- ( ph -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )

Proof

Step Hyp Ref Expression
1 tgcgrxfr.p 
 |-  P = ( Base ` G )
2 tgcgrxfr.m 
 |-  .- = ( dist ` G )
3 tgcgrxfr.i 
 |-  I = ( Itv ` G )
4 tgcgrxfr.r 
 |-  .~ = ( cgrG ` G )
5 tgcgrxfr.g 
 |-  ( ph -> G e. TarskiG )
6 tgcgrxfr.a 
 |-  ( ph -> A e. P )
7 tgcgrxfr.b 
 |-  ( ph -> B e. P )
8 tgcgrxfr.c 
 |-  ( ph -> C e. P )
9 tgcgrxfr.d 
 |-  ( ph -> D e. P )
10 tgcgrxfr.f 
 |-  ( ph -> F e. P )
11 tgcgrxfr.1 
 |-  ( ph -> B e. ( A I C ) )
12 tgcgrxfr.2 
 |-  ( ph -> ( A .- C ) = ( D .- F ) )
13 6 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> A e. P )
14 5 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> G e. TarskiG )
15 9 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> D e. P )
16 10 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> F e. P )
17 simpr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( # ` P ) = 1 )
18 1 2 3 14 13 15 16 17 tgldim0itv 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> A e. ( D I F ) )
19 7 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> B e. P )
20 8 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> C e. P )
21 1 2 3 14 13 19 15 17 13 tgldim0cgr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( A .- B ) = ( D .- A ) )
22 1 2 3 14 19 20 13 17 16 tgldim0cgr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( B .- C ) = ( A .- F ) )
23 1 2 3 14 20 13 16 17 15 tgldim0cgr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( C .- A ) = ( F .- D ) )
24 1 2 4 14 13 19 20 15 13 16 21 22 23 trgcgr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> <" A B C "> .~ <" D A F "> )
25 eleq1 
 |-  ( e = A -> ( e e. ( D I F ) <-> A e. ( D I F ) ) )
26 s3eq2 
 |-  ( e = A -> <" D e F "> = <" D A F "> )
27 26 breq2d 
 |-  ( e = A -> ( <" A B C "> .~ <" D e F "> <-> <" A B C "> .~ <" D A F "> ) )
28 25 27 anbi12d 
 |-  ( e = A -> ( ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) <-> ( A e. ( D I F ) /\ <" A B C "> .~ <" D A F "> ) ) )
29 28 rspcev 
 |-  ( ( A e. P /\ ( A e. ( D I F ) /\ <" A B C "> .~ <" D A F "> ) ) -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
30 13 18 24 29 syl12anc 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
31 5 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> G e. TarskiG )
32 simplr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> g e. P )
33 9 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> D e. P )
34 6 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> A e. P )
35 7 ad3antrrr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> B e. P )
36 1 2 3 31 32 33 34 35 axtgsegcon 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> E. e e. P ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) )
37 5 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> G e. TarskiG )
38 32 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) -> g e. P )
39 38 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> g e. P )
40 9 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> D e. P )
41 simplr 
 |-  ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) -> e e. P )
42 41 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> e e. P )
43 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> f e. P )
44 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) )
45 44 simpld 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> D e. ( g I e ) )
46 simprl 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> e e. ( g I f ) )
47 1 2 3 37 39 40 42 43 45 46 tgbtwnexch3 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> e e. ( D I f ) )
48 6 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> A e. P )
49 8 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> C e. P )
50 10 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> F e. P )
51 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( D e. ( F I g ) /\ D =/= g ) )
52 51 simprd 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> D =/= g )
53 52 necomd 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> g =/= D )
54 1 2 3 37 39 40 42 43 45 46 tgbtwnexch 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> D e. ( g I f ) )
55 51 simpld 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> D e. ( F I g ) )
56 1 2 3 37 50 40 39 55 tgbtwncom 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> D e. ( g I F ) )
57 7 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> B e. P )
58 11 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> B e. ( A I C ) )
59 44 simprd 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( D .- e ) = ( A .- B ) )
60 simprr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( e .- f ) = ( B .- C ) )
61 1 2 3 37 40 42 43 48 57 49 47 58 59 60 tgcgrextend 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( D .- f ) = ( A .- C ) )
62 12 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( A .- C ) = ( D .- F ) )
63 62 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( D .- F ) = ( A .- C ) )
64 1 2 3 37 40 48 49 39 43 50 53 54 56 61 63 tgsegconeq 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> f = F )
65 64 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( D I f ) = ( D I F ) )
66 47 65 eleqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> e e. ( D I F ) )
67 59 eqcomd 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( A .- B ) = ( D .- e ) )
68 64 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( e .- f ) = ( e .- F ) )
69 60 68 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( B .- C ) = ( e .- F ) )
70 1 2 3 5 6 8 9 10 12 tgcgrcomlr 
 |-  ( ph -> ( C .- A ) = ( F .- D ) )
71 70 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( C .- A ) = ( F .- D ) )
72 1 2 4 37 48 57 49 40 42 50 67 69 71 trgcgr 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> <" A B C "> .~ <" D e F "> )
73 66 72 jca 
 |-  ( ( ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) /\ f e. P ) /\ ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) ) -> ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
74 31 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) -> G e. TarskiG )
75 35 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) -> B e. P )
76 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) -> C e. P )
77 1 2 3 74 38 41 75 76 axtgsegcon 
 |-  ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) -> E. f e. P ( e e. ( g I f ) /\ ( e .- f ) = ( B .- C ) ) )
78 73 77 r19.29a 
 |-  ( ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) /\ ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) ) -> ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
79 78 ex 
 |-  ( ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) /\ e e. P ) -> ( ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) -> ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) )
80 79 reximdva 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> ( E. e e. P ( D e. ( g I e ) /\ ( D .- e ) = ( A .- B ) ) -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) ) )
81 36 80 mpd 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ g e. P ) /\ ( D e. ( F I g ) /\ D =/= g ) ) -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
82 5 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> G e. TarskiG )
83 10 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> F e. P )
84 9 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> D e. P )
85 simpr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) )
86 1 2 3 82 83 84 85 tgbtwndiff 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> E. g e. P ( D e. ( F I g ) /\ D =/= g ) )
87 81 86 r19.29a 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )
88 1 6 tgldimor 
 |-  ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )
89 30 87 88 mpjaodan 
 |-  ( ph -> E. e e. P ( e e. ( D I F ) /\ <" A B C "> .~ <" D e F "> ) )