Theorem legid

Description: Reflexivity of the less-than relationship. Proposition 5.7 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

	Ref	Expression
Hypotheses	legval.p	|- P = ( Base ` G )
	legval.d	|- .- = ( dist ` G )
	legval.i	|- I = ( Itv ` G )
	legval.l	|- .<_ = ( leG ` G )
	legval.g	|- ( ph -> G e. TarskiG )
	legid.a	|- ( ph -> A e. P )
	legid.b	|- ( ph -> B e. P )
Assertion	legid	|- ( ph -> ( A .- B ) .<_ ( A .- B ) )

Proof

Step	Hyp	Ref	Expression
1		legval.p	|- P = ( Base ` G )
2		legval.d	|- .- = ( dist ` G )
3		legval.i	|- I = ( Itv ` G )
4		legval.l	|- .<_ = ( leG ` G )
5		legval.g	|- ( ph -> G e. TarskiG )
6		legid.a	|- ( ph -> A e. P )
7		legid.b	|- ( ph -> B e. P )
8	1 2 3 5 6 7	tgbtwntriv2	|- ( ph -> B e. ( A I B ) )
9		eqidd	|- ( ph -> ( A .- B ) = ( A .- B ) )
10		eleq1	|- ( x = B -> ( x e. ( A I B ) <-> B e. ( A I B ) ) )
11		oveq2	|- ( x = B -> ( A .- x ) = ( A .- B ) )
12	11	eqeq2d	|- ( x = B -> ( ( A .- B ) = ( A .- x ) <-> ( A .- B ) = ( A .- B ) ) )
13	10 12	anbi12d	|- ( x = B -> ( ( x e. ( A I B ) /\ ( A .- B ) = ( A .- x ) ) <-> ( B e. ( A I B ) /\ ( A .- B ) = ( A .- B ) ) ) )
14	13	rspcev	|- ( ( B e. P /\ ( B e. ( A I B ) /\ ( A .- B ) = ( A .- B ) ) ) -> E. x e. P ( x e. ( A I B ) /\ ( A .- B ) = ( A .- x ) ) )
15	7 8 9 14	syl12anc	|- ( ph -> E. x e. P ( x e. ( A I B ) /\ ( A .- B ) = ( A .- x ) ) )
16	1 2 3 4 5 6 7 6 7	legov	|- ( ph -> ( ( A .- B ) .<_ ( A .- B ) <-> E. x e. P ( x e. ( A I B ) /\ ( A .- B ) = ( A .- x ) ) ) )
17	15 16	mpbird	|- ( ph -> ( A .- B ) .<_ ( A .- B ) )