Metamath Proof Explorer

Theorem segleantisym

Description: Antisymmetry law for segment comparison. Theorem 5.9 of Schwabhauser p. 42. (Contributed by Scott Fenton, 14-Oct-2013)

Ref Expression
Assertion segleantisym 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( <. A , B >. Seg<_ <. C , D >. /\ <. C , D >. Seg<_ <. A , B >. ) -> <. A , B >. Cgr <. C , D >. ) )

Proof

Step Hyp Ref Expression
1 brsegle 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
2 brsegle2 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. C , D >. Seg<_ <. A , B >. <-> E. t e. ( EE ` N ) ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) )
3 2 3com23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. C , D >. Seg<_ <. A , B >. <-> E. t e. ( EE ` N ) ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) )
4 1 3 anbi12d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( <. A , B >. Seg<_ <. C , D >. /\ <. C , D >. Seg<_ <. A , B >. ) <-> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ E. t e. ( EE ` N ) ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) )
5 reeanv 
 |-  ( E. y e. ( EE ` N ) E. t e. ( EE ` N ) ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) <-> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ E. t e. ( EE ` N ) ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) )
6 4 5 bitr4di 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( <. A , B >. Seg<_ <. C , D >. /\ <. C , D >. Seg<_ <. A , B >. ) <-> E. y e. ( EE ` N ) E. t e. ( EE ` N ) ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) )
7 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> N e. NN )
8 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
9 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> t e. ( EE ` N ) )
10 simprl 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> y e. ( EE ` N ) )
11 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
12 simprll 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> y Btwn <. C , D >. )
13 simprrl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> D Btwn <. C , t >. )
14 7 8 10 11 9 12 13 btwnexchand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> y Btwn <. C , t >. )
15 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
16 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
17 simprrr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> <. C , t >. Cgr <. A , B >. )
18 simprlr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> <. A , B >. Cgr <. C , y >. )
19 7 8 9 15 16 8 10 17 18 cgrtrand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> <. C , t >. Cgr <. C , y >. )
20 7 8 9 10 14 19 endofsegidand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> t = y )
21 opeq2 
 |-  ( t = y -> <. C , t >. = <. C , y >. )
22 21 breq2d 
 |-  ( t = y -> ( D Btwn <. C , t >. <-> D Btwn <. C , y >. ) )
23 21 breq1d 
 |-  ( t = y -> ( <. C , t >. Cgr <. A , B >. <-> <. C , y >. Cgr <. A , B >. ) )
24 22 23 anbi12d 
 |-  ( t = y -> ( ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) <-> ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) )
25 24 anbi2d 
 |-  ( t = y -> ( ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) <-> ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) )
26 25 anbi2d 
 |-  ( t = y -> ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) <-> ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) ) )
27 simprrl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> D Btwn <. C , y >. )
28 7 11 8 10 27 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> D Btwn <. y , C >. )
29 simprll 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> y Btwn <. C , D >. )
30 7 10 8 11 29 btwncomand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> y Btwn <. D , C >. )
31 btwnswapid 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ y e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( D Btwn <. y , C >. /\ y Btwn <. D , C >. ) -> D = y ) )
32 7 11 10 8 31 syl13anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) -> ( ( D Btwn <. y , C >. /\ y Btwn <. D , C >. ) -> D = y ) )
33 32 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> ( ( D Btwn <. y , C >. /\ y Btwn <. D , C >. ) -> D = y ) )
34 28 30 33 mp2and 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> D = y )
35 simprlr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> <. A , B >. Cgr <. C , y >. )
36 opeq2 
 |-  ( D = y -> <. C , D >. = <. C , y >. )
37 36 breq2d 
 |-  ( D = y -> ( <. A , B >. Cgr <. C , D >. <-> <. A , B >. Cgr <. C , y >. ) )
38 35 37 syl5ibrcom 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> ( D = y -> <. A , B >. Cgr <. C , D >. ) )
39 34 38 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , y >. /\ <. C , y >. Cgr <. A , B >. ) ) ) -> <. A , B >. Cgr <. C , D >. )
40 26 39 syl6bi 
 |-  ( t = y -> ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> <. A , B >. Cgr <. C , D >. ) )
41 20 40 mpcom 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) ) -> <. A , B >. Cgr <. C , D >. )
42 41 exp31 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( y e. ( EE ` N ) /\ t e. ( EE ` N ) ) -> ( ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) -> <. A , B >. Cgr <. C , D >. ) ) )
43 42 rexlimdvv 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. y e. ( EE ` N ) E. t e. ( EE ` N ) ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( D Btwn <. C , t >. /\ <. C , t >. Cgr <. A , B >. ) ) -> <. A , B >. Cgr <. C , D >. ) )
44 6 43 sylbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( <. A , B >. Seg<_ <. C , D >. /\ <. C , D >. Seg<_ <. A , B >. ) -> <. A , B >. Cgr <. C , D >. ) )