Metamath Proof Explorer


Theorem cgrane1

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 cgrane1
|- ( ph -> A =/= B )

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 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 )
15 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 )
16 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 )
17 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 )
18 eqid
 |-  ( cgrG ` G ) = ( cgrG ` G )
19 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 )
20 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 )
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 16 17 19 14 15 20 21 cgr3simp1
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( A ( dist ` G ) B ) = ( x ( dist ` G ) E ) )
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 ) ) -> ( x ( dist ` G ) E ) = ( A ( dist ` G ) B ) )
24 8 ad3antrrr
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> D e. P )
25 simpr2
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x ( K ` E ) D )
26 1 2 3 14 24 15 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 ) ) -> x =/= E )
27 1 12 2 13 14 15 16 17 23 26 tgcgrneq
 |-  ( ( ( ( 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 )
28 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 ) ) )
29 11 28 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 ) )
30 27 29 r19.29vva
 |-  ( ph -> A =/= B )