MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax5seg Structured version   Unicode version
Theorem ax5seg 24910
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 12136 . . . . . . . . . 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 1083 . . . . . . . . . . . . 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 24873 . . . . . . . . . . . . 13 |- ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. RR )
42, 3sylancom 671 . . . . . . . . . . . 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 1084 . . . . . . . . . . . . 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 24873 . . . . . . . . . . . . 13 |- ( ( D e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. RR )
75, 6sylancom 671 . . . . . . . . . . . 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 9998 . . . . . . . . . . 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 12392 . . . . . . . . . 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 13743 . . . . . . . . 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 9620 . . . . . . . 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 466 . . . . . . 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 1087 . . . . . . . . . . . . 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 24873 . . . . . . . . . . . . 13 |- ( ( G e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( G ` j ) e. RR )
1513, 14sylancom 671 . . . . . . . . . . . 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 1088 . . . . . . . . . . . . 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 24873 . . . . . . . . . . . . 13 |- ( ( H e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( H ` j ) e. RR )
1816, 17sylancom 671 . . . . . . . . . . . 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 9998 . . . . . . . . . . 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 12392 . . . . . . . . . 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 13743 . . . . . . . . 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 9620 . . . . . . . 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 466 . . . . . . 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 9594 . . . . . . . . . . . . 13 |- 0 e. RR
25 1re 9593 . . . . . . . . . . . . 13 |- 1 e. RR
2624, 25elicc2i 11651 . . . . . . . . . . . 12 |- ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
2726simp1bi 1020 . . . . . . . . . . 11 |- ( t e. ( 0 [,] 1 ) -> t e. RR )
2827recnd 9620 . . . . . . . . . 10 |- ( t e. ( 0 [,] 1 ) -> t e. CC )
2928ad2antrr 730 . . . . . . . . 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 1026 . . . . . . . 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 467 . . . . . . 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 1080 . . . . . . . 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 1036 . . . . . . . . . 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 1037 . . . . . . . . . 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 1038 . . . . . . . . . 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 1185 . . . . . . . . 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 466 . . . . . . . 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 772 . . . . . . . . . 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 1026 . . . . . . . . 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 467 . . . . . . . 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 1070 . . . . . . . . 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 467 . . . . . . . 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 24904 . . . . . . . 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 1270 . . . . . . 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 1067 . . . . . . . . . . 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 1082 . . . . . . . . . . . 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 1084 . . . . . . . . . . . 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 1086 . . . . . . . . . . . 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 1088 . . . . . . . . . . . 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 24872 . . . . . . . . . . . 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 1265 . . . . . . . . . . 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 213 . . . . . . . . . 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 1040 . . . . . . . . . . . . . . . 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 1041 . . . . . . . . . . . . . . . 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 1042 . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . 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 1062 . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . 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 1064 . . . . . . . . . . . . 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 1065 . . . . . . . . . . . . 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 24906 . . . . . . . . . . . . 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 1291 . . . . . . . . . . . 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 6265 . . . . . . . . . . 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 466 . . . . . . . . . . . . . 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 24903 . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . 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 6267 . . . . . . . . . . . 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 1066 . . . . . . . . . . . . 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 1081 . . . . . . . . . . . . . 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 1085 . . . . . . . . . . . . . 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 24872 . . . . . . . . . . . . . 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 1265 . . . . . . . . . . . . 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 213 . . . . . . . . . . . 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 6267 . . . . . . . . . . 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 6267 . . . . . . . . . 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 6267 . . . . . . . . 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 534 . . . . . . . . . . . 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 1039 . . . . . . . . . . . 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 537 . . . . . . . . . . 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 466 . . . . . . . . . 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 1068 . . . . . . . . . . 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 467 . . . . . . . . . 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 24909 . . . . . . . . . 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 1265 . . . . . . . . 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 1004 . . . . . . . . . . . . 13 |- ( ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) -> ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) )
91903ad2ant3 1028 . . . . . . . . . . . 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 536 . . . . . . . . . . 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 466 . . . . . . . . . 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 1069 . . . . . . . . . . 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 467 . . . . . . . . . 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 24909 . . . . . . . . . 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 1265 . . . . . . . . 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 2472 . . . . . . . 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 ,