let n be Nat; 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; 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); 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; ( 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 )
; ( F in Permutations n or Det (A * F) = 0. K )
assume
not F in Permutations n
; 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; verum