MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax5seg Structured version   Visualization version   Unicode version
Theorem ax5seg 25017
Description: The five segment axiom. Take two triangles A D C and E H G, a point B on A C, and a point F on E G. If all corresponding line segments except for C D and G H are congruent, then so are C D and G H. Axiom A5 of [Schwabhauser] p. 11. (Contributed by Scott Fenton, 12-Jun-2013.)
Assertion
Ref Expression
ax5seg |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( A =/= B /\ B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) -> <. C , D >.Cgr <. G , H >. ) )
Proof of Theorem ax5seg
Dummy variables i j t s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 12218 . . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( 1 ... N ) e. Fin )
2 simpl21 1092 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> C e. ( EE ` N ) )
3 fveere 24980 . . . . . . . . . . . . 13 |- ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. RR )
42, 3sylancom 678 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. RR )
5 simpl22 1093 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> D e. ( EE ` N ) )
6 fveere 24980 . . . . . . . . . . . . 13 |- ( ( D e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. RR )
75, 6sylancom 678 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. RR )
84, 7resubcld 10075 . . . . . . . . . . 11 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( C ` j ) - ( D ` j ) ) e. RR )
98resqcld 12474 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. RR )
101, 9fsumrecl 13849 . . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. RR )
1110recnd 9695 . . . . . . . 8 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. CC )
1211adantr 471 . . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) e. CC )
13 simpl32 1096 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> G e. ( EE ` N ) )
14 fveere 24980 . . . . . . . . . . . . 13 |- ( ( G e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( G ` j ) e. RR )
1513, 14sylancom 678 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( G ` j ) e. RR )
16 simpl33 1097 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> H e. ( EE ` N ) )
17 fveere 24980 . . . . . . . . . . . . 13 |- ( ( H e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( H ` j ) e. RR )
1816, 17sylancom 678 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( H ` j ) e. RR )
1915, 18resubcld 10075 . . . . . . . . . . 11 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( G ` j ) - ( H ` j ) ) e. RR )
2019resqcld 12474 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) e. RR )
211, 20fsumrecl 13849 . . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) e. RR )
2221recnd 9695 . . . . . . . 8 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) e. CC )
2322adantr 471 . . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) e. CC )
24 0re 9669 . . . . . . . . . . . . 13 |- 0 e. RR
25 1re 9668 . . . . . . . . . . . . 13 |- 1 e. RR
2624, 25elicc2i 11729 . . . . . . . . . . . 12 |- ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
2726simp1bi 1029 . . . . . . . . . . 11 |- ( t e. ( 0 [,] 1 ) -> t e. RR )
2827recnd 9695 . . . . . . . . . 10 |- ( t e. ( 0 [,] 1 ) -> t e. CC )
2928ad2antrr 737 . . . . . . . . 9 |- ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) -> t e. CC )
30293ad2ant1 1035 . . . . . . . 8 |- ( ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) -> t e. CC )
3130adantl 472 . . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> t e. CC )
32 simpl11 1089 . . . . . . . 8 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> N e. NN )
33 simp12 1045 . . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
34 simp13 1046 . . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
35 simp21 1047 . . . . . . . . . 10 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
3633, 34, 353jca 1194 . . . . . . . . 9 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
3736adantr 471 . . . . . . . 8 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
38 simprrl 779 . . . . . . . . . 10 |- ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) )
39383ad2ant1 1035 . . . . . . . . 9 |- ( ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) )
4039adantl 472 . . . . . . . 8 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) )
41 simp1rl 1079 . . . . . . . . 9 |- ( ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) -> A =/= B )
4241adantl 472 . . . . . . . 8 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> A =/= B )
43 ax5seglem4 25011 . . . . . . . 8 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A =/= B ) -> t =/= 0 )
4432, 37, 40, 42, 43syl211anc 1282 . . . . . . 7 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> t =/= 0 )
45 simpr3r 1076 . . . . . . . . . . 11 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> <. B , D >.Cgr <. F , H >. )
46 simpl13 1091 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> B e. ( EE ` N ) )
47 simpl22 1093 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> D e. ( EE ` N ) )
48 simpl31 1095 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> F e. ( EE ` N ) )
49 simpl33 1097 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> H e. ( EE ` N ) )
50 brcgr 24979 . . . . . . . . . . . 12 |- ( ( ( B e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , D >.Cgr <. F , H >. <-> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( F ` j ) - ( H ` j ) ) ^ 2 ) ) )
5146, 47, 48, 49, 50syl22anc 1277 . . . . . . . . . . 11 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( <. B , D >.Cgr <. F , H >. <-> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( F ` j ) - ( H ` j ) ) ^ 2 ) ) )
5245, 51mpbid 215 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( F ` j ) - ( H ` j ) ) ^ 2 ) )
53 simp23 1049 . . . . . . . . . . . . . . . 16 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
54 simp31 1050 . . . . . . . . . . . . . . . 16 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
55 simp32 1051 . . . . . . . . . . . . . . . 16 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
5653, 54, 553jca 1194 . . . . . . . . . . . . . . 15 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) )
5736, 56jca 539 . . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) )
5857adantr 471 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) )
59 simpr1l 1071 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) )
60 simprrr 780 . . . . . . . . . . . . . . . 16 |- ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) -> A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) )
61603ad2ant1 1035 . . . . . . . . . . . . . . 15 |- ( ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) -> A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) )
6261adantl 472 . . . . . . . . . . . . . 14 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) )
6340, 62jca 539 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) )
64 simpr2l 1073 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> <. A , B >.Cgr <. E , F >. )
65 simpr2r 1074 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> <. B , C >.Cgr <. F , G >. )
66 ax5seglem6 25013 . . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) ) /\ ( A =/= B /\ ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) ) -> t = s )
6732, 58, 42, 59, 63, 64, 65, 66syl232anc 1303 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> t = s )
6867oveq2d 6331 . . . . . . . . . . 11 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( 1 - t ) = ( 1 - s ) )
6956adantr 471 . . . . . . . . . . . . . 14 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) )
70 ax5seglem3 25010 . . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) /\ ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) )
7132, 37, 69, 59, 63, 64, 65, 70syl322anc 1304 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) )
7267, 71oveq12d 6333 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( t x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( s x. sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) ) )
73 simpr3l 1075 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> <. A , D >.Cgr <. E , H >. )
74 simpl12 1090 . . . . . . . . . . . . . 14 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> A e. ( EE ` N ) )
75 simpl23 1094 . . . . . . . . . . . . . 14 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> E e. ( EE ` N ) )
76 brcgr 24979 . . . . . . . . . . . . . 14 |- ( ( ( A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , D >.Cgr <. E , H >. <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) ) )
7774, 47, 75, 49, 76syl22anc 1277 . . . . . . . . . . . . 13 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( <. A , D >.Cgr <. E , H >. <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) ) )
7873, 77mpbid 215 . . . . . . . . . . . 12 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) )
7972, 78oveq12d 6333 . . . . . . . . . . 11 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( ( t x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) = ( ( s x. sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) ) )
8068, 79oveq12d 6333 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( ( 1 - t ) x. ( ( t x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) = ( ( 1 - s ) x. ( ( s x. sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) ) ) )
8152, 80oveq12d 6333 . . . . . . . . 9 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - t ) x. ( ( t x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( F ` j ) - ( H ` j ) ) ^ 2 ) + ( ( 1 - s ) x. ( ( s x. sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) ) ) ) )
8233, 34jca 539 . . . . . . . . . . . 12 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
83 simp22 1048 . . . . . . . . . . . 12 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
8482, 35, 83jca32 542 . . . . . . . . . . 11 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) )
8584adantr 471 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) )
86 simp1ll 1077 . . . . . . . . . . 11 |- ( ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) -> t e. ( 0 [,] 1 ) )
8786adantl 472 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> t e. ( 0 [,] 1 ) )
88 ax5seglem9 25016 . . . . . . . . . 10 |- ( ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) ) /\ ( t e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) ) ) -> ( t x. sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - t ) x. ( ( t x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
8932, 85, 87, 40, 88syl22anc 1277 . . . . . . . . 9 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( t x. sum_ j e. ( 1 ... N ) ( ( ( C ` j ) - ( D ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( D ` j ) ) ^ 2 ) + ( ( 1 - t ) x. ( ( t x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( D ` j ) ) ^ 2 ) ) ) ) )
90 3simpc 1013 . . . . . . . . . . . . 13 |- ( ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) -> ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) )
91903ad2ant3 1037 . . . . . . . . . . . 12 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) )
9253, 54, 91jca31 541 . . . . . . . . . . 11 |- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) )
9392adantr 471 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) )
94 simp1lr 1078 . . . . . . . . . . 11 |- ( ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) -> s e. ( 0 [,] 1 ) )
9594adantl 472 . . . . . . . . . 10 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> s e. ( 0 [,] 1 ) )
96 ax5seglem9 25016 . . . . . . . . . 10 |- ( ( ( N e. NN /\ ( ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) ) /\ ( s e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) -> ( s x. sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( F ` j ) - ( H ` j ) ) ^ 2 ) + ( ( 1 - s ) x. ( ( s x. sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) ) ) ) )
9732, 93, 95, 62, 96syl22anc 1277 . . . . . . . . 9 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <. B , C >.Cgr <. F , G >. ) /\ ( <. A , D >.Cgr <. E , H >. /\ <. B , D >.Cgr <. F , H >. ) ) ) -> ( s x. sum_ j e. ( 1 ... N ) ( ( ( G ` j ) - ( H ` j ) ) ^ 2 ) ) = ( sum_ j e. ( 1 ... N ) ( ( ( F ` j ) - ( H ` j ) ) ^ 2 ) + ( ( 1 - s ) x. ( ( s x. sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( G ` j ) ) ^ 2 ) ) - sum_ j e. ( 1 ... N ) ( ( ( E ` j ) - ( H ` j ) ) ^ 2 ) ) ) ) )
9881, 89, 973eqtr4d 2506 . . . . . . . 8 |- ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( ( ( t e. ( 0 [,] 1 ) /\ s e. ( 0 [,] 1 ) ) /\ ( A =/= B /\ ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - t ) x. ( A ` i ) ) + ( t x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( F ` i ) = ( ( ( 1 - s ) x. ( E ` i ) ) + ( s x. ( G ` i ) ) ) ) ) ) /\ ( <. A , B >.Cgr <. E , F >. /\ <.