let c, m, n be Nat; for D being non empty set
for AD being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col ((RCol (AD,c,pD)),i) = pD ) & ( i <> c implies Col ((RCol (AD,c,pD)),i) = Col (AD,i) ) )
let D be non empty set ; for AD being Matrix of n,m,D
for pD being FinSequence of D
for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col ((RCol (AD,c,pD)),i) = pD ) & ( i <> c implies Col ((RCol (AD,c,pD)),i) = Col (AD,i) ) )
let AD be Matrix of n,m,D; for pD being FinSequence of D
for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col ((RCol (AD,c,pD)),i) = pD ) & ( i <> c implies Col ((RCol (AD,c,pD)),i) = Col (AD,i) ) )
let pD be FinSequence of D; for i being Nat st i in Seg (width AD) holds
( ( i = c & len pD = len AD implies Col ((RCol (AD,c,pD)),i) = pD ) & ( i <> c implies Col ((RCol (AD,c,pD)),i) = Col (AD,i) ) )
let i be Nat; ( i in Seg (width AD) implies ( ( i = c & len pD = len AD implies Col ((RCol (AD,c,pD)),i) = pD ) & ( i <> c implies Col ((RCol (AD,c,pD)),i) = Col (AD,i) ) ) )
assume A1:
i in Seg (width AD)
; ( ( i = c & len pD = len AD implies Col ((RCol (AD,c,pD)),i) = pD ) & ( i <> c implies Col ((RCol (AD,c,pD)),i) = Col (AD,i) ) )
set R = RCol (AD,c,pD);
set CR = Col ((RCol (AD,c,pD)),i);
thus
( i = c & len pD = len AD implies Col ((RCol (AD,c,pD)),i) = pD )
( i <> c implies Col ((RCol (AD,c,pD)),i) = Col (AD,i) )proof
assume that A2:
i = c
and A3:
len pD = len AD
;
Col ((RCol (AD,c,pD)),i) = pD
A4:
len (RCol (AD,c,pD)) = len pD
by A3, Def2;
A5:
now for J being Nat st 1 <= J & J <= len pD holds
(Col ((RCol (AD,c,pD)),i)) . J = pD . Jlet J be
Nat;
( 1 <= J & J <= len pD implies (Col ((RCol (AD,c,pD)),i)) . J = pD . J )assume that A6:
1
<= J
and A7:
J <= len pD
;
(Col ((RCol (AD,c,pD)),i)) . J = pD . J
J in Seg (len pD)
by A6, A7;
then A8:
J in dom (RCol (AD,c,pD))
by A4, FINSEQ_1:def 3;
i in Seg (width (RCol (AD,c,pD)))
by A1, A3, Def2;
then A9:
[J,c] in Indices (RCol (AD,c,pD))
by A2, A8, ZFMISC_1:87;
A10:
Indices (RCol (AD,c,pD)) = Indices AD
by MATRIX_0:26;
(Col ((RCol (AD,c,pD)),i)) . J = (RCol (AD,c,pD)) * (
J,
c)
by A2, A8, MATRIX_0:def 8;
hence
(Col ((RCol (AD,c,pD)),i)) . J = pD . J
by A3, A9, A10, Def2;
verum end;
len (Col ((RCol (AD,c,pD)),i)) = len pD
by A4, MATRIX_0:def 8;
hence
Col (
(RCol (AD,c,pD)),
i)
= pD
by A5;
verum
end;
set CA = Col (AD,i);
A11:
len AD = n
by MATRIX_0:def 2;
A12:
len (RCol (AD,c,pD)) = n
by MATRIX_0:def 2;
A13:
len AD = len (Col (AD,i))
by MATRIX_0:def 8;
assume A14:
i <> c
; Col ((RCol (AD,c,pD)),i) = Col (AD,i)
A15:
now for j being Nat st 1 <= j & j <= len (Col (AD,i)) holds
(Col (AD,i)) . j = (Col ((RCol (AD,c,pD)),i)) . jlet j be
Nat;
( 1 <= j & j <= len (Col (AD,i)) implies (Col (AD,i)) . b1 = (Col ((RCol (AD,c,pD)),i)) . b1 )assume that A16:
1
<= j
and A17:
j <= len (Col (AD,i))
;
(Col (AD,i)) . b1 = (Col ((RCol (AD,c,pD)),i)) . b1A18:
j in Seg (len AD)
by A13, A16, A17;
then A19:
j in dom AD
by FINSEQ_1:def 3;
then A20:
(Col (AD,i)) . j = AD * (
j,
i)
by MATRIX_0:def 8;
j in dom (RCol (AD,c,pD))
by A11, A12, A18, FINSEQ_1:def 3;
then A21:
(Col ((RCol (AD,c,pD)),i)) . j = (RCol (AD,c,pD)) * (
j,
i)
by MATRIX_0:def 8;
A22:
[j,i] in Indices AD
by A1, A19, ZFMISC_1:87;
end;
len (Col ((RCol (AD,c,pD)),i)) = len (RCol (AD,c,pD))
by MATRIX_0:def 8;
hence
Col ((RCol (AD,c,pD)),i) = Col (AD,i)
by A11, A12, A13, A15; verum