let K be Field; for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt (x + y),z = (mlt x,z) + (mlt y,z)
let x, y, z be FinSequence of K; ( len x = len y & len y = len z implies mlt (x + y),z = (mlt x,z) + (mlt y,z) )
assume that
A1:
len x = len y
and
A2:
len y = len z
; mlt (x + y),z = (mlt x,z) + (mlt y,z)
A3:
dom z = Seg (len x)
by A1, A2, FINSEQ_1:def 3;
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on the carrier of K by A1, A2, FINSEQ_2:110;
A4: dom (x + y) =
Seg (len (x2 + y2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
.=
dom z
by A1, A2, FINSEQ_1:def 3
;
A5: dom (mlt y,z) =
Seg (len (mlt y2,z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
;
then A6: dom (mlt y,z) =
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
;
A7:
dom x = Seg (len x)
by FINSEQ_1:def 3;
A8:
dom y = Seg (len x)
by A1, FINSEQ_1:def 3;
A9: dom (mlt x,z) =
Seg (len (mlt x2,z2))
by FINSEQ_1:def 3
.=
Seg (len x)
by FINSEQ_1:def 18
;
then A10: dom (mlt x,z) =
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
;
A11:
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;
( i in dom (mlt (x + y),z) implies (mlt (x + y),z) . i = ((mlt x,z) + (mlt y,z)) . i )
A12:
(
rng x c= the
carrier of
K &
rng y c= the
carrier of
K )
by FINSEQ_1:def 4;
A13:
(
rng z c= the
carrier of
K &
rng (x + y) c= the
carrier of
K )
by FINSEQ_1:def 4;
dom the
multF of
K = [:the carrier of K,the carrier of K:]
by FUNCT_2:def 1;
then
(
mlt (x + y),
z = the
multF of
K .: (x + y),
z &
[:(rng (x + y)),(rng z):] c= dom the
multF of
K )
by A13, FVSUM_1:def 7, ZFMISC_1:119;
then A14:
dom (mlt (x + y),z) = (dom (x + y)) /\ (dom z)
by FUNCOP_1:84;
assume A15:
i in dom (mlt (x + y),z)
;
(mlt (x + y),z) . i = ((mlt x,z) + (mlt y,z)) . i
then
i in dom z
by A14, XBOOLE_0:def 4;
then A16:
z . i in rng z
by FUNCT_1:def 5;
len (x2 + y2) = len x
by FINSEQ_1:def 18;
then A17:
dom (x2 + y2) = Seg (len x)
by FINSEQ_1:def 3;
then A18:
i in Seg (len x)
by A15, A14, XBOOLE_0:def 4;
then A19:
(x + y) . i in rng (x + y)
by A17, FUNCT_1:def 5;
i in dom y
by A1, A18, FINSEQ_1:def 3;
then A20:
y . i in rng y
by FUNCT_1:def 5;
A21:
i in dom x
by A18, FINSEQ_1:def 3;
then
x . i in rng x
by FUNCT_1:def 5;
then reconsider a =
x . i,
b =
y . i,
d =
(x + y) . i,
e =
z . i as
Element of
K by A12, A13, A20, A16, A19;
dom <:y,z:> =
(dom x) /\ (dom x)
by A8, A3, A7, FUNCT_3:def 8
.=
dom x
;
then A22:
i in dom <:y,z:>
by A18, FINSEQ_1:def 3;
dom [:y,z:] = [:(dom y),(dom z):]
by FUNCT_3:def 9;
then A23:
[i,i] in dom [:y,z:]
by A8, A3, A15, A17, A14, ZFMISC_1:106;
dom [:y,z:] = [:(dom y),(dom z):]
by FUNCT_3:def 9;
then A24:
[i,i] in dom [:y,z:]
by A8, A3, A15, A17, A14, ZFMISC_1:106;
dom the
multF of
K = [:the carrier of K,the carrier of K:]
by FUNCT_2:def 1;
then
[b,e] in dom the
multF of
K
by ZFMISC_1:106;
then
(
dom (the multF of K * y,z) = dom (the multF of K * [:y,z:]) &
[:y,z:] . i,
i in dom the
multF of
K )
by A8, A3, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 9;
then
[i,i] in dom (the multF of K * y,z)
by A24, FUNCT_1:21;
then A25:
b * e =
(the multF of K * y,z) . i,
i
by FINSEQOP:82
.=
(the multF of K * [:y,z:]) . i,
i
by FINSEQOP:def 4
.=
the
multF of
K . ([:y,z:] . i,i)
by A23, FUNCT_1:23
.=
the
multF of
K . (y . i),
(z . i)
by A8, A3, A15, A17, A14, FUNCT_3:def 9
.=
the
multF of
K . (<:y,z:> . i)
by A8, A3, A15, A17, A14, FUNCT_3:69
.=
(the multF of K * <:y,z:>) . i
by A22, FUNCT_1:23
.=
(the multF of K .: y,z) . i
by FUNCOP_1:def 3
.=
(mlt y,z) . i
by FVSUM_1:def 7
;
dom <:(x + y),z:> =
(dom (x + y)) /\ (dom z)
by FUNCT_3:def 8
.=
dom x
by A3, A4, FINSEQ_1:def 3
;
then A26:
i in dom <:(x + y),z:>
by A18, FINSEQ_1:def 3;
A27:
(mlt (x + y),z) . i =
(the multF of K .: (x + y),z) . i
by FVSUM_1:def 7
.=
(the multF of K * <:(x + y),z:>) . i
by FUNCOP_1:def 3
.=
the
multF of
K . (<:(x + y),z:> . i)
by A26, FUNCT_1:23
.=
d * e
by A4, A15, A14, FUNCT_3:69
;
A28:
dom <:(mlt x,z),(mlt y,z):> =
(dom (mlt x,z)) /\ (dom (mlt y,z))
by FUNCT_3:def 8
.=
dom x
by A9, A5, FINSEQ_1:def 3
;
A29:
dom <:x,y:> =
(dom x) /\ (dom y)
by FUNCT_3:def 8
.=
dom x
by A8, A7
;
A30:
the
addF of
K .: (mlt x,z),
(mlt y,z) = (mlt x,z) + (mlt y,z)
by FVSUM_1:def 3;
dom [:x,z:] = [:(dom x),(dom z):]
by FUNCT_3:def 9;
then A31:
[i,i] in dom [:x,z:]
by A3, A7, A15, A17, A14, ZFMISC_1:106;
dom [:x,z:] = [:(dom x),(dom z):]
by FUNCT_3:def 9;
then A32:
[i,i] in dom [:x,z:]
by A3, A7, A15, A17, A14, ZFMISC_1:106;
dom <:x,z:> =
(dom x) /\ (dom x)
by A3, A7, FUNCT_3:def 8
.=
dom x
;
then A33:
i in dom <:x,z:>
by A18, FINSEQ_1:def 3;
A34:
(x + y) . i =
(the addF of K .: x,y) . i
by FVSUM_1:def 3
.=
(the addF of K * <:x,y:>) . i
by FUNCOP_1:def 3
.=
the
addF of
K . (<:x,y:> . i)
by A21, A29, FUNCT_1:23
.=
a + b
by A8, A7, A18, FUNCT_3:69
;
dom the
multF of
K = [:the carrier of K,the carrier of K:]
by FUNCT_2:def 1;
then
[a,e] in dom the
multF of
K
by ZFMISC_1:106;
then
(
dom (the multF of K * x,z) = dom (the multF of K * [:x,z:]) &
[:x,z:] . i,
i in dom the
multF of
K )
by A3, A7, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 9;
then
[i,i] in dom (the multF of K * x,z)
by A32, FUNCT_1:21;
then a * e =
(the multF of K * x,z) . i,
i
by FINSEQOP:82
.=
(the multF of K * [:x,z:]) . i,
i
by FINSEQOP:def 4
.=
the
multF of
K . ([:x,z:] . i,i)
by A31, FUNCT_1:23
.=
the
multF of
K . (x . i),
(z . i)
by A3, A7, A15, A17, A14, FUNCT_3:def 9
.=
the
multF of
K . (<:x,z:> . i)
by A3, A7, A15, A17, A14, FUNCT_3:69
.=
(the multF of K * <:x,z:>) . i
by A33, FUNCT_1:23
.=
(the multF of K .: x,z) . i
by FUNCOP_1:def 3
.=
(mlt x,z) . i
by FVSUM_1:def 7
;
then (a * e) + (b * e) =
the
addF of
K . (<:(mlt x,z),(mlt y,z):> . i)
by A9, A10, A6, A18, A25, FUNCT_3:69
.=
(the addF of K * <:(mlt x,z),(mlt y,z):>) . i
by A21, A28, FUNCT_1:23
.=
((mlt x,z) + (mlt y,z)) . i
by A30, FUNCOP_1:def 3
;
hence
(mlt (x + y),z) . i = ((mlt x,z) + (mlt y,z)) . i
by A34, A27, VECTSP_1:def 18;
verum
end;
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
;
hence
mlt (x + y),z = (mlt x,z) + (mlt y,z)
by A11, FINSEQ_1:17; verum