Metamath Proof Explorer

Theorem inagbtwn

Description: A flat sub-angle forces the containing angle flat: if W is inside angle <" D E F "> and E lies between D and W , then E lies between D and F . This is GeoCoq bet__in__angle__bet. Proved by unfolding isinag and following its segment point. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagbtwn.p 
|- P = ( Base ` G )
inagbtwn.i 
|- I = ( Itv ` G )
inagbtwn.k 
|- K = ( hlG ` G )
inagbtwn.g 
|- ( ph -> G e. TarskiG )
inagbtwn.d 
|- ( ph -> D e. P )
inagbtwn.e 
|- ( ph -> E e. P )
inagbtwn.f 
|- ( ph -> F e. P )
inagbtwn.w 
|- ( ph -> W e. P )
inagbtwn.in 
|- ( ph -> W ( inA ` G ) <" D E F "> )
inagbtwn.1 
|- ( ph -> E e. ( D I W ) )
Assertion inagbtwn 
|- ( ph -> E e. ( D I F ) )

Proof

Step Hyp Ref Expression
1 inagbtwn.p 
 |-  P = ( Base ` G )
2 inagbtwn.i 
 |-  I = ( Itv ` G )
3 inagbtwn.k 
 |-  K = ( hlG ` G )
4 inagbtwn.g 
 |-  ( ph -> G e. TarskiG )
5 inagbtwn.d 
 |-  ( ph -> D e. P )
6 inagbtwn.e 
 |-  ( ph -> E e. P )
7 inagbtwn.f 
 |-  ( ph -> F e. P )
8 inagbtwn.w 
 |-  ( ph -> W e. P )
9 inagbtwn.in 
 |-  ( ph -> W ( inA ` G ) <" D E F "> )
10 inagbtwn.1 
 |-  ( ph -> E e. ( D I W ) )
11 simpl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x = E ) -> ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) )
12 simpr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) )
13 12 simpld 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> x e. ( D I F ) )
14 11 13 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x = E ) -> x e. ( D I F ) )
15 simpr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x = E ) -> x = E )
16 15 eleq1d 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x = E ) -> ( x e. ( D I F ) <-> E e. ( D I F ) ) )
17 14 16 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x = E ) -> E e. ( D I F ) )
18 eqid 
 |-  ( dist ` G ) = ( dist ` G )
19 simpl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) )
20 simpll 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> ph )
21 20 4 syl 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> G e. TarskiG )
22 19 21 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> G e. TarskiG )
23 20 5 syl 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> D e. P )
24 19 23 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> D e. P )
25 20 6 syl 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> E e. P )
26 19 25 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> E e. P )
27 simplr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> x e. P )
28 19 27 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> x e. P )
29 20 7 syl 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> F e. P )
30 19 29 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> F e. P )
31 simpl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) )
32 31 22 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> G e. TarskiG )
33 31 28 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> x e. P )
34 31 26 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> E e. P )
35 31 24 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> D e. P )
36 20 8 syl 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> W e. P )
37 19 36 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> W e. P )
38 31 37 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> W e. P )
39 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> x e. ( E I W ) )
40 20 10 syl 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> E e. ( D I W ) )
41 19 40 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> E e. ( D I W ) )
42 31 41 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> E e. ( D I W ) )
43 1 18 2 32 33 34 35 38 39 42 tgbtwnintr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> E e. ( x I D ) )
44 1 18 2 32 33 34 35 43 tgbtwncom 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ x e. ( E I W ) ) -> E e. ( D I x ) )
45 simpl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) )
46 45 22 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> G e. TarskiG )
47 45 24 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> D e. P )
48 45 26 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> E e. P )
49 45 37 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> W e. P )
50 45 28 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> x e. P )
51 simpr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> x ( K ` E ) W )
52 1 2 3 28 37 26 22 ishlg 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> ( x ( K ` E ) W <-> ( x =/= E /\ W =/= E /\ ( x e. ( E I W ) \/ W e. ( E I x ) ) ) ) )
53 51 52 mpbid 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> ( x =/= E /\ W =/= E /\ ( x e. ( E I W ) \/ W e. ( E I x ) ) ) )
54 53 simp2d 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> W =/= E )
55 54 necomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> E =/= W )
56 45 55 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> E =/= W )
57 45 41 syl 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> E e. ( D I W ) )
58 simpr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> W e. ( E I x ) )
59 1 18 2 46 47 48 49 50 56 57 58 tgbtwnouttr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) /\ W e. ( E I x ) ) -> E e. ( D I x ) )
60 53 simp3d 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> ( x e. ( E I W ) \/ W e. ( E I x ) ) )
61 44 59 60 mpjaodan 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> E e. ( D I x ) )
62 19 13 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> x e. ( D I F ) )
63 1 18 2 22 24 26 28 30 61 62 tgbtwnexch 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) /\ x ( K ` E ) W ) -> E e. ( D I F ) )
64 12 simprd 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> ( x = E \/ x ( K ` E ) W ) )
65 17 63 64 mpjaodan 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) -> E e. ( D I F ) )
66 1 2 3 8 5 6 7 4 isinag 
 |-  ( ph -> ( W ( inA ` G ) <" D E F "> <-> ( ( D =/= E /\ F =/= E /\ W =/= E ) /\ E. x e. P ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) ) )
67 9 66 mpbid 
 |-  ( ph -> ( ( D =/= E /\ F =/= E /\ W =/= E ) /\ E. x e. P ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) ) )
68 67 simprd 
 |-  ( ph -> E. x e. P ( x e. ( D I F ) /\ ( x = E \/ x ( K ` E ) W ) ) )
69 65 68 r19.29a 
 |-  ( ph -> E e. ( D I F ) )