Metamath Proof Explorer

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	$⊢ \underset{˙}{-} = dist (G)$
		tkgeom.i	$⊢ I = Itv (G)$
		tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		tgcgrtriv.1	$⊢ φ \to A \in P$
		tgcgrtriv.2	$⊢ φ \to B \in P$
	Assertion	tgcgrtriv	$⊢ φ \to A \underset{˙}{-} A = B \underset{˙}{-} B$

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	$⊢ P = {Base}_{G}$
2		tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
3		tkgeom.i	$⊢ I = Itv (G)$
4		tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgcgrtriv.1	$⊢ φ \to A \in P$
6		tgcgrtriv.2	$⊢ φ \to B \in P$
7	4	ad2antrr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to G \in 𝒢_{Tarski}$
8	5	ad2antrr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to A \in P$
9		simplr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to x \in P$
10	6	ad2antrr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to B \in P$
11		simprr	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to A \underset{˙}{-} x = B \underset{˙}{-} B$
12	1 2 3 7 8 9 10 11	axtgcgrid	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to A = x$
13	12	oveq2d	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to A \underset{˙}{-} A = A \underset{˙}{-} x$
14	13 11	eqtrd	$⊢ ((φ \land x \in P) \land (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)) \to A \underset{˙}{-} A = B \underset{˙}{-} B$
15	1 2 3 4 6 5 6 6	axtgsegcon	$⊢ φ \to \exists x \in P (A \in (B I x) \land A \underset{˙}{-} x = B \underset{˙}{-} B)$
16	14 15	r19.29a	$⊢ φ \to A \underset{˙}{-} A = B \underset{˙}{-} B$