let k, m, n be Nat; for D being non empty set
for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
for i being Nat st i in Seg (width M1) holds
Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))
let D be non empty set ; for M1 being Matrix of n,k,D
for M2 being Matrix of m,k,D st width M1 = width M2 holds
for i being Nat st i in Seg (width M1) holds
Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))
let M1 be Matrix of n,k,D; for M2 being Matrix of m,k,D st width M1 = width M2 holds
for i being Nat st i in Seg (width M1) holds
Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))
let M2 be Matrix of m,k,D; ( width M1 = width M2 implies for i being Nat st i in Seg (width M1) holds
Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) )
assume A1:
width M1 = width M2
; for i being Nat st i in Seg (width M1) holds
Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))
let i be Nat; ( i in Seg (width M1) implies Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i)) )
assume A2:
i in Seg (width M1)
; Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))
A3:
dom (Col ((M1 ^ M2),i)) = Seg (len (Col ((M1 ^ M2),i)))
by FINSEQ_1:def 3;
A4: len (Col ((M1 ^ M2),i)) =
len (M1 ^ M2)
by MATRIX_0:def 8
.=
(len M1) + (len M2)
by FINSEQ_1:22
.=
(len M1) + (len (Col (M2,i)))
by MATRIX_0:def 8
.=
(len (Col (M1,i))) + (len (Col (M2,i)))
by MATRIX_0:def 8
.=
len ((Col (M1,i)) ^ (Col (M2,i)))
by FINSEQ_1:22
;
now for j being Nat st j in dom (Col ((M1 ^ M2),i)) holds
(Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . jlet j be
Nat;
( j in dom (Col ((M1 ^ M2),i)) implies (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j )assume A5:
j in dom (Col ((M1 ^ M2),i))
;
(Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . jthen
j in Seg (len (M1 ^ M2))
by A3, MATRIX_0:def 8;
then A6:
j in dom (M1 ^ M2)
by FINSEQ_1:def 3;
i in Seg (width (M1 ^ M2))
by A1, A2, Th24;
then
[j,i] in [:(dom (M1 ^ M2)),(Seg (width (M1 ^ M2))):]
by A6, ZFMISC_1:87;
then
[j,i] in Indices (M1 ^ M2)
by MATRIX_0:def 4;
then consider P being
FinSequence of
D such that A7:
P = (M1 ^ M2) . j
and A8:
(M1 ^ M2) * (
j,
i)
= P . i
by MATRIX_0:def 5;
A9:
j in dom ((Col (M1,i)) ^ (Col (M2,i)))
by A4, A3, A5, FINSEQ_1:def 3;
now (Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . jper cases
( j in dom (Col (M1,i)) or ex n being Nat st
( n in dom (Col (M2,i)) & j = (len (Col (M1,i))) + n ) )
by A9, FINSEQ_1:25;
suppose A10:
j in dom (Col (M1,i))
;
(Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . jthen
j in Seg (len (Col (M1,i)))
by FINSEQ_1:def 3;
then
j in Seg (len M1)
by MATRIX_0:def 8;
then A11:
j in dom M1
by FINSEQ_1:def 3;
then
[j,i] in [:(dom M1),(Seg (width M1)):]
by A2, ZFMISC_1:87;
then
[j,i] in Indices M1
by MATRIX_0:def 4;
then consider P1 being
FinSequence of
D such that A12:
P1 = M1 . j
and A13:
M1 * (
j,
i)
= P1 . i
by MATRIX_0:def 5;
P = P1
by A7, A11, A12, FINSEQ_1:def 7;
hence (Col ((M1 ^ M2),i)) . j =
M1 * (
j,
i)
by A6, A8, A13, MATRIX_0:def 8
.=
(Col (M1,i)) . j
by A11, MATRIX_0:def 8
.=
((Col (M1,i)) ^ (Col (M2,i))) . j
by A10, FINSEQ_1:def 7
;
verum end; suppose
ex
n being
Nat st
(
n in dom (Col (M2,i)) &
j = (len (Col (M1,i))) + n )
;
(Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . jthen consider n being
Nat such that A14:
n in dom (Col (M2,i))
and A15:
j = (len (Col (M1,i))) + n
;
n in Seg (len (Col (M2,i)))
by A14, FINSEQ_1:def 3;
then
n in Seg (len M2)
by MATRIX_0:def 8;
then A16:
n in dom M2
by FINSEQ_1:def 3;
then
[n,i] in [:(dom M2),(Seg (width M2)):]
by A1, A2, ZFMISC_1:87;
then
[n,i] in Indices M2
by MATRIX_0:def 4;
then consider P2 being
FinSequence of
D such that A17:
P2 = M2 . n
and A18:
M2 * (
n,
i)
= P2 . i
by MATRIX_0:def 5;
len (Col (M2,i)) = len M2
by MATRIX_0:def 8;
then
(
len (Col (M1,i)) = len M1 &
dom (Col (M2,i)) = dom M2 )
by FINSEQ_3:29, MATRIX_0:def 8;
then
P = P2
by A7, A14, A15, A17, FINSEQ_1:def 7;
hence (Col ((M1 ^ M2),i)) . j =
M2 * (
n,
i)
by A6, A8, A18, MATRIX_0:def 8
.=
(Col (M2,i)) . n
by A16, MATRIX_0:def 8
.=
((Col (M1,i)) ^ (Col (M2,i))) . j
by A14, A15, FINSEQ_1:def 7
;
verum end; end; end; hence
(Col ((M1 ^ M2),i)) . j = ((Col (M1,i)) ^ (Col (M2,i))) . j
;
verum end;
hence
Col ((M1 ^ M2),i) = (Col (M1,i)) ^ (Col (M2,i))
by A4, FINSEQ_2:9; verum