Metamath Proof Explorer

Theorem cgrtriv

Description: Degenerate segments are congruent. Theorem 2.8 of Schwabhauser p. 28. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrtriv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A A Cgr B B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → N ∈ ℕ
2 simp2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
3 simp3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
4 axsegcon ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N A Btwn A x ∧ A x Cgr B B
5 1 2 2 3 3 4 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N A Btwn A x ∧ A x Cgr B B
6 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ
7 simpl2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
8 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
9 simpl3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
10 axcgrid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A x Cgr B B → A = x
11 6 7 8 9 10 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → A x Cgr B B → A = x
12 opeq2 ⊢ A = x → A A = A x
13 12 breq1d ⊢ A = x → A A Cgr B B ↔ A x Cgr B B
14 13 biimprd ⊢ A = x → A x Cgr B B → A A Cgr B B
15 11 14 syli ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → A x Cgr B B → A A Cgr B B
16 15 adantld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → A Btwn A x ∧ A x Cgr B B → A A Cgr B B
17 16 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N A Btwn A x ∧ A x Cgr B B → A A Cgr B B
18 5 17 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A A Cgr B B