let c, m, n be Nat; :: thesis: for D being non empty set
for pD being FinSequence of D
for A being Matrix of n,m,D
for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
let D be non empty set ; :: thesis: for pD being FinSequence of D
for A being Matrix of n,m,D
for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
let pD be FinSequence of D; :: thesis: for A being Matrix of n,m,D
for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
let A be Matrix of n,m,D; :: thesis: for A9 being Matrix of m,n,D st A9 = A @ & ( m = 0 implies n = 0 ) holds
ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
let A9 be Matrix of m,n,D; :: thesis: ( A9 = A @ & ( m = 0 implies n = 0 ) implies ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ )
assume that
A1: A9 = A @ and
A2: ( m = 0 implies n = 0 ) ; :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
set RC = ReplaceCol (A,c,pD);
set RL = ReplaceLine (A9,c,pD);
now :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
per cases ( n = 0 or ( len pD <> len A & n > 0 ) or ( len pD = len A & n > 0 ) ) ;
suppose A5: ( len pD <> len A & n > 0 ) ; :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
then A6: width A = m by MATRIX_0:23;
then A7: width A9 = len A by A1, A2, A5, MATRIX_0:54;
A8: len A = n by A5, MATRIX_0:23;
thus ReplaceCol (A,c,pD) = A by A5, Def2
.= (A @) @ by A2, A5, A8, A6, MATRIX_0:57
.= (ReplaceLine (A9,c,pD)) @ by A1, A5, A7, MATRIX11:def 3 ; :: thesis: verum
end;
suppose A9: ( len pD = len A & n > 0 ) ; :: thesis: ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @
then A10: width (ReplaceLine (A9,c,pD)) = n by A2, MATRIX_0:23;
then A11: len ((ReplaceLine (A9,c,pD)) @) = n by A9, MATRIX_0:54;
len (ReplaceLine (A9,c,pD)) = m by A2, A9, MATRIX_0:23;
then width ((ReplaceLine (A9,c,pD)) @) = m by A9, A10, MATRIX_0:54;
then reconsider RL9 = (ReplaceLine (A9,c,pD)) @ as Matrix of n,m,D by A11, MATRIX_0:51;
A12: len A = n by A9, MATRIX_0:23;
A13: width A9 = n by A2, A9, MATRIX_0:23;
now :: thesis: for i, j being Nat st [i,j] in Indices (ReplaceCol (A,c,pD)) holds
(ReplaceCol (A,c,pD)) * (i,j) = RL9 * (i,j)
A14: Indices (ReplaceCol (A,c,pD)) = Indices A by MATRIX_0:26;
A15: Indices (ReplaceLine (A9,c,pD)) = Indices A9 by MATRIX_0:26;
let i, j be Nat; :: thesis: ( [i,j] in Indices (ReplaceCol (A,c,pD)) implies (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2) )
assume A16: [i,j] in Indices (ReplaceCol (A,c,pD)) ; :: thesis: (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2)
reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;
Indices (ReplaceCol (A,c,pD)) = Indices RL9 by MATRIX_0:26;
then A17: [j,i] in Indices (ReplaceLine (A9,c,pD)) by A16, MATRIX_0:def 6;
per cases ( J = c or J <> c ) ;
suppose A18: J = c ; :: thesis: (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2)
hence (ReplaceCol (A,c,pD)) * (i,j) = pD . I by A9, A16, A14, Def2
.= (ReplaceLine (A9,c,pD)) * (J,I) by A9, A12, A13, A17, A15, A18, MATRIX11:def 3
.= RL9 * (i,j) by A17, MATRIX_0:def 6 ;
:: thesis: verum
end;
suppose A19: J <> c ; :: thesis: (ReplaceCol (A,c,pD)) * (b1,b2) = RL9 * (b1,b2)
hence (ReplaceCol (A,c,pD)) * (i,j) = A * (I,J) by A9, A16, A14, Def2
.= A9 * (j,i) by A1, A16, A14, MATRIX_0:def 6
.= (ReplaceLine (A9,c,pD)) * (J,I) by A9, A12, A13, A17, A15, A19, MATRIX11:def 3
.= RL9 * (i,j) by A17, MATRIX_0:def 6 ;
:: thesis: verum
end;
end;
end;
hence ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ by MATRIX_0:27; :: thesis: verum
end;
end;
end;
hence ReplaceCol (A,c,pD) = (ReplaceLine (A9,c,pD)) @ ; :: thesis: verum