Metamath Proof Explorer

Theorem seglelin

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

Ref Expression
Assertion seglelin 
|- ( ( 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 >. ) )

Proof

Step Hyp Ref Expression
1 segcon2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( ( B Btwn <. A , x >. \/ x Btwn <. A , B >. ) /\ <. A , x >. Cgr <. C , D >. ) )
2 andir 
 |-  ( ( ( B Btwn <. A , x >. \/ x Btwn <. A , B >. ) /\ <. A , x >. Cgr <. C , D >. ) <-> ( ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ ( x Btwn <. A , B >. /\ <. A , x >. Cgr <. C , D >. ) ) )
3 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
4 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
5 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
6 simpl3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
7 cgrcom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , x >. Cgr <. C , D >. <-> <. C , D >. Cgr <. A , x >. ) )
8 3 4 5 6 7 syl121anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( <. A , x >. Cgr <. C , D >. <-> <. C , D >. Cgr <. A , x >. ) )
9 8 anbi2d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( x Btwn <. A , B >. /\ <. A , x >. Cgr <. C , D >. ) <-> ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) )
10 9 orbi2d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ ( x Btwn <. A , B >. /\ <. A , x >. Cgr <. C , D >. ) ) <-> ( ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) ) )
11 2 10 syl5bb 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( ( B Btwn <. A , x >. \/ x Btwn <. A , B >. ) /\ <. A , x >. Cgr <. C , D >. ) <-> ( ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) ) )
12 11 rexbidva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( ( B Btwn <. A , x >. \/ x Btwn <. A , B >. ) /\ <. A , x >. Cgr <. C , D >. ) <-> E. x e. ( EE ` N ) ( ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) ) )
13 brsegle2 
 |-  ( ( 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. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
14 brsegle 
 |-  ( ( 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. x e. ( EE ` N ) ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) )
15 14 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. x e. ( EE ` N ) ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) )
16 13 15 orbi12d 
 |-  ( ( 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. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ E. x e. ( EE ` N ) ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) ) )
17 r19.43 
 |-  ( E. x e. ( EE ` N ) ( ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) <-> ( E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ E. x e. ( EE ` N ) ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) )
18 16 17 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. x e. ( EE ` N ) ( ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) \/ ( x Btwn <. A , B >. /\ <. C , D >. Cgr <. A , x >. ) ) ) )
19 12 18 bitr4d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( ( B Btwn <. A , x >. \/ x Btwn <. A , B >. ) /\ <. A , x >. Cgr <. C , D >. ) <-> ( <. A , B >. Seg<_ <. C , D >. \/ <. C , D >. Seg<_ <. A , B >. ) ) )
20 1 19 mpbid 
 |-  ( ( 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 >. ) )