Metamath Proof Explorer

Theorem isleagd

Description: Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020)

Ref Expression
Hypotheses isleag.p 
|- P = ( Base ` G )
isleag.g 
|- ( ph -> G e. TarskiG )
isleag.a 
|- ( ph -> A e. P )
isleag.b 
|- ( ph -> B e. P )
isleag.c 
|- ( ph -> C e. P )
isleag.d 
|- ( ph -> D e. P )
isleag.e 
|- ( ph -> E e. P )
isleag.f 
|- ( ph -> F e. P )
isleagd.s 
|- .<_ = ( leA ` G )
isleagd.x 
|- ( ph -> X e. P )
isleagd.1 
|- ( ph -> X ( inA ` G ) <" D E F "> )
isleagd.2 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E X "> )
Assertion isleagd 
|- ( ph -> <" A B C "> .<_ <" D E F "> )

Proof

Step Hyp Ref Expression
1 isleag.p 
 |-  P = ( Base ` G )
2 isleag.g 
 |-  ( ph -> G e. TarskiG )
3 isleag.a 
 |-  ( ph -> A e. P )
4 isleag.b 
 |-  ( ph -> B e. P )
5 isleag.c 
 |-  ( ph -> C e. P )
6 isleag.d 
 |-  ( ph -> D e. P )
7 isleag.e 
 |-  ( ph -> E e. P )
8 isleag.f 
 |-  ( ph -> F e. P )
9 isleagd.s 
 |-  .<_ = ( leA ` G )
10 isleagd.x 
 |-  ( ph -> X e. P )
11 isleagd.1 
 |-  ( ph -> X ( inA ` G ) <" D E F "> )
12 isleagd.2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E X "> )
13 9 eqcomi 
 |-  ( leA ` G ) = .<_
14 13 a1i 
 |-  ( ph -> ( leA ` G ) = .<_ )
15 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
16 15 breq1d 
 |-  ( ( ph /\ x = X ) -> ( x ( inA ` G ) <" D E F "> <-> X ( inA ` G ) <" D E F "> ) )
17 eqidd 
 |-  ( ( ph /\ x = X ) -> D = D )
18 eqidd 
 |-  ( ( ph /\ x = X ) -> E = E )
19 17 18 15 s3eqd 
 |-  ( ( ph /\ x = X ) -> <" D E x "> = <" D E X "> )
20 19 breq2d 
 |-  ( ( ph /\ x = X ) -> ( <" A B C "> ( cgrA ` G ) <" D E x "> <-> <" A B C "> ( cgrA ` G ) <" D E X "> ) )
21 16 20 anbi12d 
 |-  ( ( ph /\ x = X ) -> ( ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) <-> ( X ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E X "> ) ) )
22 11 12 jca 
 |-  ( ph -> ( X ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E X "> ) )
23 10 21 22 rspcedvd 
 |-  ( ph -> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) )
24 1 2 3 4 5 6 7 8 isleag 
 |-  ( ph -> ( <" A B C "> ( leA ` G ) <" D E F "> <-> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) )
25 23 24 mpbird 
 |-  ( ph -> <" A B C "> ( leA ` G ) <" D E F "> )
26 14 25 breqdi 
 |-  ( ph -> <" A B C "> .<_ <" D E F "> )