Metamath Proof Explorer

Theorem leagne3

Description: Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023)

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 )
leagne.1 
|- ( ph -> <" A B C "> ( leA ` G ) <" D E F "> )
Assertion leagne3 
|- ( ph -> D =/= E )

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 leagne.1 
 |-  ( ph -> <" A B C "> ( leA ` G ) <" D E F "> )
10 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
11 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
12 2 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> G e. TarskiG )
13 3 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> A e. P )
14 4 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> B e. P )
15 5 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> C e. P )
16 6 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> D e. P )
17 7 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> E e. P )
18 simplr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> x e. P )
19 simprr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> <" A B C "> ( cgrA ` G ) <" D E x "> )
20 1 10 11 12 13 14 15 16 17 18 19 cgrane3 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> E =/= D )
21 20 necomd 
 |-  ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> D =/= E )
22 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 "> ) ) )
23 9 22 mpbid 
 |-  ( ph -> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) )
24 21 23 r19.29a 
 |-  ( ph -> D =/= E )