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 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) -> D = E ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> N e. NN )
2 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
3 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
4 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
5 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ D Btwn <. A , E >. ) ) -> D Btwn <. A , E >. )
6 simprl3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ D Btwn <. A , E >. ) ) -> <. A , D >. Cgr <. A , E >. )
7 1 2 4 2 3 6 cgrcomand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ D Btwn <. A , E >. ) ) -> <. A , E >. Cgr <. A , D >. )
8 1 2 3 4 5 7 endofsegidand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ D Btwn <. A , E >. ) ) -> E = D )
9 8 eqcomd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ D Btwn <. A , E >. ) ) -> D = E )
10 9 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) ) -> ( D Btwn <. A , E >. -> D = E ) )
11 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ E Btwn <. A , D >. ) ) -> E Btwn <. A , D >. )
12 simprl3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ E Btwn <. A , D >. ) ) -> <. A , D >. Cgr <. A , E >. )
13 1 2 4 3 11 12 endofsegidand 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) /\ E Btwn <. A , D >. ) ) -> D = E )
14 13 expr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) ) -> ( E Btwn <. A , D >. -> D = E ) )
15 3simpa 
 |-  ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) -> ( D Btwn <. A , B >. /\ E Btwn <. A , B >. ) )
16 15 adantl 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) ) -> ( D Btwn <. A , B >. /\ E Btwn <. A , B >. ) )
17 simp2r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
18 btwnconn3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. ) -> ( D Btwn <. A , E >. \/ E Btwn <. A , D >. ) ) )
19 1 2 4 3 17 18 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. ) -> ( D Btwn <. A , E >. \/ E Btwn <. A , D >. ) ) )
20 19 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) ) -> ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. ) -> ( D Btwn <. A , E >. \/ E Btwn <. A , D >. ) ) )
21 16 20 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) ) -> ( D Btwn <. A , E >. \/ E Btwn <. A , D >. ) )
22 10 14 21 mpjaod 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) ) -> D = E )
23 22 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( D Btwn <. A , B >. /\ E Btwn <. A , B >. /\ <. A , D >. Cgr <. A , E >. ) -> D = E ) )