Theorem tgcgrtriv

Description: Degenerate segments are congruent. Theorem 2.8 of Schwabhauser p. 28. (Contributed by Thierry Arnoux, 23-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 )
	tgcgrtriv.1	|- ( ph -> A e. P )
	tgcgrtriv.2	|- ( ph -> B e. P )
Assertion	tgcgrtriv	|- ( ph -> ( A .- A ) = ( B .- 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		tgcgrtriv.1	|- ( ph -> A e. P )
6		tgcgrtriv.2	|- ( ph -> B e. P )
7	4	ad2antrr	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> G e. TarskiG )
8	5	ad2antrr	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> A e. P )
9		simplr	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> x e. P )
10	6	ad2antrr	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> B e. P )
11		simprr	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> ( A .- x ) = ( B .- B ) )
12	1 2 3 7 8 9 10 11	axtgcgrid	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> A = x )
13	12	oveq2d	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> ( A .- A ) = ( A .- x ) )
14	13 11	eqtrd	|- ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) ) -> ( A .- A ) = ( B .- B ) )
15	1 2 3 4 6 5 6 6	axtgsegcon	|- ( ph -> E. x e. P ( A e. ( B I x ) /\ ( A .- x ) = ( B .- B ) ) )
16	14 15	r19.29a	|- ( ph -> ( A .- A ) = ( B .- B ) )