Metamath Proof Explorer

Theorem midofsegid

Description: If two points fall in the same place in the middle of a segment, then they are identical. (Contributed by Scott Fenton, 16-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion midofsegid ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) → 𝐷 = 𝐸 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simp2l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ) ) → 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ )
6 simprl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ) ) → ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ )
7 1 2 4 2 3 6 cgrcomand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ) ) → ⟨ 𝐴 , 𝐸 ⟩ Cgr ⟨ 𝐴 , 𝐷 ⟩ )
8 1 2 3 4 5 7 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ) ) → 𝐸 = 𝐷 )
9 8 eqcomd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ) ) → 𝐷 = 𝐸 )
10 9 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ → 𝐷 = 𝐸 ) )
11 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ )
12 simprl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ )
13 1 2 4 3 11 12 endofsegidand ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐷 = 𝐸 )
14 13 expr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ) → ( 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ → 𝐷 = 𝐸 ) )
15 3simpa ⊢ ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
16 15 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
17 simp2r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
18 btwnconn3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ∨ 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
19 1 2 4 3 17 18 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ∨ 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
20 19 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ∨ 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
21 16 20 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐸 ⟩ ∨ 𝐸 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
22 10 14 21 mpjaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) ) → 𝐷 = 𝐸 )
23 22 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝐸 Btwn ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐷 ⟩ Cgr ⟨ 𝐴 , 𝐸 ⟩ ) → 𝐷 = 𝐸 ) )