Metamath Proof Explorer

Theorem cgrane2

Description: Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020)

Ref Expression
Hypotheses iscgra.p 
|- P = ( Base ` G )
iscgra.i 
|- I = ( Itv ` G )
iscgra.k 
|- K = ( hlG ` G )
iscgra.g 
|- ( ph -> G e. TarskiG )
iscgra.a 
|- ( ph -> A e. P )
iscgra.b 
|- ( ph -> B e. P )
iscgra.c 
|- ( ph -> C e. P )
iscgra.d 
|- ( ph -> D e. P )
iscgra.e 
|- ( ph -> E e. P )
iscgra.f 
|- ( ph -> F e. P )
cgrahl1.2 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
Assertion cgrane2 
|- ( ph -> B =/= C )

Proof

Step Hyp Ref Expression
1 iscgra.p 
 |-  P = ( Base ` G )
2 iscgra.i 
 |-  I = ( Itv ` G )
3 iscgra.k 
 |-  K = ( hlG ` G )
4 iscgra.g 
 |-  ( ph -> G e. TarskiG )
5 iscgra.a 
 |-  ( ph -> A e. P )
6 iscgra.b 
 |-  ( ph -> B e. P )
7 iscgra.c 
 |-  ( ph -> C e. P )
8 iscgra.d 
 |-  ( ph -> D e. P )
9 iscgra.e 
 |-  ( ph -> E e. P )
10 iscgra.f 
 |-  ( ph -> F e. P )
11 cgrahl1.2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
12 eqid 
 |-  ( dist ` G ) = ( dist ` G )
13 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> G e. TarskiG )
14 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> E e. P )
15 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y e. P )
16 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> B e. P )
17 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> C e. P )
18 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
19 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> A e. P )
20 simpllr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x e. P )
21 simpr1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
22 1 12 2 18 13 19 16 17 20 14 15 21 cgr3simp2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B ( dist ` G ) C ) = ( E ( dist ` G ) y ) )
23 22 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( E ( dist ` G ) y ) = ( B ( dist ` G ) C ) )
24 10 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> F e. P )
25 simpr3 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y ( K ` E ) F )
26 1 2 3 15 24 14 13 25 hlne1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y =/= E )
27 26 necomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> E =/= y )
28 1 12 2 13 14 15 16 17 23 27 tgcgrneq 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> B =/= C )
29 1 2 3 4 5 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )
30 11 29 mpbid 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) )
31 28 30 r19.29vva 
 |-  ( ph -> B =/= C )