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→AACgrBB

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∈𝔼⁡NABtwnAx∧AxCgrBB
5 1 2 2 3 3 4 syl122anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃x∈𝔼⁡NABtwnAx∧AxCgrBB
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→AxCgrBB→A=x
11 6 7 8 9 10 syl13anc ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→AxCgrBB→A=x
12 opeq2 ⊢A=x→AA=Ax
13 12 breq1d ⊢A=x→AACgrBB↔AxCgrBB
14 13 biimprd ⊢A=x→AxCgrBB→AACgrBB
15 11 14 syli ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→AxCgrBB→AACgrBB
16 15 adantld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧x∈𝔼⁡N→ABtwnAx∧AxCgrBB→AACgrBB
17 16 rexlimdva ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→∃x∈𝔼⁡NABtwnAx∧AxCgrBB→AACgrBB
18 5 17 mpd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N→AACgrBB