let R be Ring; :: thesis: for I, K, L being Nat st ( I = 0 implies K = 0 ) holds
for i, k, l being Nat st k in Seg K holds
(canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
let I, K, L be Nat; :: thesis: ( ( I = 0 implies K = 0 ) implies for i, k, l being Nat st k in Seg K holds
(canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) )
assume A1: ( I = 0 implies K = 0 ) ; :: thesis: for i, k, l being Nat st k in Seg K holds
(canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
let i, k, l be Nat; :: thesis: ( k in Seg K implies (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) )
assume A2: k in Seg K ; :: thesis: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
set LHS = (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R));
set RHS = canMat (i,l,I,L,R);
per cases ( I = 0 or ( I <> 0 & K = 0 ) or ( I <> 0 & K <> 0 ) ) ;
suppose I = 0 ; :: thesis: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
hence (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) by A1, A2; :: thesis: verum
end;
suppose ( I <> 0 & K = 0 ) ; :: thesis: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
hence (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) by A2; :: thesis: verum
end;
suppose A3: ( I <> 0 & K <> 0 ) ; :: thesis: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
per cases ( ( i in Seg I & l in Seg L ) or not i in Seg I or not l in Seg L ) ;
suppose ( i in Seg I & l in Seg L ) ; :: thesis: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
hence (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R) by A2, Th47; :: thesis: verum
end;
suppose A4: not i in Seg I ; :: thesis: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
A5: ( width (0. (R,I,K)) = K & width (canMat (k,l,K,L,R)) = L & len (canMat (k,l,K,L,R)) = K ) by A3, MATRIX_0:23;
dom (canMat (i,k,I,K,R)) = Seg (len (canMat (i,k,I,K,R))) by FINSEQ_1:def 3
.= Seg I by MATRIX_0:25 ;
then not [i,k] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A4, ZFMISC_1:87;
then not [i,k] in Indices (canMat (i,k,I,K,R)) by MATRIX_0:def 4;
then canMat (i,k,I,K,R) = 0. (R,I,K) by Th41;
then A6: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = 0. (R,I,L) by A5, Th17;
dom (canMat (i,l,I,L,R)) = Seg (len (canMat (i,l,I,L,R))) by FINSEQ_1:def 3
.= Seg I by MATRIX_0:25 ;
then not [i,l] in [:(dom (canMat (i,l,I,L,R))),(Seg (width (canMat (i,l,I,L,R)))):] by A4, ZFMISC_1:87;
then not [i,l] in Indices (canMat (i,l,I,L,R)) by MATRIX_0:def 4;
hence canMat (i,l,I,L,R) = (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) by A6, Th41; :: thesis: verum
end;
suppose A7: not l in Seg L ; :: thesis: (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)
A8: not [k,l] in Indices (canMat (k,l,K,L,R))
proof
set X = canMat (k,l,K,L,R);
not l in Seg (width (canMat (k,l,K,L,R))) by A3, A7, Th43;
then not [k,l] in [:(dom (canMat (k,l,K,L,R))),(Seg (width (canMat (k,l,K,L,R)))):] by ZFMISC_1:87;
hence not [k,l] in Indices (canMat (k,l,K,L,R)) by MATRIX_0:def 4; :: thesis: verum
end;
A9: not [i,l] in Indices (canMat (i,l,I,L,R))
proof
set X = canMat (i,l,I,L,R);
not l in Seg (width (canMat (i,l,I,L,R))) by A3, A7, Th43;
then not [i,l] in [:(dom (canMat (i,l,I,L,R))),(Seg (width (canMat (i,l,I,L,R)))):] by ZFMISC_1:87;
hence not [i,l] in Indices (canMat (i,l,I,L,R)) by MATRIX_0:def 4; :: thesis: verum
end;
set A = canMat (i,k,I,K,R);
A10: ( L = width (canMat (k,l,K,L,R)) & I = len (canMat (i,k,I,K,R)) & K = width (canMat (i,k,I,K,R)) ) by A3, Th43;
A11: canMat (k,l,K,L,R) = 0. (R,(width (canMat (i,k,I,K,R))),L) by A10, A8, Th41;
thus canMat (i,l,I,L,R) = 0. (R,(len (canMat (i,k,I,K,R))),L) by A10, A9, Th41
.= (canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) by A10, A11, Th18 ; :: thesis: verum
end;
end;
end;
end;