:: by Katarzyna Zawadzka

::

:: Received May 17, 1993

:: Copyright (c) 1993-2021 Association of Mizar Users

definition
end;

:: deftheorem defines 0. MATRIX_3:def 1 :

for K being Ring

for n, m being Nat holds 0. (K,n,m) = n |-> (m |-> (0. K));

for K being Ring

for n, m being Nat holds 0. (K,n,m) = n |-> (m |-> (0. K));

definition

let K be Ring;

let A be Matrix of K;

ex b_{1} being Matrix of K st

( len b_{1} = len A & width b_{1} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{1} * (i,j) = - (A * (i,j)) ) )

for b_{1}, b_{2} being Matrix of K st len b_{1} = len A & width b_{1} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{1} * (i,j) = - (A * (i,j)) ) & len b_{2} = len A & width b_{2} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{2} * (i,j) = - (A * (i,j)) ) holds

b_{1} = b_{2}

end;
let A be Matrix of K;

func - A -> Matrix of K means :Def2: :: MATRIX_3:def 2

( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds

it * (i,j) = - (A * (i,j)) ) );

existence ( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds

it * (i,j) = - (A * (i,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines - MATRIX_3:def 2 :

for K being Ring

for A, b_{3} being Matrix of K holds

( b_{3} = - A iff ( len b_{3} = len A & width b_{3} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{3} * (i,j) = - (A * (i,j)) ) ) );

for K being Ring

for A, b

( b

b

definition

let K be Ring;

let A, B be Matrix of K;

ex b_{1} being Matrix of K st

( len b_{1} = len A & width b_{1} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{1} * (i,j) = (A * (i,j)) + (B * (i,j)) ) )

for b_{1}, b_{2} being Matrix of K st len b_{1} = len A & width b_{1} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{1} * (i,j) = (A * (i,j)) + (B * (i,j)) ) & len b_{2} = len A & width b_{2} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{2} * (i,j) = (A * (i,j)) + (B * (i,j)) ) holds

b_{1} = b_{2}

end;
let A, B be Matrix of K;

func A + B -> Matrix of K means :Def3: :: MATRIX_3:def 3

( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds

it * (i,j) = (A * (i,j)) + (B * (i,j)) ) );

existence ( len it = len A & width it = width A & ( for i, j being Nat st [i,j] in Indices A holds

it * (i,j) = (A * (i,j)) + (B * (i,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines + MATRIX_3:def 3 :

for K being Ring

for A, B, b_{4} being Matrix of K holds

( b_{4} = A + B iff ( len b_{4} = len A & width b_{4} = width A & ( for i, j being Nat st [i,j] in Indices A holds

b_{4} * (i,j) = (A * (i,j)) + (B * (i,j)) ) ) );

for K being Ring

for A, B, b

( b

b

theorem Th1: :: MATRIX_3:1

for n, m being Nat

for K being Ring

for i, j being Nat st [i,j] in Indices (0. (K,n,m)) holds

(0. (K,n,m)) * (i,j) = 0. K

for K being Ring

for i, j being Nat st [i,j] in Indices (0. (K,n,m)) holds

(0. (K,n,m)) * (i,j) = 0. K

proof end;

theorem :: MATRIX_3:2

for K being Ring

for A, B being Matrix of K st len A = len B & width A = width B holds

A + B = B + A

for A, B being Matrix of K st len A = len B & width A = width B holds

A + B = B + A

proof end;

theorem :: MATRIX_3:3

for K being Ring

for A, B, C being Matrix of K st len A = len B & width A = width B holds

(A + B) + C = A + (B + C)

for A, B, C being Matrix of K st len A = len B & width A = width B holds

(A + B) + C = A + (B + C)

proof end;

definition

let K be Ring;

let A, B be Matrix of K;

assume A1: width A = len B ;

ex b_{1} being Matrix of K st

( len b_{1} = len A & width b_{1} = width B & ( for i, j being Nat st [i,j] in Indices b_{1} holds

b_{1} * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )

for b_{1}, b_{2} being Matrix of K st len b_{1} = len A & width b_{1} = width B & ( for i, j being Nat st [i,j] in Indices b_{1} holds

b_{1} * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) & len b_{2} = len A & width b_{2} = width B & ( for i, j being Nat st [i,j] in Indices b_{2} holds

b_{2} * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) holds

b_{1} = b_{2}

end;
let A, B be Matrix of K;

assume A1: width A = len B ;

func A * B -> Matrix of K means :Def4: :: MATRIX_3:def 4

( len it = len A & width it = width B & ( for i, j being Nat st [i,j] in Indices it holds

it * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) );

existence ( len it = len A & width it = width B & ( for i, j being Nat st [i,j] in Indices it holds

it * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines * MATRIX_3:def 4 :

for K being Ring

for A, B being Matrix of K st width A = len B holds

for b_{4} being Matrix of K holds

( b_{4} = A * B iff ( len b_{4} = len A & width b_{4} = width B & ( for i, j being Nat st [i,j] in Indices b_{4} holds

b_{4} * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) );

for K being Ring

for A, B being Matrix of K st width A = len B holds

for b

( b

b

definition

let n, k, m be Nat;

let K be Ring;

let A be Matrix of n,k,K;

let B be Matrix of width A,m,K;

:: original: *

redefine func A * B -> Matrix of len A, width B,K;

coherence

A * B is Matrix of len A, width B,K

end;
let K be Ring;

let A be Matrix of n,k,K;

let B be Matrix of width A,m,K;

:: original: *

redefine func A * B -> Matrix of len A, width B,K;

coherence

A * B is Matrix of len A, width B,K

proof end;

definition

let K be Ring;

let M be Matrix of K;

let a be Element of K;

ex b_{1} being Matrix of K st

( len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = a * (M * (i,j)) ) )

for b_{1}, b_{2} being Matrix of K st len b_{1} = len M & width b_{1} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = a * (M * (i,j)) ) & len b_{2} = len M & width b_{2} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{2} * (i,j) = a * (M * (i,j)) ) holds

b_{1} = b_{2}

end;
let M be Matrix of K;

let a be Element of K;

func a * M -> Matrix of K means :: MATRIX_3:def 5

( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds

it * (i,j) = a * (M * (i,j)) ) );

existence ( len it = len M & width it = width M & ( for i, j being Nat st [i,j] in Indices M holds

it * (i,j) = a * (M * (i,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines * MATRIX_3:def 5 :

for K being Ring

for M being Matrix of K

for a being Element of K

for b_{4} being Matrix of K holds

( b_{4} = a * M iff ( len b_{4} = len M & width b_{4} = width M & ( for i, j being Nat st [i,j] in Indices M holds

b_{4} * (i,j) = a * (M * (i,j)) ) ) );

for K being Ring

for M being Matrix of K

for a being Element of K

for b

( b

b

definition
end;

:: deftheorem defines * MATRIX_3:def 6 :

for K being Ring

for M being Matrix of K

for a being Element of K holds M * a = a * M;

for K being Ring

for M being Matrix of K

for a being Element of K holds M * a = a * M;

theorem :: MATRIX_3:6

for K being Ring

for p, q being FinSequence of K st len p = len q holds

( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q )

for p, q being FinSequence of K st len p = len q holds

( len (mlt (p,q)) = len p & len (mlt (p,q)) = len q )

proof end;

theorem :: MATRIX_3:7

for n being Nat

for K being Ring

for i, l being Nat st [i,l] in Indices (1. (K,n)) & l = i holds

(Line ((1. (K,n)),i)) . l = 1. K

for K being Ring

for i, l being Nat st [i,l] in Indices (1. (K,n)) & l = i holds

(Line ((1. (K,n)),i)) . l = 1. K

proof end;

theorem :: MATRIX_3:8

for n being Nat

for K being Ring

for i, l being Nat st [i,l] in Indices (1. (K,n)) & l <> i holds

(Line ((1. (K,n)),i)) . l = 0. K

for K being Ring

for i, l being Nat st [i,l] in Indices (1. (K,n)) & l <> i holds

(Line ((1. (K,n)),i)) . l = 0. K

proof end;

theorem :: MATRIX_3:9

for n being Nat

for K being Ring

for l, j being Nat st [l,j] in Indices (1. (K,n)) & l = j holds

(Col ((1. (K,n)),j)) . l = 1. K

for K being Ring

for l, j being Nat st [l,j] in Indices (1. (K,n)) & l = j holds

(Col ((1. (K,n)),j)) . l = 1. K

proof end;

theorem :: MATRIX_3:10

for n being Nat

for K being Ring

for l, j being Nat st [l,j] in Indices (1. (K,n)) & l <> j holds

(Col ((1. (K,n)),j)) . l = 0. K

for K being Ring

for l, j being Nat st [l,j] in Indices (1. (K,n)) & l <> j holds

(Col ((1. (K,n)),j)) . l = 0. K

proof end;

Lm1: for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being FinSequence of L st ( for i being Element of NAT st i in dom p holds

p . i = 0. L ) holds

Sum p = 0. L

proof end;

theorem Th11: :: MATRIX_3:11

for n being Element of NAT

for K being non empty right_complementable add-associative right_zeroed addLoopStr holds Sum (n |-> (0. K)) = 0. K

for K being non empty right_complementable add-associative right_zeroed addLoopStr holds Sum (n |-> (0. K)) = 0. K

proof end;

theorem Th12: :: MATRIX_3:12

for K being non empty right_complementable add-associative right_zeroed addLoopStr

for p being FinSequence of K

for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds

p . k = 0. K ) holds

Sum p = p . i

for p being FinSequence of K

for i being Nat st i in dom p & ( for k being Nat st k in dom p & k <> i holds

p . k = 0. K ) holds

Sum p = p . i

proof end;

theorem Th14: :: MATRIX_3:14

for K being Ring

for p, q being FinSequence of K

for i being Nat st p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds

p . k = 0. K ) holds

for j being Nat st j in dom (mlt (p,q)) holds

( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )

for p, q being FinSequence of K

for i being Nat st p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds

p . k = 0. K ) holds

for j being Nat st j in dom (mlt (p,q)) holds

( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) )

proof end;

theorem Th15: :: MATRIX_3:15

for n being Nat

for K being Ring

for i, j being Nat st [i,j] in Indices (1. (K,n)) holds

( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )

for K being Ring

for i, j being Nat st [i,j] in Indices (1. (K,n)) holds

( ( i = j implies (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )

proof end;

theorem Th16: :: MATRIX_3:16

for n being Nat

for K being Ring

for i, j being Nat st [i,j] in Indices (1. (K,n)) holds

( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )

for K being Ring

for i, j being Nat st [i,j] in Indices (1. (K,n)) holds

( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )

proof end;

theorem Th17: :: MATRIX_3:17

for K being Ring

for p, q being FinSequence of K

for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds

p . k = 0. K ) holds

Sum (mlt (p,q)) = q . i

for p, q being FinSequence of K

for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds

p . k = 0. K ) holds

Sum (mlt (p,q)) = q . i

proof end;

theorem :: MATRIX_3:21

for K being Field

for a1, a2, b1, b2, c1, c2, d1, d2 being Element of K holds ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))

for a1, a2, b1, b2, c1, c2, d1, d2 being Element of K holds ((a1,b1) ][ (c1,d1)) * ((a2,b2) ][ (c2,d2)) = (((a1 * a2) + (b1 * c2)),((a1 * b2) + (b1 * d2))) ][ (((c1 * a2) + (d1 * c2)),((c1 * b2) + (d1 * d2)))

proof end;

theorem :: MATRIX_3:22

for K being Field

for A, B being Matrix of K st width A = len B & width B <> 0 holds

(A * B) @ = (B @) * (A @)

for A, B being Matrix of K st width A = len B & width B <> 0 holds

(A * B) @ = (B @) * (A @)

proof end;

definition

let I, J be non empty set ;

let X be Element of Fin I;

let Y be Element of Fin J;

:: original: [:

redefine func [:X,Y:] -> Element of Fin [:I,J:];

coherence

[:X,Y:] is Element of Fin [:I,J:]

end;
let X be Element of Fin I;

let Y be Element of Fin J;

:: original: [:

redefine func [:X,Y:] -> Element of Fin [:I,J:];

coherence

[:X,Y:] is Element of Fin [:I,J:]

proof end;

definition

let I, J, D be non empty set ;

let G be BinOp of D;

let f be Function of I,D;

let g be Function of J,D;

:: original: *

redefine func G * (f,g) -> Function of [:I,J:],D;

coherence

G * (f,g) is Function of [:I,J:],D by FINSEQOP:79;

end;
let G be BinOp of D;

let f be Function of I,D;

let g be Function of J,D;

:: original: *

redefine func G * (f,g) -> Function of [:I,J:],D;

coherence

G * (f,g) is Function of [:I,J:],D by FINSEQOP:79;

theorem Th23: :: MATRIX_3:23

for I, J, D being non empty set

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds

F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds

F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))

proof end;

theorem Th24: :: MATRIX_3:24

for D, I, J being non empty set

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D st F is commutative & F is associative holds

for x being Element of I

for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D st F is commutative & F is associative holds

for x being Element of I

for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ ({.y.},g)))))

proof end;

theorem Th25: :: MATRIX_3:25

for D, I, J being non empty set

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds

for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G is_distributive_wrt F holds

for x being Element of I holds F $$ ([:{.x.},Y:],(G * (f,g))) = F $$ ({.x.},(G [:] (f,(F $$ (Y,g)))))

proof end;

theorem Th26: :: MATRIX_3:26

for D, I, J being non empty set

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds

F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F holds

F $$ ([:X,Y:],(G * (f,g))) = F $$ (X,(G [:] (f,(F $$ (Y,g)))))

proof end;

theorem :: MATRIX_3:27

for D, I, J being non empty set

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D st F is commutative & F is associative & G is commutative holds

for x being Element of I

for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D st F is commutative & F is associative & G is commutative holds

for x being Element of I

for y being Element of J holds F $$ ([:{.x.},{.y.}:],(G * (f,g))) = F $$ ({.y.},(G [;] ((F $$ ({.x.},f)),g)))

proof end;

theorem :: MATRIX_3:28

for D, I, J being non empty set

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds

F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))

for F, G being BinOp of D

for f being Function of I,D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp & G is_distributive_wrt F & G is commutative holds

F $$ ([:X,Y:],(G * (f,g))) = F $$ (Y,(G [;] ((F $$ (X,f)),g)))

proof end;

theorem Th29: :: MATRIX_3:29

for D, I, J being non empty set

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of I,D

for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds

for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds

F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of I,D

for Y being Element of Fin J st F is having_a_unity & F is commutative & F is associative holds

for x being Element of I st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) holds

F $$ ([:{.x.},Y:],f) = F $$ ({.x.},g)

proof end;

theorem Th30: :: MATRIX_3:30

for D, I, J being non empty set

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of I,D

for X being Element of Fin I

for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds

F $$ ([:X,Y:],f) = F $$ (X,g)

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of I,D

for X being Element of Fin I

for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds

F $$ ([:X,Y:],f) = F $$ (X,g)

proof end;

theorem Th31: :: MATRIX_3:31

for D, I, J being non empty set

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of J,D

for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds

for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds

F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of J,D

for X being Element of Fin I st F is having_a_unity & F is commutative & F is associative holds

for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds

F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)

proof end;

theorem Th32: :: MATRIX_3:32

for D, I, J being non empty set

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds

F $$ ([:X,Y:],f) = F $$ (Y,g)

for F being BinOp of D

for f being Function of [:I,J:],D

for g being Function of J,D

for X being Element of Fin I

for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds

F $$ ([:X,Y:],f) = F $$ (Y,g)

proof end;

theorem :: MATRIX_3:33

for K being commutative Ring

for A, B, C being Matrix of K st width A = len B & width B = len C holds

(A * B) * C = A * (B * C)

for A, B, C being Matrix of K st width A = len B & width B = len C holds

(A * B) * C = A * (B * C)

proof end;

definition

let n be Nat;

let K be Ring;

let M be Matrix of n,K;

let p be Element of Permutations n;

ex b_{1} being FinSequence of K st

( len b_{1} = n & ( for i, j being Nat st i in dom b_{1} & j = p . i holds

b_{1} . i = M * (i,j) ) )

for b_{1}, b_{2} being FinSequence of K st len b_{1} = n & ( for i, j being Nat st i in dom b_{1} & j = p . i holds

b_{1} . i = M * (i,j) ) & len b_{2} = n & ( for i, j being Nat st i in dom b_{2} & j = p . i holds

b_{2} . i = M * (i,j) ) holds

b_{1} = b_{2}

end;
let K be Ring;

let M be Matrix of n,K;

let p be Element of Permutations n;

func Path_matrix (p,M) -> FinSequence of K means :Def7: :: MATRIX_3:def 7

( len it = n & ( for i, j being Nat st i in dom it & j = p . i holds

it . i = M * (i,j) ) );

existence ( len it = n & ( for i, j being Nat st i in dom it & j = p . i holds

it . i = M * (i,j) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines Path_matrix MATRIX_3:def 7 :

for n being Nat

for K being Ring

for M being Matrix of n,K

for p being Element of Permutations n

for b_{5} being FinSequence of K holds

( b_{5} = Path_matrix (p,M) iff ( len b_{5} = n & ( for i, j being Nat st i in dom b_{5} & j = p . i holds

b_{5} . i = M * (i,j) ) ) );

for n being Nat

for K being Ring

for M being Matrix of n,K

for p being Element of Permutations n

for b

( b

b

definition

let n be Nat;

let K be Ring;

let M be Matrix of n,K;

ex b_{1} being Function of (Permutations n), the carrier of K st

for p being Element of Permutations n holds b_{1} . p = - (( the multF of K $$ (Path_matrix (p,M))),p)

for b_{1}, b_{2} being Function of (Permutations n), the carrier of K st ( for p being Element of Permutations n holds b_{1} . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ) & ( for p being Element of Permutations n holds b_{2} . p = - (( the multF of K $$ (Path_matrix (p,M))),p) ) holds

b_{1} = b_{2}

end;
let K be Ring;

let M be Matrix of n,K;

func Path_product M -> Function of (Permutations n), the carrier of K means :Def8: :: MATRIX_3:def 8

for p being Element of Permutations n holds it . p = - (( the multF of K $$ (Path_matrix (p,M))),p);

existence for p being Element of Permutations n holds it . p = - (( the multF of K $$ (Path_matrix (p,M))),p);

ex b

for p being Element of Permutations n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines Path_product MATRIX_3:def 8 :

for n being Nat

for K being Ring

for M being Matrix of n,K

for b_{4} being Function of (Permutations n), the carrier of K holds

( b_{4} = Path_product M iff for p being Element of Permutations n holds b_{4} . p = - (( the multF of K $$ (Path_matrix (p,M))),p) );

for n being Nat

for K being Ring

for M being Matrix of n,K

for b

( b

definition

let n be Nat;

let K be Ring;

let M be Matrix of n,K;

the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) is Element of K ;

end;
let K be Ring;

let M be Matrix of n,K;

func Det M -> Element of K equals :: MATRIX_3:def 9

the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M));

coherence the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M));

the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M)) is Element of K ;

:: deftheorem defines Det MATRIX_3:def 9 :

for n being Nat

for K being Ring

for M being Matrix of n,K holds Det M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M));

for n being Nat

for K being Ring

for M being Matrix of n,K holds Det M = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),(Path_product M));

definition

let n be Nat;

let K be Ring;

let M be Matrix of n,K;

ex b_{1} being FinSequence of K st

( len b_{1} = n & ( for i being Nat st i in Seg n holds

b_{1} . i = M * (i,i) ) )

for b_{1}, b_{2} being FinSequence of K st len b_{1} = n & ( for i being Nat st i in Seg n holds

b_{1} . i = M * (i,i) ) & len b_{2} = n & ( for i being Nat st i in Seg n holds

b_{2} . i = M * (i,i) ) holds

b_{1} = b_{2}

end;
let K be Ring;

let M be Matrix of n,K;

func diagonal_of_Matrix M -> FinSequence of K means :: MATRIX_3:def 10

( len it = n & ( for i being Nat st i in Seg n holds

it . i = M * (i,i) ) );

existence ( len it = n & ( for i being Nat st i in Seg n holds

it . i = M * (i,i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines diagonal_of_Matrix MATRIX_3:def 10 :

for n being Nat

for K being Ring

for M being Matrix of n,K

for b_{4} being FinSequence of K holds

( b_{4} = diagonal_of_Matrix M iff ( len b_{4} = n & ( for i being Nat st i in Seg n holds

b_{4} . i = M * (i,i) ) ) );

for n being Nat

for K being Ring

for M being Matrix of n,K

for b

( b

b