Metamath Proof Explorer

Theorem isinagd

Description: Sufficient conditions for in-angle relation, deduction version. (Contributed by Thierry Arnoux, 20-Oct-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 )
isinagd.g 
|- ( ph -> G e. V )
isinagd.y 
|- ( ph -> Y e. P )
isinagd.1 
|- ( ph -> A =/= B )
isinagd.2 
|- ( ph -> C =/= B )
isinagd.3 
|- ( ph -> X =/= B )
isinagd.4 
|- ( ph -> Y e. ( A I C ) )
isinagd.5 
|- ( ph -> ( Y = B \/ Y ( K ` B ) X ) )
Assertion isinagd 
|- ( ph -> X ( inA ` G ) <" A B C "> )

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 isinagd.g 
 |-  ( ph -> G e. V )
9 isinagd.y 
 |-  ( ph -> Y e. P )
10 isinagd.1 
 |-  ( ph -> A =/= B )
11 isinagd.2 
 |-  ( ph -> C =/= B )
12 isinagd.3 
 |-  ( ph -> X =/= B )
13 isinagd.4 
 |-  ( ph -> Y e. ( A I C ) )
14 isinagd.5 
 |-  ( ph -> ( Y = B \/ Y ( K ` B ) X ) )
15 10 11 12 3jca 
 |-  ( ph -> ( A =/= B /\ C =/= B /\ X =/= B ) )
16 simpr 
 |-  ( ( ph /\ x = Y ) -> x = Y )
17 eqidd 
 |-  ( ( ph /\ x = Y ) -> ( A I C ) = ( A I C ) )
18 16 17 eleq12d 
 |-  ( ( ph /\ x = Y ) -> ( x e. ( A I C ) <-> Y e. ( A I C ) ) )
19 eqidd 
 |-  ( ( ph /\ x = Y ) -> B = B )
20 16 19 eqeq12d 
 |-  ( ( ph /\ x = Y ) -> ( x = B <-> Y = B ) )
21 16 breq1d 
 |-  ( ( ph /\ x = Y ) -> ( x ( K ` B ) X <-> Y ( K ` B ) X ) )
22 20 21 orbi12d 
 |-  ( ( ph /\ x = Y ) -> ( ( x = B \/ x ( K ` B ) X ) <-> ( Y = B \/ Y ( K ` B ) X ) ) )
23 18 22 anbi12d 
 |-  ( ( ph /\ x = Y ) -> ( ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) <-> ( Y e. ( A I C ) /\ ( Y = B \/ Y ( K ` B ) X ) ) ) )
24 13 14 jca 
 |-  ( ph -> ( Y e. ( A I C ) /\ ( Y = B \/ Y ( K ` B ) X ) ) )
25 9 23 24 rspcedvd 
 |-  ( ph -> E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) )
26 15 25 jca 
 |-  ( ph -> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
27 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 ) ) ) ) )
28 26 27 mpbird 
 |-  ( ph -> X ( inA ` G ) <" A B C "> )