Theorem inagne1

Description: Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021)

	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 )
	inagflat.g	|- ( ph -> G e. TarskiG )
	inagswap.1	|- ( ph -> X ( inA ` G ) <" A B C "> )
Assertion	inagne1	|- ( ph -> A =/= B )

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		inagflat.g	|- ( ph -> G e. TarskiG )
9		inagswap.1	|- ( ph -> X ( inA ` G ) <" A B C "> )
10	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 ) ) ) ) )
11	9 10	mpbid	|- ( ph -> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
12	11	simpld	|- ( ph -> ( A =/= B /\ C =/= B /\ X =/= B ) )
13	12	simp1d	|- ( ph -> A =/= B )