let x, y be FinSequence of COMPLEX ; :: thesis:
A1: len (Im y) = len y by COMPLSP2:48;
A2: len (y *' ) = len (y *' ) ;
A3: y *' = - (- (y *' ))
.= ((- 1) * (- 1)) * (y *' ) by COMPLSP2:53
.= 1 * (y *' ) ;
A4: len (x *' ) = len x by COMPLSP2:def 1;
then A5: len (x + (x *' )) = len x by COMPLSP2:6;
A6: len ((x *' ) + x) = len x by A4, COMPLSP2:6;
A7: len x = len x ;
A8: x = - (- x)
.= ((- 1) * (- 1)) * x by COMPLSP2:53
.= 1 * x ;
set Imx = FR2FC (Im x);
assume A9: len x = len y ; :: thesis:
A10: len (FR2FC (Im x)) = len y by A9, COMPLSP2:48
.= len (y *' ) by COMPLSP2:def 1 ;
set Imy = FR2FC (Im y);
set Rey = FR2FC (Re y);
set Rex = FR2FC (Re x);
A11: len ( * (FR2FC (Im x))) = len (FR2FC (Im x)) by COMPLSP2:3
.= len x by COMPLSP2:48
.= len (FR2FC (Re x)) by COMPLSP2:48 ;
A12: len (FR2FC (Re x)) = len x by COMPLSP2:48;
A13: len (Im x) = len x by COMPLSP2:48;
then A14: mlt (Im x),(Im y) = mlt (FR2FC (Im x)),(FR2FC (Im y)) by A9, A1, Th38;
A15: len (Re y) = len y by COMPLSP2:48;
then A16: mlt (Im x),(Re y) = mlt (FR2FC (Im x)),(FR2FC (Re y)) by A9, A13, Th38;
A17: len (Re x) = len x by COMPLSP2:48;
then A18: mlt (Re x),(Re y) = mlt (FR2FC (Re x)),(FR2FC (Re y)) by A9, A15, Th38;
A19: mlt (Re x),(Im y) = mlt (FR2FC (Re x)),(FR2FC (Im y)) by A9, A17, A1, Th38;
A20: len ( * (FR2FC (Im x))) = len (FR2FC (Im x)) by COMPLSP2:3
.= len y by A9, COMPLSP2:48
.= len (y *' ) by COMPLSP2:def 1 ;
FR2FC (Im x) = (- ((1 / 2) * )) * (x - (x *' )) by COMPLSP2:def 3;
then A21: * (FR2FC (Im x)) = ( * (- ((1 / 2) * ))) * (x - (x *' )) by COMPLSP2:53
.= (1 / 2) * (x - (x *' )) ;
FR2FC (Im y) = (- ((1 / 2) * )) * (y - (y *' )) by COMPLSP2:def 3;
then A22: * (FR2FC (Im y)) = ( * (- ((1 / 2) * ))) * (y - (y *' )) by COMPLSP2:53
.= (1 / 2) * (y - (y *' )) ;
A23: FR2FC (Re x) = (1 / 2) * (x + (x *' )) by COMPLSP2:def 2;
A24: len (y *' ) = len y by COMPLSP2:def 1;
then A25: len (y + (y *' )) = len y by COMPLSP2:6;
len (x - (x *' )) = len x by A4, COMPLSP2:7;
then A26: (FR2FC (Re x)) + ( * (FR2FC (Im x))) = (1 / 2) * ((x + (x *' )) + (x - (x *' ))) by A23, A21, A5, COMPLSP2:30
.= (1 / 2) * ((x + ((x *' ) + x)) - (x *' )) by A4, A5, COMPLSP2:37
.= (1 / 2) * (x + ((x + (x *' )) - (x *' ))) by A4, A6, COMPLSP2:37
.= (1 / 2) * (x + (x + ((x *' ) - (x *' )))) by A4, COMPLSP2:37
.= (1 / 2) * (x + (x + (0c (len (x *' ))))) by COMPLSP2:34
.= (1 / 2) * (x + (x + (0c (len x)))) by COMPLSP2:def 1
.= (1 / 2) * (x + x) by COMPLSP2:33
.= ((1 / 2) * x) + ((1 / 2) * x) by A7, COMPLSP2:30
.= ((1 / 2) + (1 / 2)) * x by COMPLSP2:63
.= x by A8 ;
A27: FR2FC (Re y) = (1 / 2) * (y + (y *' )) by COMPLSP2:def 2;
len (y - (y *' )) = len y by A24, COMPLSP2:7;
then A28: (FR2FC (Re y)) - ( * (FR2FC (Im y))) = (1 / 2) * ((y + (y *' )) - (y - (y *' ))) by A27, A22, A25, COMPLSP2:43
.= (1 / 2) * ((((y *' ) + y) - y) + (y *' )) by A24, A25, COMPLSP2:40
.= (1 / 2) * (((y *' ) + (y - y)) + (y *' )) by A24, COMPLSP2:37
.= (1 / 2) * (((y *' ) + (0c (len y))) + (y *' )) by COMPLSP2:34
.= (1 / 2) * ((y *' ) + (y *' )) by A24, COMPLSP2:33
.= ((1 / 2) * (y *' )) + ((1 / 2) * (y *' )) by A2, COMPLSP2:30
.= ((1 / 2) + (1 / 2)) * (y *' ) by COMPLSP2:63
.= y *' by A3 ;
A29: len (FR2FC (Re y)) = len y by COMPLSP2:48;
then A30: len (mlt (FR2FC (Re x)),(FR2FC (Re y))) = len x by A9, A12, FINSEQ_2:86;
A31: len ( * (FR2FC (Im y))) = len (FR2FC (Im y)) by COMPLSP2:3
.= len y by COMPLSP2:48 ;
then len (mlt (FR2FC (Re x)),( * (FR2FC (Im y)))) = len (FR2FC (Re x)) by A9, A12, FINSEQ_2:86;
then A32: len ((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) = len (mlt (FR2FC (Re x)),(FR2FC (Re y))) by A12, A30, COMPLSP2:7;
A33: len (FR2FC (Im x)) = len x by COMPLSP2:48;
then len (mlt (FR2FC (Im x)),(FR2FC (Re y))) = len x by A9, A29, FINSEQ_2:86;
then A34: len (mlt (FR2FC (Im x)),(FR2FC (Re y))) = len (mlt (FR2FC (Im x)),( * (FR2FC (Im y)))) by A9, A31, A33, FINSEQ_2:86;
A35: len (FR2FC (Im y)) = len y by COMPLSP2:48;
then A36: len (mlt (FR2FC (Im x)),(FR2FC (Im y))) = len x by A9, A33, FINSEQ_2:86;
A37: len ( * (mlt (FR2FC (Re x)),(FR2FC (Im y)))) = len (mlt (FR2FC (Re x)),(FR2FC (Im y))) by COMPLSP2:3
.= len x by A9, A12, A35, FINSEQ_2:86 ;
A38: len ( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))) = len (mlt (FR2FC (Im x)),(FR2FC (Re y))) by COMPLSP2:3
.= len x by A9, A29, A33, FINSEQ_2:86 ;
then A39: len ((mlt (FR2FC (Re x)),(FR2FC (Re y))) - ( * (mlt (FR2FC (Re x)),(FR2FC (Im y))))) = len ( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))) by A30, A37, COMPLSP2:7;
len ((mlt (FR2FC (Re x)),(FR2FC (Re y))) - ( * (mlt (FR2FC (Re x)),(FR2FC (Im y))))) = len ( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))) by A30, A37, A38, COMPLSP2:7;
then A40: len (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - ( * (mlt (FR2FC (Re x)),(FR2FC (Im y))))) + ( * (mlt (FR2FC (Im x)),(FR2FC (Re y))))) = len ((mlt (FR2FC (Re x)),(FR2FC (Re y))) - ( * (mlt (FR2FC (Re x)),(FR2FC (Im y))))) by COMPLSP2:6
.= len (mlt (FR2FC (Im x)),(FR2FC (Im y))) by A36, A30, A37, COMPLSP2:7 ;
|(x,y)| = ((|((Re x),(Re y))| - ( * |((Re x),(Im y))|)) + ( * |((Im x),(Re y))|)) + |((Im x),(Im y))| by COMPLSP2:def 4
.= (((Sum (mlt (Re x),(Re y))) - ( * |((Re x),(Im y))|)) + ( * |((Im x),(Re y))|)) + |((Im x),(Im y))|
.= (((Sum (mlt (Re x),(Re y))) - ( * (Sum (mlt (Re x),(Im y))))) + ( * |((Im x),(Re y))|)) + |((Im x),(Im y))|
.= (((Sum (mlt (Re x),(Re y))) - ( * (Sum (mlt (Re x),(Im y))))) + ( * (Sum (mlt (Im x),(Re y))))) + |((Im x),(Im y))|
.= (((Sum (mlt (FR2FC (Re x)),(FR2FC (Re y)))) - ( * (Sum (mlt (FR2FC (Re x)),(FR2FC (Im y)))))) + ( * (Sum (mlt (FR2FC (Im x)),(FR2FC (Re y)))))) + (Sum (mlt (Im x),(Im y))) by A16, A18, A19
.= (((Sum (mlt (FR2FC (Re x)),(FR2FC (Re y)))) - (Sum ( * (mlt (FR2FC (Re x)),(FR2FC (Im y)))))) + ( * (Sum (mlt (FR2FC (Im x)),(FR2FC (Re y)))))) + (Sum (mlt (FR2FC (Im x)),(FR2FC (Im y)))) by A14, Th29
.= (((Sum (mlt (FR2FC (Re x)),(FR2FC (Re y)))) - (Sum ( * (mlt (FR2FC (Re x)),(FR2FC (Im y)))))) + (Sum ( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))))) + (Sum (mlt (FR2FC (Im x)),(FR2FC (Im y)))) by Th29
.= ((Sum ((mlt (FR2FC (Re x)),(FR2FC (Re y))) - ( * (mlt (FR2FC (Re x)),(FR2FC (Im y)))))) + (Sum ( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))))) + (Sum (mlt (FR2FC (Im x)),(FR2FC (Im y)))) by A30, A37, Th32
.= (Sum (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - ( * (mlt (FR2FC (Re x)),(FR2FC (Im y))))) + ( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))))) + (Sum (mlt (FR2FC (Im x)),(FR2FC (Im y)))) by A39, Th37
.= Sum ((((mlt (FR2FC (Re x)),(FR2FC (Re y))) - ( * (mlt (FR2FC (Re x)),(FR2FC (Im y))))) + ( * (mlt (FR2FC (Im x)),(FR2FC (Re y))))) + (mlt (FR2FC (Im x)),(FR2FC (Im y)))) by A40, Th37
.= Sum ((((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) + ( * (mlt (FR2FC (Im x)),(FR2FC (Re y))))) + (mlt (FR2FC (Im x)),(FR2FC (Im y)))) by A9, A12, A35, Th26
.= Sum (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) + (( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))) + (- (- (mlt (FR2FC (Im x)),(FR2FC (Im y))))))) by A36, A30, A38, A32, COMPLSP2:28
.= Sum (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) + (( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))) - (( * ) * (mlt (FR2FC (Im x)),(FR2FC (Im y))))))
.= Sum (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) + (( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))) - ( * ( * (mlt (FR2FC (Im x)),(FR2FC (Im y))))))) by COMPLSP2:53
.= Sum (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) + (( * (mlt (FR2FC (Im x)),(FR2FC (Re y)))) - ( * (mlt (FR2FC (Im x)),( * (FR2FC (Im y))))))) by A9, A35, A33, Th26
.= Sum (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) + ( * ((mlt (FR2FC (Im x)),(FR2FC (Re y))) - (mlt (FR2FC (Im x)),( * (FR2FC (Im y))))))) by A34, COMPLSP2:43
.= Sum (((mlt (FR2FC (Re x)),(FR2FC (Re y))) - (mlt (FR2FC (Re x)),( * (FR2FC (Im y))))) + ( * (mlt (FR2FC (Im x)),(y *' )))) by A9, A31, A29, A33, A28, Th34
.= Sum ((mlt (FR2FC (Re x)),((FR2FC (Re y)) - ( * (FR2FC (Im y))))) + ( * (mlt (FR2FC (Im x)),(y *' )))) by A9, A31, A29, A12, Th34
.= Sum ((mlt (FR2FC (Re x)),(y *' )) + (mlt ( * (FR2FC (Im x))),(y *' ))) by A10, A28, Th27
.= Sum (mlt x,(y *' )) by A11, A20, A26, Th36 ;
hence |(x,y)| = Sum (mlt x,(y *' )) ; :: thesis: