let n be Nat; :: thesis: for K being commutative Ring
for F being Function of (Seg n),(Seg n)
for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like & not F in Permutations n holds
Det (A * F) = 0. K
let K be commutative Ring; :: thesis: for F being Function of (Seg n),(Seg n)
for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like & not F in Permutations n holds
Det (A * F) = 0. K
let F be Function of (Seg n),(Seg n); :: thesis: for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like & not F in Permutations n holds
Det (A * F) = 0. K
let A be Matrix of n,K; :: thesis: ( not K is degenerated & K is well-unital & K is domRing-like & not F in Permutations n implies Det (A * F) = 0. K )
assume A0: ( not K is degenerated & K is well-unital & K is domRing-like ) ; :: thesis: ( F in Permutations n or Det (A * F) = 0. K )
assume not F in Permutations n ; :: thesis: Det (A * F) = 0. K
then A1: ( not F is onto or not F is one-to-one ) by MATRIX_1:def 12;
card (Seg n) = card (Seg n) ;
then not F is one-to-one by A1, FINSEQ_4:63;
then consider x, y being object such that
A2: x in dom F and
A3: y in dom F and
A4: F . x = F . y and
A5: x <> y by FUNCT_1:def 4;
A6: dom F = Seg n by FUNCT_2:52;
then reconsider x = x, y = y as Nat by A2, A3;
Line ((A * F),x) = A . (F . x) by A2, A6, Th38;
then A7: Line ((A * F),x) = Line ((A * F),y) by A3, A4, A6, Th38;
( x > y or y > x ) by A5, XXREAL_0:1;
hence Det (A * F) = 0. K by A2, A0, A3, A6, A7, Th50; :: thesis: verum