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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tkgeom.d	⊢ − = ( dist ‘ 𝐺 )
	tkgeom.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tkgeom.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgcgrtriv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgcgrtriv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
Assertion	tgcgrtriv	⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = ( 𝐵 − 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tkgeom.d	⊢ − = ( dist ‘ 𝐺 )
3		tkgeom.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tkgeom.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tgcgrtriv.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		tgcgrtriv.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
8	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → 𝐴 ∈ 𝑃 )
9		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → 𝑥 ∈ 𝑃 )
10	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → 𝐵 ∈ 𝑃 )
11		simprr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) )
12	1 2 3 7 8 9 10 11	axtgcgrid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → 𝐴 = 𝑥 )
13	12	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → ( 𝐴 − 𝐴 ) = ( 𝐴 − 𝑥 ) )
14	13 11	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) ) → ( 𝐴 − 𝐴 ) = ( 𝐵 − 𝐵 ) )
15	1 2 3 4 6 5 6 6	axtgsegcon	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ ( 𝐴 − 𝑥 ) = ( 𝐵 − 𝐵 ) ) )
16	14 15	r19.29a	⊢ ( 𝜑 → ( 𝐴 − 𝐴 ) = ( 𝐵 − 𝐵 ) )