let K be Ring; 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: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 (y,z)) =
Seg (len (mlt (y2,z2)))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
;
then A6: dom (mlt (y,z)) =
Seg (len ((mlt (x2,z2)) + (mlt (y2,z2))))
by CARD_1:def 7
.=
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 CARD_1:def 7
;
then A10: dom (mlt (x,z)) =
Seg (len ((mlt (x2,z2)) + (mlt (y2,z2))))
by CARD_1:def 7
.=
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:96;
then A14:
dom (mlt ((x + y),z)) = (dom (x + y)) /\ (dom z)
by FUNCOP_1:69;
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 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 <:y,z:> =
(dom x) /\ (dom x)
by A8, A3, A7, FUNCT_3:def 7
.=
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 8;
then A23:
[i,i] in dom [:y,z:]
by A8, A3, A15, A17, A14, ZFMISC_1:87;
dom [:y,z:] = [:(dom y),(dom z):]
by FUNCT_3:def 8;
then A24:
[i,i] in dom [:y,z:]
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
[b,e] in dom the
multF of
K
by ZFMISC_1:87;
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 8;
then
[i,i] in dom ( the multF of K * (y,z))
by A24, FUNCT_1:11;
then A25:
b * e =
( the multF of K * (y,z)) . (
i,
i)
by FINSEQOP:77
.=
( the multF of K * [:y,z:]) . (
i,
i)
by FINSEQOP:def 4
.=
the
multF of
K . ([:y,z:] . (i,i))
by A23, FUNCT_1:13
.=
the
multF of
K . (
(y . i),
(z . i))
by A8, A3, A15, A17, A14, FUNCT_3:def 8
.=
the
multF of
K . (<:y,z:> . i)
by A8, A3, A15, A17, A14, FUNCT_3:49
.=
( the multF of K * <:y,z:>) . i
by A22, FUNCT_1:13
.=
( 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 7
.=
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:13
.=
d * e
by A4, A15, A14, FUNCT_3:49
;
A28:
dom <:(mlt (x,z)),(mlt (y,z)):> =
(dom (mlt (x,z))) /\ (dom (mlt (y,z)))
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 (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 8;
then A31:
[i,i] in dom [:x,z:]
by A3, A7, A15, A17, A14, ZFMISC_1:87;
dom [:x,z:] = [:(dom x),(dom z):]
by FUNCT_3:def 8;
then A32:
[i,i] in dom [:x,z:]
by A3, A7, A15, A17, A14, ZFMISC_1:87;
dom <:x,z:> =
(dom x) /\ (dom x)
by A3, A7, FUNCT_3:def 7
.=
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: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
[a,e] in dom the
multF of
K
by ZFMISC_1:87;
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 8;
then
[i,i] in dom ( the multF of K * (x,z))
by A32, FUNCT_1:11;
then a * e =
( the multF of K * (x,z)) . (
i,
i)
by FINSEQOP:77
.=
( the multF of K * [:x,z:]) . (
i,
i)
by FINSEQOP:def 4
.=
the
multF of
K . ([:x,z:] . (i,i))
by A31, FUNCT_1:13
.=
the
multF of
K . (
(x . i),
(z . i))
by A3, A7, A15, A17, A14, FUNCT_3:def 8
.=
the
multF of
K . (<:x,z:> . i)
by A3, A7, A15, A17, A14, FUNCT_3:49
.=
( the multF of K * <:x,z:>) . i
by A33, FUNCT_1:13
.=
( 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:49
.=
( the addF of K * <:(mlt (x,z)),(mlt (y,z)):>) . i
by A21, A28, FUNCT_1:13
.=
((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 7;
verum
end;
dom (mlt ((x + y),z)) =
Seg (len (mlt ((x2 + y2),z2)))
by FINSEQ_1:def 3
.=
Seg (len x)
by CARD_1:def 7
.=
Seg (len ((mlt (x2,z2)) + (mlt (y2,z2))))
by CARD_1:def 7
.=
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:13; verum