let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies |(x,y)| = Sum (mlt (x,(y *'))) )
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: |(x,y)| = Sum (mlt (x,(y *')))
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 (<i> * (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, Th35;
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, Th35;
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, Th35;
A19: mlt ((Re x),(Im y)) = mlt ((FR2FC (Re x)),(FR2FC (Im y))) by A9, A17, A1, Th35;
A20: len (<i> * (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) * <i>)) * (x - (x *')) by COMPLSP2:def 3;
then A21: <i> * (FR2FC (Im x)) = (<i> * (- ((1 / 2) * <i>))) * (x - (x *')) by COMPLSP2:53
.= (1 / 2) * (x - (x *')) ;
FR2FC (Im y) = (- ((1 / 2) * <i>)) * (y - (y *')) by COMPLSP2:def 3;
then A22: <i> * (FR2FC (Im y)) = (<i> * (- ((1 / 2) * <i>))) * (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)) + (<i> * (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)) - (<i> * (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:72;
A31: len (<i> * (FR2FC (Im y))) = len (FR2FC (Im y)) by COMPLSP2:3
.= len y by COMPLSP2:48 ;
then len (mlt ((FR2FC (Re x)),(<i> * (FR2FC (Im y))))) = len (FR2FC (Re x)) by A9, A12, FINSEQ_2:72;
then A32: len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(<i> * (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:72;
then A34: len (mlt ((FR2FC (Im x)),(FR2FC (Re y)))) = len (mlt ((FR2FC (Im x)),(<i> * (FR2FC (Im y))))) by A9, A31, A33, FINSEQ_2:72;
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:72;
A37: len (<i> * (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:72 ;
A38: len (<i> * (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:72 ;
then A39: len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) = len (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) by A30, A37, COMPLSP2:7;
len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) = len (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) by A30, A37, A38, COMPLSP2:7;
then A40: len (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) + (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y)))))) = len ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (<i> * (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))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| by COMPLSP2:def 4
.= (((Sum (mlt ((Re x),(Re y)))) - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|
.= (((Sum (mlt ((Re x),(Re y)))) - (<i> * (Sum (mlt ((Re x),(Im y)))))) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|
.= (((Sum (mlt ((Re x),(Re y)))) - (<i> * (Sum (mlt ((Re x),(Im y)))))) + (<i> * (Sum (mlt ((Im x),(Re y)))))) + |((Im x),(Im y))|
.= (((Sum (mlt ((FR2FC (Re x)),(FR2FC (Re y))))) - (<i> * (Sum (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (<i> * (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 (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (<i> * (Sum (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A14, Th26
.= (((Sum (mlt ((FR2FC (Re x)),(FR2FC (Re y))))) - (Sum (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (Sum (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by Th26
.= ((Sum ((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y))))))) + (Sum (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A30, A37, Th29
.= (Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) + (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))))) + (Sum (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A39, Th34
.= Sum ((((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (<i> * (mlt ((FR2FC (Re x)),(FR2FC (Im y)))))) + (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y)))))) + (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A40, Th34
.= Sum ((((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(<i> * (FR2FC (Im y)))))) + (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y)))))) + (mlt ((FR2FC (Im x)),(FR2FC (Im y))))) by A9, A12, A35, Th23
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(<i> * (FR2FC (Im y)))))) + ((<i> * (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)),(<i> * (FR2FC (Im y)))))) + ((<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) - ((<i> * <i>) * (mlt ((FR2FC (Im x)),(FR2FC (Im y)))))))
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(<i> * (FR2FC (Im y)))))) + ((<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) - (<i> * (<i> * (mlt ((FR2FC (Im x)),(FR2FC (Im y)))))))) by COMPLSP2:53
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(<i> * (FR2FC (Im y)))))) + ((<i> * (mlt ((FR2FC (Im x)),(FR2FC (Re y))))) - (<i> * (mlt ((FR2FC (Im x)),(<i> * (FR2FC (Im y)))))))) by A9, A35, A33, Th23
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(<i> * (FR2FC (Im y)))))) + (<i> * ((mlt ((FR2FC (Im x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Im x)),(<i> * (FR2FC (Im y)))))))) by A34, COMPLSP2:43
.= Sum (((mlt ((FR2FC (Re x)),(FR2FC (Re y)))) - (mlt ((FR2FC (Re x)),(<i> * (FR2FC (Im y)))))) + (<i> * (mlt ((FR2FC (Im x)),(y *'))))) by A9, A31, A29, A33, A28, Th31
.= Sum ((mlt ((FR2FC (Re x)),((FR2FC (Re y)) - (<i> * (FR2FC (Im y)))))) + (<i> * (mlt ((FR2FC (Im x)),(y *'))))) by A9, A31, A29, A12, Th31
.= Sum ((mlt ((FR2FC (Re x)),(y *'))) + (mlt ((<i> * (FR2FC (Im x))),(y *')))) by A10, A28, Th24
.= Sum (mlt (x,(y *'))) by A11, A20, A26, Th33 ;
hence |(x,y)| = Sum (mlt (x,(y *'))) ; :: thesis: verum