MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax5seg Structured version   Unicode version
Theorem ax5seg 23007
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 11779 . . . . . . . . . 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 1059 . . . . . . . . . . . . 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 22970 . . . . . . . . . . . . 13 |- ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. RR )
42, 3sylancom 660 . . . . . . . . . . . 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 1060 . . . . . . . . . . . . 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 22970 . . . . . . . . . . . . 13 |- ( ( D e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( D ` j ) e. RR )
75, 6sylancom 660 . . . . . . . . . . . 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 9764 . . . . . . . . . . 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 12018 . . . . . . . . . 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 13195 . . . . . . . . 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 9400 . . . . . . . 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 462 . . . . . . 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 1063 . . . . . . . . . . . . 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 22970 . . . . . . . . . . . . 13 |- ( ( G e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( G ` j ) e. RR )
1513, 14sylancom 660 . . . . . . . . . . . 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 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 ) ) ) /\ j e. ( 1 ... N ) ) -> H e. ( EE ` N ) )
17 fveere 22970 . . . . . . . . . . . . 13 |- ( ( H e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( H ` j ) e. RR )
1816, 17sylancom 660 . . . . . . . . . . . 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 9764 . . . . . . . . . . 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 12018 . . . . . . . . . 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 13195 . . . . . . . . 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 9400 . . . . . . . 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 462 . . . . . . 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 9374 . . . . . . . . . . . . 13 |- 0 e. RR
25 1re 9373 . . . . . . . . . . . . 13 |- 1 e. RR
2624, 25elicc2i 11349 . . . . . . . . . . . 12 |- ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
2726simp1bi 996 . . . . . . . . . . 11 |- ( t e. ( 0 [,] 1 ) -> t e. RR )
2827recnd 9400 . . . . . . . . . 10 |- ( t e. ( 0 [,] 1 ) -> t e. CC )
2928ad2antrr 718 . . . . . . . . 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 1002 . . . . . . . 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 463 . . . . . . 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 1056 . . . . . . . 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 1012 . . . . . . . . . 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 1013 . . . . . . . . . 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 1014 . . . . . . . . . 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 1161 . . . . . . . . 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 462 . . . . . . . 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 756 . . . . . . . . . 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 1002 . . . . . . . . 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 463 . . . . . . . 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 1046 . . . . . . . . 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 463 . . . . . . . 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 23001 . . . . . . . 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 1217 . . . . . . 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 1043 . . . . . . . . . . 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 1058 . . . . . . . . . . . 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 1060 . . . . . . . . . . . 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 1062 . . . . . . . . . . . 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 1064 . . . . . . . . . . . 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 22969 . . . . . . . . . . . 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 1212 . . . . . . . . . . 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 210 . . . . . . . . . 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 1016 . . . . . . . . . . . . . . . 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 1017 . . . . . . . . . . . . . . . 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 1018 . . . . . . . . . . . . . . . 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 1161 . . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 1038 . . . . . . . . . . . . 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 757 . . . . . . . . . . . . . . . 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 1002 . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . 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 529 . . . . . . . . . . . . 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 1040 . . . . . . . . . . . . 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 1041 . . . . . . . . . . . . 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 23003 . . . . . . . . . . . . 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 1238 . . . . . . . . . . . 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 6096 . . . . . . . . . . 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 462 . . . . . . . . . . . . . 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 23000 . . . . . . . . . . . . . 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 1239 . . . . . . . . . . . . 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 6098 . . . . . . . . . . . 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 1042 . . . . . . . . . . . . 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 1057 . . . . . . . . . . . . . 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 1061 . . . . . . . . . . . . . 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 22969 . . . . . . . . . . . . . 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 1212 . . . . . . . . . . . . 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 210 . . . . . . . . . . . 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 6098 . . . . . . . . . . 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 6098 . . . . . . . . . 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 6098 . . . . . . . . 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 529 . . . . . . . . . . . 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 1015 . . . . . . . . . . . 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 532 . . . . . . . . . . 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 462 . . . . . . . . . 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 1044 . . . . . . . . . . 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 463 . . . . . . . . . 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 23006 . . . . . . . . . 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 1212 . . . . . . . . 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 980 . . . . . . . . . . . . 13 |- ( ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) -> ( G e. ( EE ` N ) /\ H e. ( EE ` N ) ) )
91903ad2ant3 1004 . . . . . . . . . . . 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 531 . . . . . . . . . . 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 462 . . . . . . . . . 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 1045 . . . . . . . . . . 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 463 . . . . . . . . . 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 23006 . . . . . . . . . 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 1212 . . . . . . . . 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 2475 . . . . . . . 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 ,