Metamath Proof Explorer

Theorem ax5seglem6

Description: Lemma for ax5seg . Given two line segments that are divided into pieces, if the pieces are congruent, then the scaling constant is the same. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion ax5seglem6 
|- ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> T = S )

Proof

Step Hyp Ref Expression
1 simp22l 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> T e. ( 0 [,] 1 ) )
2 elicc01 
 |-  ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
3 2 simp1bi 
 |-  ( T e. ( 0 [,] 1 ) -> T e. RR )
4 resqcl 
 |-  ( T e. RR -> ( T ^ 2 ) e. RR )
5 4 recnd 
 |-  ( T e. RR -> ( T ^ 2 ) e. CC )
6 1 3 5 3syl 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( T ^ 2 ) e. CC )
7 simp22r 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> S e. ( 0 [,] 1 ) )
8 elicc01 
 |-  ( S e. ( 0 [,] 1 ) <-> ( S e. RR /\ 0 <_ S /\ S <_ 1 ) )
9 8 simp1bi 
 |-  ( S e. ( 0 [,] 1 ) -> S e. RR )
10 resqcl 
 |-  ( S e. RR -> ( S ^ 2 ) e. RR )
11 10 recnd 
 |-  ( S e. RR -> ( S ^ 2 ) e. CC )
12 7 9 11 3syl 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( S ^ 2 ) e. CC )
13 fzfid 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( 1 ... N ) e. Fin )
14 simprl1 
 |-  ( ( 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 ) ) ) ) -> A e. ( EE ` N ) )
15 14 3ad2ant1 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> A e. ( EE ` N ) )
16 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
17 15 16 sylan 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
18 simprl3 
 |-  ( ( 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 ) ) ) ) -> C e. ( EE ` N ) )
19 18 3ad2ant1 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> C e. ( EE ` N ) )
20 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
21 19 20 sylan 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
22 17 21 subcld 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
23 22 sqcld 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
24 13 23 fsumcl 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
25 simp1l 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> N e. NN )
26 simp1rl 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
27 simp21 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> A =/= B )
28 simp23l 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) )
29 ax5seglem5 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 )
30 25 26 27 1 28 29 syl23anc 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 )
31 simp3l 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. A , B >. Cgr <. D , E >. )
32 simprl2 
 |-  ( ( 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 ) ) ) ) -> B e. ( EE ` N ) )
33 simprr1 
 |-  ( ( 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 ) ) ) ) -> D e. ( EE ` N ) )
34 simprr2 
 |-  ( ( 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 ) ) ) ) -> E e. ( EE ` N ) )
35 brcgr 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) ) )
36 14 32 33 34 35 syl22anc 
 |-  ( ( 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 ) ) ) ) -> ( <. A , B >. Cgr <. D , E >. <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) ) )
37 36 3ad2ant1 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( <. A , B >. Cgr <. D , E >. <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) ) )
38 31 37 mpbid 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) )
39 ax5seglem1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
40 25 15 19 1 28 39 syl122anc 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( B ` j ) ) ^ 2 ) = ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
41 33 3ad2ant1 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> D e. ( EE ` N ) )
42 simprr3 
 |-  ( ( 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 ) ) ) ) -> F e. ( EE ` N ) )
43 42 3ad2ant1 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> F e. ( EE ` N ) )
44 simp23r 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) )
45 ax5seglem1 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( S e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
46 25 41 43 7 44 45 syl122anc 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( E ` j ) ) ^ 2 ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
47 38 40 46 3eqtr3d 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
48 simp1rr 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) )
49 simp22 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( T e. ( 0 [,] 1 ) /\ S e. ( 0 [,] 1 ) ) )
50 simp23 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A. i e. ( 1 ... N ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) )
51 simp3r 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> <. B , C >. Cgr <. E , F >. )
52 ax5seglem3 
 |-  ( ( ( 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 ) ) ) /\ ( ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )
53 25 26 48 49 50 31 51 52 syl322anc 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) )
54 53 oveq2d 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( D ` j ) - ( F ` j ) ) ^ 2 ) ) )
55 47 54 eqtr4d 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( T ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = ( ( S ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
56 6 12 24 30 55 mulcan2ad 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( T ^ 2 ) = ( S ^ 2 ) )
57 2 simp2bi 
 |-  ( T e. ( 0 [,] 1 ) -> 0 <_ T )
58 3 57 jca 
 |-  ( T e. ( 0 [,] 1 ) -> ( T e. RR /\ 0 <_ T ) )
59 1 58 syl 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( T e. RR /\ 0 <_ T ) )
60 8 simp2bi 
 |-  ( S e. ( 0 [,] 1 ) -> 0 <_ S )
61 9 60 jca 
 |-  ( S e. ( 0 [,] 1 ) -> ( S e. RR /\ 0 <_ S ) )
62 7 61 syl 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( S e. RR /\ 0 <_ S ) )
63 sq11 
 |-  ( ( ( T e. RR /\ 0 <_ T ) /\ ( S e. RR /\ 0 <_ S ) ) -> ( ( T ^ 2 ) = ( S ^ 2 ) <-> T = S ) )
64 59 62 63 syl2anc 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> ( ( T ^ 2 ) = ( S ^ 2 ) <-> T = S ) )
65 56 64 mpbid 
 |-  ( ( ( 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 ) ) ) ) /\ ( 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 ) ( E ` i ) = ( ( ( 1 - S ) x. ( D ` i ) ) + ( S x. ( F ` i ) ) ) ) ) /\ ( <. A , B >. Cgr <. D , E >. /\ <. B , C >. Cgr <. E , F >. ) ) -> T = S )