Metamath Proof Explorer

Theorem cgracol

Description: Angle congruence preserves colinearity. (Contributed by Thierry Arnoux, 9-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 cgracol.p 
 |-  P = ( Base ` G )
2 cgracol.i 
 |-  I = ( Itv ` G )
3 cgracol.m 
 |-  .- = ( dist ` G )
4 cgracol.g 
 |-  ( ph -> G e. TarskiG )
5 cgracol.a 
 |-  ( ph -> A e. P )
6 cgracol.b 
 |-  ( ph -> B e. P )
7 cgracol.c 
 |-  ( ph -> C e. P )
8 cgracol.d 
 |-  ( ph -> D e. P )
9 cgracol.e 
 |-  ( ph -> E e. P )
10 cgracol.f 
 |-  ( ph -> F e. P )
11 cgracol.1 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
12 cgracol.l 
 |-  L = ( LineG ` G )
13 cgracol.2 
 |-  ( ph -> ( C e. ( A L B ) \/ A = B ) )
14 4 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> G e. TarskiG )
15 5 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> A e. P )
16 6 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> B e. P )
17 7 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> C e. P )
18 8 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> D e. P )
19 9 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> E e. P )
20 10 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> F e. P )
21 11 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
22 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
23 1 2 22 4 5 6 7 8 9 10 11 cgrane2 
 |-  ( ph -> B =/= C )
24 23 necomd 
 |-  ( ph -> C =/= B )
25 24 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C =/= B )
26 1 2 22 4 5 6 7 8 9 10 11 cgrane1 
 |-  ( ph -> A =/= B )
27 26 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> A =/= B )
28 4 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> G e. TarskiG )
29 5 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> A e. P )
30 7 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. P )
31 6 adantr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> B e. P )
32 simpr 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. ( A I B ) )
33 1 3 2 28 29 30 31 32 tgbtwncom 
 |-  ( ( ph /\ C e. ( A I B ) ) -> C e. ( B I A ) )
34 33 orcd 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( C e. ( B I A ) \/ A e. ( B I C ) ) )
35 25 27 34 3jca 
 |-  ( ( ph /\ C e. ( A I B ) ) -> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) )
36 24 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> C =/= B )
37 26 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A =/= B )
38 4 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> G e. TarskiG )
39 7 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> C e. P )
40 5 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. P )
41 6 adantr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> B e. P )
42 simpr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. ( C I B ) )
43 1 3 2 38 39 40 41 42 tgbtwncom 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. ( B I C ) )
44 43 olcd 
 |-  ( ( ph /\ A e. ( C I B ) ) -> ( C e. ( B I A ) \/ A e. ( B I C ) ) )
45 36 37 44 3jca 
 |-  ( ( ph /\ A e. ( C I B ) ) -> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) )
46 35 45 jaodan 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) )
47 1 2 22 7 5 6 4 ishlg 
 |-  ( ph -> ( C ( ( hlG ` G ) ` B ) A <-> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) ) )
48 47 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( C ( ( hlG ` G ) ` B ) A <-> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) ) )
49 46 48 mpbird 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> C ( ( hlG ` G ) ` B ) A )
50 1 2 22 17 15 16 14 49 hlcomd 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> A ( ( hlG ` G ) ` B ) C )
51 1 2 3 14 15 16 17 18 19 20 21 22 50 cgrahl 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> D ( ( hlG ` G ) ` E ) F )
52 1 2 22 18 20 19 14 ishlg 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( D ( ( hlG ` G ) ` E ) F <-> ( D =/= E /\ F =/= E /\ ( D e. ( E I F ) \/ F e. ( E I D ) ) ) ) )
53 51 52 mpbid 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( D =/= E /\ F =/= E /\ ( D e. ( E I F ) \/ F e. ( E I D ) ) ) )
54 53 simp3d 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( D e. ( E I F ) \/ F e. ( E I D ) ) )
55 4 adantr 
 |-  ( ( ph /\ D e. ( E I F ) ) -> G e. TarskiG )
56 9 adantr 
 |-  ( ( ph /\ D e. ( E I F ) ) -> E e. P )
57 8 adantr 
 |-  ( ( ph /\ D e. ( E I F ) ) -> D e. P )
58 10 adantr 
 |-  ( ( ph /\ D e. ( E I F ) ) -> F e. P )
59 simpr 
 |-  ( ( ph /\ D e. ( E I F ) ) -> D e. ( E I F ) )
60 1 3 2 55 56 57 58 59 tgbtwncom 
 |-  ( ( ph /\ D e. ( E I F ) ) -> D e. ( F I E ) )
61 60 olcd 
 |-  ( ( ph /\ D e. ( E I F ) ) -> ( F e. ( D I E ) \/ D e. ( F I E ) ) )
62 4 adantr 
 |-  ( ( ph /\ F e. ( E I D ) ) -> G e. TarskiG )
63 9 adantr 
 |-  ( ( ph /\ F e. ( E I D ) ) -> E e. P )
64 10 adantr 
 |-  ( ( ph /\ F e. ( E I D ) ) -> F e. P )
65 8 adantr 
 |-  ( ( ph /\ F e. ( E I D ) ) -> D e. P )
66 simpr 
 |-  ( ( ph /\ F e. ( E I D ) ) -> F e. ( E I D ) )
67 1 3 2 62 63 64 65 66 tgbtwncom 
 |-  ( ( ph /\ F e. ( E I D ) ) -> F e. ( D I E ) )
68 67 orcd 
 |-  ( ( ph /\ F e. ( E I D ) ) -> ( F e. ( D I E ) \/ D e. ( F I E ) ) )
69 61 68 jaodan 
 |-  ( ( ph /\ ( D e. ( E I F ) \/ F e. ( E I D ) ) ) -> ( F e. ( D I E ) \/ D e. ( F I E ) ) )
70 54 69 syldan 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( F e. ( D I E ) \/ D e. ( F I E ) ) )
71 70 orcd 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( ( F e. ( D I E ) \/ D e. ( F I E ) ) \/ E e. ( D I F ) ) )
72 df-3or 
 |-  ( ( F e. ( D I E ) \/ D e. ( F I E ) \/ E e. ( D I F ) ) <-> ( ( F e. ( D I E ) \/ D e. ( F I E ) ) \/ E e. ( D I F ) ) )
73 71 72 sylibr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( F e. ( D I E ) \/ D e. ( F I E ) \/ E e. ( D I F ) ) )
74 1 2 4 22 5 6 7 8 9 10 11 cgracom 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" A B C "> )
75 1 2 22 4 8 9 10 5 6 7 74 cgrane1 
 |-  ( ph -> D =/= E )
76 1 12 2 4 8 9 75 10 tgellng 
 |-  ( ph -> ( F e. ( D L E ) <-> ( F e. ( D I E ) \/ D e. ( F I E ) \/ E e. ( D I F ) ) ) )
77 76 adantr 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( F e. ( D L E ) <-> ( F e. ( D I E ) \/ D e. ( F I E ) \/ E e. ( D I F ) ) ) )
78 73 77 mpbird 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> F e. ( D L E ) )
79 78 orcd 
 |-  ( ( ph /\ ( C e. ( A I B ) \/ A e. ( C I B ) ) ) -> ( F e. ( D L E ) \/ D = E ) )
80 4 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> G e. TarskiG )
81 8 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> D e. P )
82 9 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> E e. P )
83 10 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> F e. P )
84 5 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> A e. P )
85 6 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. P )
86 7 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> C e. P )
87 11 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> <" A B C "> ( cgrA ` G ) <" D E F "> )
88 simpr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( A I C ) )
89 1 2 3 80 84 85 86 81 82 83 87 88 cgrabtwn 
 |-  ( ( ph /\ B e. ( A I C ) ) -> E e. ( D I F ) )
90 1 12 2 80 81 82 83 89 btwncolg3 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( F e. ( D L E ) \/ D = E ) )
91 26 neneqd 
 |-  ( ph -> -. A = B )
92 13 orcomd 
 |-  ( ph -> ( A = B \/ C e. ( A L B ) ) )
93 92 ord 
 |-  ( ph -> ( -. A = B -> C e. ( A L B ) ) )
94 91 93 mpd 
 |-  ( ph -> C e. ( A L B ) )
95 1 12 2 4 5 6 26 7 tgellng 
 |-  ( ph -> ( C e. ( A L B ) <-> ( C e. ( A I B ) \/ A e. ( C I B ) \/ B e. ( A I C ) ) ) )
96 94 95 mpbid 
 |-  ( ph -> ( C e. ( A I B ) \/ A e. ( C I B ) \/ B e. ( A I C ) ) )
97 df-3or 
 |-  ( ( C e. ( A I B ) \/ A e. ( C I B ) \/ B e. ( A I C ) ) <-> ( ( C e. ( A I B ) \/ A e. ( C I B ) ) \/ B e. ( A I C ) ) )
98 96 97 sylib 
 |-  ( ph -> ( ( C e. ( A I B ) \/ A e. ( C I B ) ) \/ B e. ( A I C ) ) )
99 79 90 98 mpjaodan 
 |-  ( ph -> ( F e. ( D L E ) \/ D = E ) )