let x, y be FinSequence of COMPLEX ; ( 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
; |(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 *')))
; verum