let K be Ring; for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y))
let x, y, z be FinSequence of K; ( len x = len y & len y = len z implies mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) )
assume that
A1:
len x = len y
and
A2:
len y = len z
; mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y))
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:92;
A4: dom (x + y) =
Seg (len (x2 + y2))
by FINSEQ_1:def 3
.=
dom z
by A1, A2, CARD_1:def 7, FINSEQ_1:def 3
;
A5: dom (mlt (z,y)) =
Seg (len (mlt (z2,y2)))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
;
then A6: dom (mlt (z,y)) =
Seg (len ((mlt (z2,x2)) + (mlt (z2,y2))))
by CARD_1:def 7
.=
dom ((mlt (z2,x2)) + (mlt (z2,y2)))
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 (z,x)) =
Seg (len (mlt (z2,x2)))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
;
then A10: dom (mlt (z,x)) =
Seg (len ((mlt (z2,x2)) + (mlt (z2,y2))))
by CARD_1:def 7
.=
dom ((mlt (z2,x2)) + (mlt (z2,y2)))
by FINSEQ_1:def 3
;
A11:
for i being Nat st i in dom (mlt (z,(x + y))) holds
(mlt (z,(x + y))) . i = ((mlt (z,x)) + (mlt (z,y))) . i
proof
let i be
Nat;
( i in dom (mlt (z,(x + y))) implies (mlt (z,(x + y))) . i = ((mlt (z,x)) + (mlt (z,y))) . 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 (
z,
(x + y))
= the
multF of
K .: (
z,
(x + y)) &
[:(rng z),(rng (x + y)):] c= dom the
multF of
K )
by A13, FVSUM_1:def 7, ZFMISC_1:96;
then A14:
dom (mlt (z,(x + y))) = (dom z) /\ (dom (x + y))
by FUNCOP_1:69;
assume A15:
i in dom (mlt (z,(x + y)))
;
(mlt (z,(x + y))) . i = ((mlt (z,x)) + (mlt (z,y))) . i
then
i in dom z
by A14, XBOOLE_0:def 4;
then A16:
z . i in rng z
by FUNCT_1:def 3;
len (x2 + y2) = len x
by CARD_1:def 7;
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 3;
i in dom y
by A1, A18, FINSEQ_1:def 3;
then A20:
y . i in rng y
by FUNCT_1:def 3;
A21:
i in dom x
by A18, FINSEQ_1:def 3;
then
x . i in rng x
by FUNCT_1:def 3;
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 <:z,y:> =
(dom x) /\ (dom x)
by A8, A3, A7, FUNCT_3:def 7
.=
dom x
;
then A22:
i in dom <:z,y:>
by A18, FINSEQ_1:def 3;
dom [:z,y:] = [:(dom z),(dom y):]
by FUNCT_3:def 8;
then A23:
[i,i] in dom [:z,y:]
by A8, A3, A15, A17, A14, ZFMISC_1:87;
dom [:z,y:] = [:(dom z),(dom y):]
by FUNCT_3:def 8;
then A24:
[i,i] in dom [:z,y:]
by A8, A3, A15, A17, A14, ZFMISC_1:87;
dom the
multF of
K = [: the carrier of K, the carrier of K:]
by FUNCT_2:def 1;
then
[e,b] in dom the
multF of
K
by ZFMISC_1:87;
then
(
dom ( the multF of K * (z,y)) = dom ( the multF of K * [:z,y:]) &
[:z,y:] . (
i,
i)
in dom the
multF of
K )
by A8, A3, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;
then
[i,i] in dom ( the multF of K * (z,y))
by A24, FUNCT_1:11;
then A25:
e * b =
( the multF of K * (z,y)) . (
i,
i)
by FINSEQOP:77
.=
( the multF of K * [:z,y:]) . (
i,
i)
by FINSEQOP:def 4
.=
the
multF of
K . ([:z,y:] . (i,i))
by A23, FUNCT_1:13
.=
the
multF of
K . (
(z . i),
(y . i))
by A8, A3, A15, A17, A14, FUNCT_3:def 8
.=
the
multF of
K . (<:z,y:> . i)
by A8, A3, A15, A17, A14, FUNCT_3:49
.=
( the multF of K * <:z,y:>) . i
by A22, FUNCT_1:13
.=
( the multF of K .: (z,y)) . i
by FUNCOP_1:def 3
.=
(mlt (z,y)) . i
by FVSUM_1:def 7
;
dom <:z,(x + y):> =
(dom z) /\ (dom (x + y))
by FUNCT_3:def 7
.=
dom x
by A3, A4, FINSEQ_1:def 3
;
then A26:
i in dom <:z,(x + y):>
by A18, FINSEQ_1:def 3;
A27:
(mlt (z,(x + y))) . i =
( the multF of K .: (z,(x + y))) . i
by FVSUM_1:def 7
.=
( the multF of K * <:z,(x + y):>) . i
by FUNCOP_1:def 3
.=
the
multF of
K . (<:z,(x + y):> . i)
by A26, FUNCT_1:13
.=
e * d
by A4, A15, A14, FUNCT_3:49
;
A28:
dom <:(mlt (z,x)),(mlt (z,y)):> =
(dom (mlt (z,x))) /\ (dom (mlt (z,y)))
by FUNCT_3:def 7
.=
dom x
by A9, A5, FINSEQ_1:def 3
;
A29:
dom <:x,y:> =
(dom x) /\ (dom y)
by FUNCT_3:def 7
.=
dom x
by A8, A7
;
A30:
the
addF of
K .: (
(mlt (z,x)),
(mlt (z,y)))
= (mlt (z,x)) + (mlt (z,y))
by FVSUM_1:def 3;
dom [:z,x:] = [:(dom z),(dom x):]
by FUNCT_3:def 8;
then A31:
[i,i] in dom [:z,x:]
by A3, A7, A15, A17, A14, ZFMISC_1:87;
dom [:z,x:] = [:(dom z),(dom x):]
by FUNCT_3:def 8;
then A32:
[i,i] in dom [:z,x:]
by A3, A7, A15, A17, A14, ZFMISC_1:87;
dom <:z,x:> =
(dom x) /\ (dom x)
by A3, A7, FUNCT_3:def 7
.=
dom x
;
then A33:
i in dom <:z,x:>
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:13
.=
a + b
by A8, A7, A18, FUNCT_3:49
;
dom the
multF of
K = [: the carrier of K, the carrier of K:]
by FUNCT_2:def 1;
then
[e,a] in dom the
multF of
K
by ZFMISC_1:87;
then
(
dom ( the multF of K * (z,x)) = dom ( the multF of K * [:z,x:]) &
[:z,x:] . (
i,
i)
in dom the
multF of
K )
by A3, A7, A15, A17, A14, FINSEQOP:def 4, FUNCT_3:def 8;
then
[i,i] in dom ( the multF of K * (z,x))
by A32, FUNCT_1:11;
then e * a =
( the multF of K * (z,x)) . (
i,
i)
by FINSEQOP:77
.=
( the multF of K * [:z,x:]) . (
i,
i)
by FINSEQOP:def 4
.=
the
multF of
K . ([:z,x:] . (i,i))
by A31, FUNCT_1:13
.=
the
multF of
K . (
(z . i),
(x . i))
by A3, A7, A15, A17, A14, FUNCT_3:def 8
.=
the
multF of
K . (<:z,x:> . i)
by A3, A7, A15, A17, A14, FUNCT_3:49
.=
( the multF of K * <:z,x:>) . i
by A33, FUNCT_1:13
.=
( the multF of K .: (z,x)) . i
by FUNCOP_1:def 3
.=
(mlt (z,x)) . i
by FVSUM_1:def 7
;
then (e * a) + (e * b) =
the
addF of
K . (<:(mlt (z,x)),(mlt (z,y)):> . i)
by A9, A10, A6, A18, A25, FUNCT_3:49
.=
( the addF of K * <:(mlt (z,x)),(mlt (z,y)):>) . i
by A21, A28, FUNCT_1:13
.=
((mlt (z,x)) + (mlt (z,y))) . i
by A30, FUNCOP_1:def 3
;
hence
(mlt (z,(x + y))) . i = ((mlt (z,x)) + (mlt (z,y))) . i
by A34, A27, VECTSP_1:def 7;
verum
end;
dom (mlt (z,(x + y))) =
Seg (len (mlt (z2,(x2 + y2))))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
.=
Seg (len ((mlt (z2,x2)) + (mlt (z2,y2))))
by CARD_1:def 7
.=
dom ((mlt (z2,x2)) + (mlt (z2,y2)))
by FINSEQ_1:def 3
;
hence
mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y))
by A11, FINSEQ_1:13; verum