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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
2 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
5 1 2 2 3 3 4 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
6 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
7 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
10 axcgrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ → 𝐴 = 𝑥 ) )
11 6 7 8 9 10 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ → 𝐴 = 𝑥 ) )
12 opeq2 ⊢ ( 𝐴 = 𝑥 → ⟨ 𝐴 , 𝐴 ⟩ = ⟨ 𝐴 , 𝑥 ⟩ )
13 12 breq1d ⊢ ( 𝐴 = 𝑥 → ( ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ↔ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
14 13 biimprd ⊢ ( 𝐴 = 𝑥 → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
15 11 14 syli ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
16 15 adantld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
17 16 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐴 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐴 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
18 5 17 mpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ⟨ 𝐴 , 𝐴 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ )