Metamath Proof Explorer

Theorem tgaasne

Description: Two DISTINCT points F and H on one half-line from E , subtending congruent angles at a point D off the line, are contradictory. ishlg unfolds the half-line to "one of them is strictly between E and the other" -- both sub-branches are proved, each by tgaasexc on its own triangle, and they are not permutations of one another: the second needs the non-collinearity transported to line E H by cgrancol . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgaasne.p 
|- P = ( Base ` G )
tgaasne.m 
|- .- = ( dist ` G )
tgaasne.i 
|- I = ( Itv ` G )
tgaasne.l 
|- L = ( LineG ` G )
tgaasne.k 
|- K = ( hlG ` G )
tgaasne.g 
|- ( ph -> G e. TarskiG )
tgaasne.d 
|- ( ph -> D e. P )
tgaasne.e 
|- ( ph -> E e. P )
tgaasne.f 
|- ( ph -> F e. P )
tgaasne.h 
|- ( ph -> H e. P )
tgaasne.1 
|- ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
tgaasne.2 
|- ( ph -> H ( K ` E ) F )
tgaasne.3 
|- ( ph -> F =/= H )
tgaasne.4 
|- ( ph -> <" D F E "> ( cgrA ` G ) <" D H E "> )
Assertion tgaasne 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 tgaasne.p 
 |-  P = ( Base ` G )
2 tgaasne.m 
 |-  .- = ( dist ` G )
3 tgaasne.i 
 |-  I = ( Itv ` G )
4 tgaasne.l 
 |-  L = ( LineG ` G )
5 tgaasne.k 
 |-  K = ( hlG ` G )
6 tgaasne.g 
 |-  ( ph -> G e. TarskiG )
7 tgaasne.d 
 |-  ( ph -> D e. P )
8 tgaasne.e 
 |-  ( ph -> E e. P )
9 tgaasne.f 
 |-  ( ph -> F e. P )
10 tgaasne.h 
 |-  ( ph -> H e. P )
11 tgaasne.1 
 |-  ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
12 tgaasne.2 
 |-  ( ph -> H ( K ` E ) F )
13 tgaasne.3 
 |-  ( ph -> F =/= H )
14 tgaasne.4 
 |-  ( ph -> <" D F E "> ( cgrA ` G ) <" D H E "> )
15 6 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> G e. TarskiG )
16 7 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> D e. P )
17 8 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> E e. P )
18 10 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> H e. P )
19 9 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> F e. P )
20 11 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> -. ( D e. ( E L F ) \/ E = F ) )
21 simpr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> H e. ( E I F ) )
22 1 3 5 10 9 8 6 ishlg 
 |-  ( ph -> ( H ( K ` E ) F <-> ( H =/= E /\ F =/= E /\ ( H e. ( E I F ) \/ F e. ( E I H ) ) ) ) )
23 12 22 mpbid 
 |-  ( ph -> ( H =/= E /\ F =/= E /\ ( H e. ( E I F ) \/ F e. ( E I H ) ) ) )
24 23 simp1d 
 |-  ( ph -> H =/= E )
25 24 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> H =/= E )
26 13 necomd 
 |-  ( ph -> H =/= F )
27 26 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> H =/= F )
28 14 adantr 
 |-  ( ( ph /\ H e. ( E I F ) ) -> <" D F E "> ( cgrA ` G ) <" D H E "> )
29 1 2 3 4 15 16 17 18 19 20 21 25 27 28 tgaasexc 
 |-  ( ( ph /\ H e. ( E I F ) ) -> ps )
30 6 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> G e. TarskiG )
31 7 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> D e. P )
32 8 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> E e. P )
33 9 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> F e. P )
34 10 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> H e. P )
35 1 3 2 6 7 9 8 7 10 8 14 cgraswaplr 
 |-  ( ph -> <" E F D "> ( cgrA ` G ) <" E H D "> )
36 1 3 2 6 8 9 7 8 10 7 35 4 11 cgrancol 
 |-  ( ph -> -. ( D e. ( E L H ) \/ E = H ) )
37 36 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> -. ( D e. ( E L H ) \/ E = H ) )
38 simpr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> F e. ( E I H ) )
39 23 simp2d 
 |-  ( ph -> F =/= E )
40 39 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> F =/= E )
41 13 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> F =/= H )
42 1 3 6 5 7 9 8 7 10 8 14 cgracom 
 |-  ( ph -> <" D H E "> ( cgrA ` G ) <" D F E "> )
43 42 adantr 
 |-  ( ( ph /\ F e. ( E I H ) ) -> <" D H E "> ( cgrA ` G ) <" D F E "> )
44 1 2 3 4 30 31 32 33 34 37 38 40 41 43 tgaasexc 
 |-  ( ( ph /\ F e. ( E I H ) ) -> ps )
45 23 simp3d 
 |-  ( ph -> ( H e. ( E I F ) \/ F e. ( E I H ) ) )
46 29 44 45 mpjaodan 
 |-  ( ph -> ps )