Metamath Proof Explorer

Theorem idinside

Description: Law for finding a point inside a segment. Theorem 4.19 of Schwabhauser p. 38. (Contributed by Scott Fenton, 7-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
2 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
3 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
4 cgrid2 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. C , C >. Cgr <. C , D >. -> C = D ) )
5 1 2 2 3 4 syl13anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. C , C >. Cgr <. C , D >. -> C = D ) )
6 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
7 axbtwnid 
 |-  ( ( N e. NN /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( C Btwn <. A , A >. -> C = A ) )
8 1 2 6 7 syl3anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. A , A >. -> C = A ) )
9 opeq1 
 |-  ( C = A -> <. C , C >. = <. A , C >. )
10 opeq1 
 |-  ( C = A -> <. C , D >. = <. A , D >. )
11 9 10 breq12d 
 |-  ( C = A -> ( <. C , C >. Cgr <. C , D >. <-> <. A , C >. Cgr <. A , D >. ) )
12 11 imbi1d 
 |-  ( C = A -> ( ( <. C , C >. Cgr <. C , D >. -> C = D ) <-> ( <. A , C >. Cgr <. A , D >. -> C = D ) ) )
13 12 biimpcd 
 |-  ( ( <. C , C >. Cgr <. C , D >. -> C = D ) -> ( C = A -> ( <. A , C >. Cgr <. A , D >. -> C = D ) ) )
14 ax-1 
 |-  ( C = D -> ( <. B , C >. Cgr <. B , D >. -> C = D ) )
15 13 14 syl8 
 |-  ( ( <. C , C >. Cgr <. C , D >. -> C = D ) -> ( C = A -> ( <. A , C >. Cgr <. A , D >. -> ( <. B , C >. Cgr <. B , D >. -> C = D ) ) ) )
16 5 8 15 sylsyld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. A , A >. -> ( <. A , C >. Cgr <. A , D >. -> ( <. B , C >. Cgr <. B , D >. -> C = D ) ) ) )
17 16 3impd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , A >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) )
18 opeq2 
 |-  ( A = B -> <. A , A >. = <. A , B >. )
19 18 breq2d 
 |-  ( A = B -> ( C Btwn <. A , A >. <-> C Btwn <. A , B >. ) )
20 19 3anbi1d 
 |-  ( A = B -> ( ( C Btwn <. A , A >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) <-> ( C Btwn <. A , B >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) )
21 20 imbi1d 
 |-  ( A = B -> ( ( ( C Btwn <. A , A >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) <-> ( ( C Btwn <. A , B >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) ) )
22 17 21 syl5ib 
 |-  ( A = B -> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) ) )
23 simpr1 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> N e. NN )
24 simpr2l 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> A e. ( EE ` N ) )
25 simpr2r 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> B e. ( EE ` N ) )
26 simpr3l 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> C e. ( EE ` N ) )
27 btwncolinear1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> A Colinear <. B , C >. ) )
28 23 24 25 26 27 syl13anc 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> ( C Btwn <. A , B >. -> A Colinear <. B , C >. ) )
29 idd 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> ( <. A , C >. Cgr <. A , D >. -> <. A , C >. Cgr <. A , D >. ) )
30 idd 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> ( <. B , C >. Cgr <. B , D >. -> <. B , C >. Cgr <. B , D >. ) )
31 28 29 30 3anim123d 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) )
32 simp1 
 |-  ( ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> A Colinear <. B , C >. )
33 32 anim2i 
 |-  ( ( A =/= B /\ ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) -> ( A =/= B /\ A Colinear <. B , C >. ) )
34 3simpc 
 |-  ( ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> ( <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) )
35 34 adantl 
 |-  ( ( A =/= B /\ ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) -> ( <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) )
36 33 35 jca 
 |-  ( ( A =/= B /\ ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) -> ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) )
37 lineid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( ( A =/= B /\ A Colinear <. B , C >. ) /\ ( <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) -> C = D ) )
38 36 37 syl5 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( A =/= B /\ ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) ) -> C = D ) )
39 38 expd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( A =/= B -> ( ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) ) )
40 39 impcom 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> ( ( A Colinear <. B , C >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) )
41 31 40 syld 
 |-  ( ( A =/= B /\ ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) )
42 41 ex 
 |-  ( A =/= B -> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) ) )
43 22 42 pm2.61ine 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , C >. Cgr <. A , D >. /\ <. B , C >. Cgr <. B , D >. ) -> C = D ) )