Metamath Proof Explorer

Theorem btwnconn1lem7

Description: Lemma for btwnconn1 . Under our assumptions, C and d are distinct. (Contributed by Scott Fenton, 8-Oct-2013)

Ref Expression
Assertion btwnconn1lem7 
|- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) /\ ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) ) ) -> C =/= d )

Proof

Step Hyp Ref Expression
1 simp1l3 
 |-  ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) -> C =/= c )
2 1 adantr 
 |-  ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) /\ ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) ) -> C =/= c )
3 simp2rr 
 |-  ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) -> <. C , d >. Cgr <. C , D >. )
4 3 adantr 
 |-  ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) /\ ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) ) -> <. C , d >. Cgr <. C , D >. )
5 simp2lr 
 |-  ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) -> <. D , c >. Cgr <. C , D >. )
6 5 adantr 
 |-  ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) /\ ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) ) -> <. D , c >. Cgr <. C , D >. )
7 2 4 6 3jca 
 |-  ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) /\ ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) ) -> ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) )
8 simp11 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> N e. NN )
9 simp21 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
10 simp22 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
11 simp23 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> c e. ( EE ` N ) )
12 simp31 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> d e. ( EE ` N ) )
13 simpr1 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) -> C =/= c )
14 opeq2 
 |-  ( C = d -> <. C , C >. = <. C , d >. )
15 14 breq1d 
 |-  ( C = d -> ( <. C , C >. Cgr <. C , D >. <-> <. C , d >. Cgr <. C , D >. ) )
16 15 3anbi2d 
 |-  ( C = d -> ( ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) <-> ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) )
17 16 biimparc 
 |-  ( ( ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) /\ C = d ) -> ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) )
18 simp2 
 |-  ( ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) -> <. C , C >. Cgr <. C , D >. )
19 simp1 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> N e. NN )
20 simp2l 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
21 simp2r 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
22 cgrid2 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. C , C >. Cgr <. C , D >. -> C = D ) )
23 19 20 20 21 22 syl13anc 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( <. C , C >. Cgr <. C , D >. -> C = D ) )
24 18 23 syl5 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) -> C = D ) )
25 24 imp 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) -> C = D )
26 opeq1 
 |-  ( C = D -> <. C , c >. = <. D , c >. )
27 opeq2 
 |-  ( C = D -> <. C , C >. = <. C , D >. )
28 26 27 breq12d 
 |-  ( C = D -> ( <. C , c >. Cgr <. C , C >. <-> <. D , c >. Cgr <. C , D >. ) )
29 28 biimparc 
 |-  ( ( <. D , c >. Cgr <. C , D >. /\ C = D ) -> <. C , c >. Cgr <. C , C >. )
30 simp3l 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> c e. ( EE ` N ) )
31 axcgrid 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ c e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. C , c >. Cgr <. C , C >. -> C = c ) )
32 19 20 30 20 31 syl13anc 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( <. C , c >. Cgr <. C , C >. -> C = c ) )
33 29 32 syl5 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( <. D , c >. Cgr <. C , D >. /\ C = D ) -> C = c ) )
34 33 expdimp 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ <. D , c >. Cgr <. C , D >. ) -> ( C = D -> C = c ) )
35 34 3ad2antr3 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) -> ( C = D -> C = c ) )
36 25 35 mpd 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) -> C = c )
37 36 ex 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( C =/= c /\ <. C , C >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) -> C = c ) )
38 17 37 syl5 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) /\ C = d ) -> C = c ) )
39 38 expdimp 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) -> ( C = d -> C = c ) )
40 39 necon3d 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) -> ( C =/= c -> C =/= d ) )
41 13 40 mpd 
 |-  ( ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) ) -> C =/= d )
42 41 ex 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) -> C =/= d ) )
43 8 9 10 11 12 42 syl122anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( C =/= c /\ <. C , d >. Cgr <. C , D >. /\ <. D , c >. Cgr <. C , D >. ) -> C =/= d ) )
44 7 43 syl5 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) /\ ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) ) -> C =/= d ) )
45 44 imp 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) /\ ( ( ( ( A =/= B /\ B =/= C /\ C =/= c ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) /\ ( E Btwn <. C , c >. /\ E Btwn <. D , d >. ) ) ) -> C =/= d )