let x, y, z be FinSequence of COMPLEX ; :: thesis: ( len x = len y & len y = len z implies mlt (x - y),z = (mlt x,z) - (mlt y,z) )
assume
( len x = len y & len y = len z )
; :: thesis: mlt (x - y),z = (mlt x,z) - (mlt y,z)
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
A1: dom (mlt (x - y),z) =
Seg (len (mlt (x2 - y2),z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
.=
Seg (len ((mlt x2,z2) - (mlt y2,z2)))
by FINSEQ_1:def 18
.=
dom ((mlt x2,z2) - (mlt y2,z2))
by FINSEQ_1:def 3
;
A2: dom (mlt x,z) =
Seg (len (mlt x2,z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
.=
Seg (len ((mlt x2,z2) - (mlt y2,z2)))
by FINSEQ_1:def 18
.=
dom ((mlt x2,z2) - (mlt y2,z2))
by FINSEQ_1:def 3
;
A3: dom (mlt y,z) =
Seg (len (mlt y2,z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
.=
Seg (len ((mlt x2,z2) - (mlt y2,z2)))
by FINSEQ_1:def 18
.=
dom ((mlt x2,z2) - (mlt y2,z2))
by FINSEQ_1:def 3
;
for i being Nat st i in dom (mlt (x - y),z) holds
(mlt (x - y),z) . i = ((mlt x,z) - (mlt y,z)) . i
proof
let i be
Nat;
:: thesis: ( i in dom (mlt (x - y),z) implies (mlt (x - y),z) . i = ((mlt x,z) - (mlt y,z)) . i )
assume A4:
i in dom (mlt (x - y),z)
;
:: thesis: (mlt (x - y),z) . i = ((mlt x,z) - (mlt y,z)) . i
len (x2 - y2) = len x
by FINSEQ_1:def 18;
then A5:
dom (x2 - y2) =
Seg (len x)
by FINSEQ_1:def 3
.=
Seg (len (mlt x2,z2))
by FINSEQ_1:def 18
.=
dom (mlt x,z)
by FINSEQ_1:def 3
;
set a =
x . i;
set b =
y . i;
set d =
(x - y) . i;
set e =
z . i;
A6:
(x - y) . i = (x . i) - (y . i)
by A1, A2, A4, A5, COMPLSP2:2;
thus (mlt (x - y),z) . i =
((x - y) . i) * (z . i)
by A4, Th19
.=
((x . i) * (z . i)) - ((y . i) * (z . i))
by A6
.=
((mlt x,z) . i) - ((y . i) * (z . i))
by A1, A2, A4, Th19
.=
((mlt x,z) . i) - ((mlt y,z) . i)
by A1, A3, A4, Th19
.=
((mlt x,z) - (mlt y,z)) . i
by A1, A4, COMPLSP2:2
;
:: thesis: verum
end;
hence
mlt (x - y),z = (mlt x,z) - (mlt y,z)
by A1, FINSEQ_1:17; :: thesis: verum