let n be Nat; :: thesis: for K being Field
for a being Element of K
for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col M,i) . k = a * ((Col N,i) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col M,l = Col N,l ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix p,M) /. l = a * ((Path_matrix p,N) /. l) )
let K be Field; :: thesis: for a being Element of K
for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col M,i) . k = a * ((Col N,i) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col M,l = Col N,l ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix p,M) /. l = a * ((Path_matrix p,N) /. l) )
let a be Element of K; :: thesis: for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col M,i) . k = a * ((Col N,i) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col M,l = Col N,l ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix p,M) /. l = a * ((Path_matrix p,N) /. l) )
let M, N be Matrix of n,K; :: thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col M,i) . k = a * ((Col N,i) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col M,l = Col N,l ) ) implies for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix p,M) /. l = a * ((Path_matrix p,N) /. l) ) )
assume ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col M,i) . k = a * ((Col N,i) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col M,l = Col N,l ) ) ; :: thesis: for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix p,M) /. l = a * ((Path_matrix p,N) /. l) )
then consider i being Element of NAT such that
A1: i in Seg n and
A2: for k being Element of NAT st k in Seg n holds
(Col M,i) . k = a * ((Col N,i) /. k) and
for l being Element of NAT st l <> i & l in Seg n holds
Col M,l = Col N,l ;
let p be Element of Permutations n; :: thesis: ex l being Element of NAT st
( l in Seg n & (Path_matrix p,M) /. l = a * ((Path_matrix p,N) /. l) )
n in NAT by ORDINAL1:def 13;
then consider k being Element of NAT such that
A3: k in Seg n and
A4: i = p . k by A1, Th48;
A5: 1 <= k by A3, FINSEQ_1:3;
len (Path_matrix p,N) = n by MATRIX_3:def 7;
then A6: k in dom (Path_matrix p,N) by A3, FINSEQ_1:def 3;
then (Path_matrix p,N) . k = N * k,i by A4, MATRIX_3:def 7;
then A7: (Path_matrix p,N) /. k = N * k,i by A6, PARTFUN1:def 8;
len (Col N,i) = len N by MATRIX_1:def 9;
then A8: dom (Col N,i) = dom N by FINSEQ_3:31;
len N = n by MATRIX_1:def 3;
then k <= len N by A3, FINSEQ_1:3;
then A9: k in dom N by A5, FINSEQ_3:27;
then (Col N,i) . k = N * k,i by MATRIX_1:def 9;
then A10: (Col N,i) /. k = (Path_matrix p,N) /. k by A9, A7, A8, PARTFUN1:def 8;
len M = n by MATRIX_1:def 3;
then k <= len M by A3, FINSEQ_1:3;
then A11: k in dom M by A5, FINSEQ_3:27;
take k ; :: thesis: ( k in Seg n & (Path_matrix p,M) /. k = a * ((Path_matrix p,N) /. k) )
len (Path_matrix p,M) = n by MATRIX_3:def 7;
then A12: dom (Path_matrix p,M) = Seg n by FINSEQ_1:def 3;
then (Path_matrix p,M) . k = M * k,i by A3, A4, MATRIX_3:def 7;
then (Path_matrix p,M) . k = (Col M,i) . k by A11, MATRIX_1:def 9
.= a * ((Path_matrix p,N) /. k) by A2, A3, A10 ;
hence ( k in Seg n & (Path_matrix p,M) /. k = a * ((Path_matrix p,N) /. k) ) by A12, A3, PARTFUN1:def 8; :: thesis: verum