Theorem tgbtwntriv2

Description: Betweenness always holds for the second endpoint. Theorem 3.1 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Hypotheses	tkgeom.p	|- P = ( Base ` G )
	tkgeom.d	|- .- = ( dist ` G )
	tkgeom.i	|- I = ( Itv ` G )
	tkgeom.g	|- ( ph -> G e. TarskiG )
	tgbtwntriv2.1	|- ( ph -> A e. P )
	tgbtwntriv2.2	|- ( ph -> B e. P )
Assertion	tgbtwntriv2	|- ( ph -> B e. ( A I B ) )

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	|- P = ( Base ` G )
2		tkgeom.d	|- .- = ( dist ` G )
3		tkgeom.i	|- I = ( Itv ` G )
4		tkgeom.g	|- ( ph -> G e. TarskiG )
5		tgbtwntriv2.1	|- ( ph -> A e. P )
6		tgbtwntriv2.2	|- ( ph -> B e. P )
7		simprl	|- ( ( ( ph /\ x e. P ) /\ ( B e. ( A I x ) /\ ( B .- x ) = ( B .- B ) ) ) -> B e. ( A I x ) )
8	4	ad2antrr	|- ( ( ( ph /\ x e. P ) /\ ( B .- x ) = ( B .- B ) ) -> G e. TarskiG )
9	6	ad2antrr	|- ( ( ( ph /\ x e. P ) /\ ( B .- x ) = ( B .- B ) ) -> B e. P )
10		simplr	|- ( ( ( ph /\ x e. P ) /\ ( B .- x ) = ( B .- B ) ) -> x e. P )
11		simpr	|- ( ( ( ph /\ x e. P ) /\ ( B .- x ) = ( B .- B ) ) -> ( B .- x ) = ( B .- B ) )
12	1 2 3 8 9 10 9 11	axtgcgrid	|- ( ( ( ph /\ x e. P ) /\ ( B .- x ) = ( B .- B ) ) -> B = x )
13	12	adantrl	|- ( ( ( ph /\ x e. P ) /\ ( B e. ( A I x ) /\ ( B .- x ) = ( B .- B ) ) ) -> B = x )
14	13	oveq2d	|- ( ( ( ph /\ x e. P ) /\ ( B e. ( A I x ) /\ ( B .- x ) = ( B .- B ) ) ) -> ( A I B ) = ( A I x ) )
15	7 14	eleqtrrd	|- ( ( ( ph /\ x e. P ) /\ ( B e. ( A I x ) /\ ( B .- x ) = ( B .- B ) ) ) -> B e. ( A I B ) )
16	1 2 3 4 5 6 6 6	axtgsegcon	|- ( ph -> E. x e. P ( B e. ( A I x ) /\ ( B .- x ) = ( B .- B ) ) )
17	15 16	r19.29a	|- ( ph -> B e. ( A I B ) )