Metamath Proof Explorer

Theorem inaghl

Description: The "point lie in angle" relation is independent of the points chosen on the half lines starting from B . Theorem 11.25 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 27-Sep-2020)

Ref Expression
Hypotheses isinag.p 
|- P = ( Base ` G )
isinag.i 
|- I = ( Itv ` G )
isinag.k 
|- K = ( hlG ` G )
isinag.x 
|- ( ph -> X e. P )
isinag.a 
|- ( ph -> A e. P )
isinag.b 
|- ( ph -> B e. P )
isinag.c 
|- ( ph -> C e. P )
inagflat.g 
|- ( ph -> G e. TarskiG )
inagswap.1 
|- ( ph -> X ( inA ` G ) <" A B C "> )
inaghl.d 
|- ( ph -> D e. P )
inaghl.f 
|- ( ph -> F e. P )
inaghl.y 
|- ( ph -> Y e. P )
inaghl.1 
|- ( ph -> D ( K ` B ) A )
inaghl.2 
|- ( ph -> F ( K ` B ) C )
inaghl.3 
|- ( ph -> Y ( K ` B ) X )
Assertion inaghl 
|- ( ph -> Y ( inA ` G ) <" D B F "> )

Proof

Step Hyp Ref Expression
1 isinag.p 
 |-  P = ( Base ` G )
2 isinag.i 
 |-  I = ( Itv ` G )
3 isinag.k 
 |-  K = ( hlG ` G )
4 isinag.x 
 |-  ( ph -> X e. P )
5 isinag.a 
 |-  ( ph -> A e. P )
6 isinag.b 
 |-  ( ph -> B e. P )
7 isinag.c 
 |-  ( ph -> C e. P )
8 inagflat.g 
 |-  ( ph -> G e. TarskiG )
9 inagswap.1 
 |-  ( ph -> X ( inA ` G ) <" A B C "> )
10 inaghl.d 
 |-  ( ph -> D e. P )
11 inaghl.f 
 |-  ( ph -> F e. P )
12 inaghl.y 
 |-  ( ph -> Y e. P )
13 inaghl.1 
 |-  ( ph -> D ( K ` B ) A )
14 inaghl.2 
 |-  ( ph -> F ( K ` B ) C )
15 inaghl.3 
 |-  ( ph -> Y ( K ` B ) X )
16 1 2 3 10 5 6 8 13 hlne1 
 |-  ( ph -> D =/= B )
17 1 2 3 11 7 6 8 14 hlne1 
 |-  ( ph -> F =/= B )
18 1 2 3 12 4 6 8 15 hlne1 
 |-  ( ph -> Y =/= B )
19 16 17 18 3jca 
 |-  ( ph -> ( D =/= B /\ F =/= B /\ Y =/= B ) )
20 6 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. P )
21 eleq1 
 |-  ( y = B -> ( y e. ( D I F ) <-> B e. ( D I F ) ) )
22 eqeq1 
 |-  ( y = B -> ( y = B <-> B = B ) )
23 breq1 
 |-  ( y = B -> ( y ( K ` B ) Y <-> B ( K ` B ) Y ) )
24 22 23 orbi12d 
 |-  ( y = B -> ( ( y = B \/ y ( K ` B ) Y ) <-> ( B = B \/ B ( K ` B ) Y ) ) )
25 21 24 anbi12d 
 |-  ( y = B -> ( ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) <-> ( B e. ( D I F ) /\ ( B = B \/ B ( K ` B ) Y ) ) ) )
26 25 adantl 
 |-  ( ( ( ph /\ B e. ( A I C ) ) /\ y = B ) -> ( ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) <-> ( B e. ( D I F ) /\ ( B = B \/ B ( K ` B ) Y ) ) ) )
27 5 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> A e. P )
28 10 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> D e. P )
29 11 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> F e. P )
30 8 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> G e. TarskiG )
31 1 2 3 10 5 6 8 13 hlcomd 
 |-  ( ph -> A ( K ` B ) D )
32 31 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> A ( K ` B ) D )
33 eqid 
 |-  ( dist ` G ) = ( dist ` G )
34 7 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> C e. P )
35 1 2 3 11 7 6 8 14 hlcomd 
 |-  ( ph -> C ( K ` B ) F )
36 35 adantr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> C ( K ` B ) F )
37 simpr 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( A I C ) )
38 1 33 2 30 27 20 34 37 tgbtwncom 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( C I A ) )
39 1 2 3 34 29 27 30 20 36 38 btwnhl 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( F I A ) )
40 1 33 2 30 29 20 27 39 tgbtwncom 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( A I F ) )
41 1 2 3 27 28 29 30 20 32 40 btwnhl 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B e. ( D I F ) )
42 eqidd 
 |-  ( ( ph /\ B e. ( A I C ) ) -> B = B )
43 42 orcd 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( B = B \/ B ( K ` B ) Y ) )
44 41 43 jca 
 |-  ( ( ph /\ B e. ( A I C ) ) -> ( B e. ( D I F ) /\ ( B = B \/ B ( K ` B ) Y ) ) )
45 20 26 44 rspcedvd 
 |-  ( ( ph /\ B e. ( A I C ) ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
46 simpllr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> x e. P )
47 simpr 
 |-  ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) /\ y = x ) -> y = x )
48 47 eleq1d 
 |-  ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) /\ y = x ) -> ( y e. ( D I F ) <-> x e. ( D I F ) ) )
49 47 eqeq1d 
 |-  ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) /\ y = x ) -> ( y = B <-> x = B ) )
50 47 breq1d 
 |-  ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) /\ y = x ) -> ( y ( K ` B ) Y <-> x ( K ` B ) Y ) )
51 49 50 orbi12d 
 |-  ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) /\ y = x ) -> ( ( y = B \/ y ( K ` B ) Y ) <-> ( x = B \/ x ( K ` B ) Y ) ) )
52 48 51 anbi12d 
 |-  ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) /\ y = x ) -> ( ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) <-> ( x e. ( D I F ) /\ ( x = B \/ x ( K ` B ) Y ) ) ) )
53 simpr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> x = B )
54 5 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> A e. P )
55 10 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> D e. P )
56 11 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> F e. P )
57 8 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> G e. TarskiG )
58 6 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> B e. P )
59 31 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> A ( K ` B ) D )
60 7 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> C e. P )
61 35 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> C ( K ` B ) F )
62 simplr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> x e. ( A I C ) )
63 1 33 2 57 54 46 60 62 tgbtwncom 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> x e. ( C I A ) )
64 53 63 eqeltrrd 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> B e. ( C I A ) )
65 1 2 3 60 56 54 57 58 61 64 btwnhl 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> B e. ( F I A ) )
66 1 33 2 57 56 58 54 65 tgbtwncom 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> B e. ( A I F ) )
67 1 2 3 54 55 56 57 58 59 66 btwnhl 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> B e. ( D I F ) )
68 53 67 eqeltrd 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> x e. ( D I F ) )
69 53 orcd 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> ( x = B \/ x ( K ` B ) Y ) )
70 68 69 jca 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> ( x e. ( D I F ) /\ ( x = B \/ x ( K ` B ) Y ) ) )
71 46 52 70 rspcedvd 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x = B ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
72 8 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> G e. TarskiG )
73 72 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> G e. TarskiG )
74 simplr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> z e. P )
75 6 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> B e. P )
76 75 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> B e. P )
77 7 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> C e. P )
78 77 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> C e. P )
79 10 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> D e. P )
80 79 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> D e. P )
81 11 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> F e. P )
82 simpllr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> x e. P )
83 82 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> x e. P )
84 simprl 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> x ( K ` B ) z )
85 1 2 3 83 74 76 73 84 hlne2 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> z =/= B )
86 35 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> C ( K ` B ) F )
87 simprr 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> z e. ( C I D ) )
88 1 33 2 73 78 74 80 87 tgbtwncom 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> z e. ( D I C ) )
89 1 2 3 73 74 76 78 80 81 85 86 88 hlpasch 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> E. y e. P ( z ( K ` B ) y /\ y e. ( D I F ) ) )
90 simprr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> y e. ( D I F ) )
91 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> y e. P )
92 74 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> z e. P )
93 12 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> Y e. P )
94 73 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> G e. TarskiG )
95 76 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> B e. P )
96 simprl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> z ( K ` B ) y )
97 1 2 3 92 91 95 94 96 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> y ( K ` B ) z )
98 82 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> x e. P )
99 4 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> X e. P )
100 15 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> Y ( K ` B ) X )
101 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> x ( K ` B ) X )
102 1 2 3 98 99 95 94 101 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> X ( K ` B ) x )
103 1 2 3 93 99 98 94 95 100 102 hltr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> Y ( K ` B ) x )
104 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> ( x ( K ` B ) z /\ z e. ( C I D ) ) )
105 104 simpld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> x ( K ` B ) z )
106 1 2 3 93 98 92 94 95 103 105 hltr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> Y ( K ` B ) z )
107 1 2 3 93 92 95 94 106 hlcomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> z ( K ` B ) Y )
108 1 2 3 91 92 93 94 95 97 107 hltr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> y ( K ` B ) Y )
109 108 olcd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> ( y = B \/ y ( K ` B ) Y ) )
110 90 109 jca 
 |-  ( ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) /\ ( z ( K ` B ) y /\ y e. ( D I F ) ) ) -> ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
111 110 ex 
 |-  ( ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) /\ y e. P ) -> ( ( z ( K ` B ) y /\ y e. ( D I F ) ) -> ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) ) )
112 111 reximdva 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> ( E. y e. P ( z ( K ` B ) y /\ y e. ( D I F ) ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) ) )
113 89 112 mpd 
 |-  ( ( ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) /\ z e. P ) /\ ( x ( K ` B ) z /\ z e. ( C I D ) ) ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
114 5 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> A e. P )
115 4 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> X e. P )
116 simpr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> x ( K ` B ) X )
117 1 2 3 82 115 75 72 116 hlne1 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> x =/= B )
118 31 ad4antr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> A ( K ` B ) D )
119 simplr 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> x e. ( A I C ) )
120 1 33 2 72 114 82 77 119 tgbtwncom 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> x e. ( C I A ) )
121 1 2 3 72 82 75 114 77 79 117 118 120 hlpasch 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> E. z e. P ( x ( K ` B ) z /\ z e. ( C I D ) ) )
122 113 121 r19.29a 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ x ( K ` B ) X ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
123 71 122 jaodan 
 |-  ( ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ x e. ( A I C ) ) /\ ( x = B \/ x ( K ` B ) X ) ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
124 123 anasss 
 |-  ( ( ( ( ph /\ -. B e. ( A I C ) ) /\ x e. P ) /\ ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
125 1 2 3 4 5 6 7 8 isinag 
 |-  ( ph -> ( X ( inA ` G ) <" A B C "> <-> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) )
126 9 125 mpbid 
 |-  ( ph -> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
127 126 simprd 
 |-  ( ph -> E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) )
128 127 adantr 
 |-  ( ( ph /\ -. B e. ( A I C ) ) -> E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) )
129 124 128 r19.29a 
 |-  ( ( ph /\ -. B e. ( A I C ) ) -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
130 45 129 pm2.61dan 
 |-  ( ph -> E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) )
131 1 2 3 12 10 6 11 8 isinag 
 |-  ( ph -> ( Y ( inA ` G ) <" D B F "> <-> ( ( D =/= B /\ F =/= B /\ Y =/= B ) /\ E. y e. P ( y e. ( D I F ) /\ ( y = B \/ y ( K ` B ) Y ) ) ) ) )
132 19 130 131 mpbir2and 
 |-  ( ph -> Y ( inA ` G ) <" D B F "> )