:: by Yatsuka Nakamura , Kunio Oniumi and Wenpai Chang

::

:: Received April 2, 2008

:: Copyright (c) 2008-2019 Association of Mizar Users

definition
end;

:: deftheorem defines 0* MATRIX14:def 1 :

for K being non empty ZeroStr

for n being Element of NAT holds 0* (K,n) = n |-> (0. K);

for K being non empty ZeroStr

for n being Element of NAT holds 0* (K,n) = n |-> (0. K);

definition

let K be non empty ZeroStr ;

let n be Element of NAT ;

:: original: 0*

redefine func 0* (K,n) -> Element of n -tuples_on the carrier of K;

coherence

0* (K,n) is Element of n -tuples_on the carrier of K ;

end;
let n be Element of NAT ;

:: original: 0*

redefine func 0* (K,n) -> Element of n -tuples_on the carrier of K;

coherence

0* (K,n) is Element of n -tuples_on the carrier of K ;

theorem Th1: :: MATRIX14:1

for L being non empty addLoopStr

for x being FinSequence of L holds x is Element of (len x) -tuples_on the carrier of L

for x being FinSequence of L holds x is Element of (len x) -tuples_on the carrier of L

proof end;

theorem Th2: :: MATRIX14:2

for L being non empty addLoopStr

for x1, x2 being FinSequence of L st len x1 = len x2 holds

len (x1 + x2) = len x1

for x1, x2 being FinSequence of L st len x1 = len x2 holds

len (x1 + x2) = len x1

proof end;

theorem Th3: :: MATRIX14:3

for L being non empty addLoopStr

for x1, x2 being FinSequence of L st len x1 = len x2 holds

len (x1 - x2) = len x1

for x1, x2 being FinSequence of L st len x1 = len x2 holds

len (x1 - x2) = len x1

proof end;

theorem Th4: :: MATRIX14:4

for G being non empty multLoopStr

for x1, x2 being FinSequence of G

for i being Element of NAT st i in dom (mlt (x1,x2)) holds

( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )

for x1, x2 being FinSequence of G

for i being Element of NAT st i in dom (mlt (x1,x2)) holds

( (mlt (x1,x2)) . i = (x1 /. i) * (x2 /. i) & (mlt (x1,x2)) /. i = (x1 /. i) * (x2 /. i) )

proof end;

theorem Th5: :: MATRIX14:5

for L being non empty addLoopStr

for x1, x2 being FinSequence of L

for i being Nat st len x1 = len x2 & 1 <= i & i <= len x1 holds

( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) )

for x1, x2 being FinSequence of L

for i being Nat st len x1 = len x2 & 1 <= i & i <= len x1 holds

( (x1 + x2) . i = (x1 /. i) + (x2 /. i) & (x1 - x2) . i = (x1 /. i) - (x2 /. i) )

proof end;

theorem Th6: :: MATRIX14:6

for K being Field

for a being Element of K

for x being FinSequence of K holds

( - (a * x) = (- a) * x & - (a * x) = a * (- x) )

for a being Element of K

for x being FinSequence of K holds

( - (a * x) = (- a) * x & - (a * x) = a * (- x) )

proof end;

theorem Th7: :: MATRIX14:7

for G being non empty multLoopStr

for x1, x2, y1, y2 being FinSequence of G st len x1 = len x2 & len y1 = len y2 holds

mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))

for x1, x2, y1, y2 being FinSequence of G st len x1 = len x2 & len y1 = len y2 holds

mlt ((x1 ^ y1),(x2 ^ y2)) = (mlt (x1,x2)) ^ (mlt (y1,y2))

proof end;

theorem Th8: :: MATRIX14:8

for K being Field

for x, y being FinSequence of K

for a being Element of K st len x = len y holds

( mlt ((a * x),y) = a * (mlt (x,y)) & mlt (x,(a * y)) = a * (mlt (x,y)) )

for x, y being FinSequence of K

for a being Element of K st len x = len y holds

( mlt ((a * x),y) = a * (mlt (x,y)) & mlt (x,(a * y)) = a * (mlt (x,y)) )

proof end;

theorem :: MATRIX14:9

for K being Field

for x, y being FinSequence of K

for a being Element of K st len x = len y holds

|((a * x),y)| = a * |(x,y)|

for x, y being FinSequence of K

for a being Element of K st len x = len y holds

|((a * x),y)| = a * |(x,y)|

proof end;

theorem Th10: :: MATRIX14:10

for K being Field

for x, y being FinSequence of K

for a being Element of K st len x = len y holds

|(x,(a * y))| = a * |(x,y)|

for x, y being FinSequence of K

for a being Element of K st len x = len y holds

|(x,(a * y))| = a * |(x,y)|

proof end;

theorem Th11: :: MATRIX14:11

for K being Field

for x, y1, y2 being FinSequence of K

for a being Element of K st len x = len y1 & len x = len y2 holds

|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|

for x, y1, y2 being FinSequence of K

for a being Element of K st len x = len y1 & len x = len y2 holds

|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|

proof end;

theorem Th12: :: MATRIX14:12

for K being Field

for x1, x2, y1, y2 being FinSequence of K st len x1 = len x2 & len y1 = len y2 holds

|((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|

for x1, x2, y1, y2 being FinSequence of K st len x1 = len x2 & len y1 = len y2 holds

|((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|

proof end;

theorem Th13: :: MATRIX14:13

for n being Element of NAT

for K being Field

for p1 being Element of n -tuples_on the carrier of K holds mlt (p1,(n |-> (0. K))) = n |-> (0. K)

for K being Field

for p1 being Element of n -tuples_on the carrier of K holds mlt (p1,(n |-> (0. K))) = n |-> (0. K)

proof end;

notation
end;

theorem Th17: :: MATRIX14:17

for n being Element of NAT

for K being Field

for A, B, C being Matrix of n,K holds (A * B) * C = A * (B * C)

for K being Field

for A, B, C being Matrix of n,K holds (A * B) * C = A * (B * C)

proof end;

theorem Th18: :: MATRIX14:18

for n being Element of NAT

for K being Field

for A, B being Matrix of n,K holds

( A is invertible & B = A ~ iff ( B * A = 1. (K,n) & A * B = 1. (K,n) ) )

for K being Field

for A, B being Matrix of n,K holds

( A is invertible & B = A ~ iff ( B * A = 1. (K,n) & A * B = 1. (K,n) ) )

proof end;

theorem Th19: :: MATRIX14:19

for n being Element of NAT

for K being Field

for A being Matrix of n,K holds

( A is invertible iff ex B being Matrix of n,K st

( B * A = 1. (K,n) & A * B = 1. (K,n) ) )

for K being Field

for A being Matrix of n,K holds

( A is invertible iff ex B being Matrix of n,K st

( B * A = 1. (K,n) & A * B = 1. (K,n) ) )

proof end;

definition

let K be Field;

let n, i be Nat;

Replace ((n |-> (0. K)),i,(1. K)) is FinSequence of K ;

end;
let n, i be Nat;

func Base_FinSeq (K,n,i) -> FinSequence of K equals :: MATRIX14:def 2

Replace ((n |-> (0. K)),i,(1. K));

coherence Replace ((n |-> (0. K)),i,(1. K));

Replace ((n |-> (0. K)),i,(1. K)) is FinSequence of K ;

:: deftheorem defines Base_FinSeq MATRIX14:def 2 :

for K being Field

for n, i being Nat holds Base_FinSeq (K,n,i) = Replace ((n |-> (0. K)),i,(1. K));

for K being Field

for n, i being Nat holds Base_FinSeq (K,n,i) = Replace ((n |-> (0. K)),i,(1. K));

theorem Th25: :: MATRIX14:25

for K being Field

for i, j, n being Nat st 1 <= j & j <= n & i <> j holds

(Base_FinSeq (K,n,i)) . j = 0. K

for i, j, n being Nat st 1 <= j & j <= n & i <> j holds

(Base_FinSeq (K,n,i)) . j = 0. K

proof end;

theorem Th27: :: MATRIX14:27

for n being Element of NAT

for K being Field

for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds

(1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j

for K being Field

for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds

(1. (K,n)) * (i,j) = (Base_FinSeq (K,n,i)) . j

proof end;

theorem :: MATRIX14:28

for n being Element of NAT

for K being Field

for A being Matrix of n,K holds

( A = 0. (K,n) iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds

A * (i,j) = 0. K )

for K being Field

for A being Matrix of n,K holds

( A = 0. (K,n) iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds

A * (i,j) = 0. K )

proof end;

theorem Th29: :: MATRIX14:29

for n being Element of NAT

for K being Field

for A being Matrix of n,K holds

( A = 1. (K,n) iff for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds

A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )

for K being Field

for A being Matrix of n,K holds

( A = 1. (K,n) iff for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds

A * (i,j) = IFEQ (i,j,(1. K),(0. K)) )

proof end;

theorem Th30: :: MATRIX14:30

for n being Element of NAT

for K being Field

for A, B being Matrix of n,K holds (A * B) @ = (B @) * (A @)

for K being Field

for A, B being Matrix of n,K holds (A * B) @ = (B @) * (A @)

proof end;

theorem :: MATRIX14:31

for n being Element of NAT

for K being Field

for A being Matrix of n,K st A is invertible holds

( A @ is invertible & (A @) ~ = (A ~) @ )

for K being Field

for A being Matrix of n,K st A is invertible holds

( A @ is invertible & (A @) ~ = (A ~) @ )

proof end;

theorem Th32: :: MATRIX14:32

for K being Field

for x being FinSequence of K

for a being Element of K st ex i being Element of NAT st

( 1 <= i & i <= len x & x . i = a & ( for j being Element of NAT st j <> i & 1 <= j & j <= len x holds

x . j = 0. K ) ) holds

Sum x = a

for x being FinSequence of K

for a being Element of K st ex i being Element of NAT st

( 1 <= i & i <= len x & x . i = a & ( for j being Element of NAT st j <> i & 1 <= j & j <= len x holds

x . j = 0. K ) ) holds

Sum x = a

proof end;

theorem :: MATRIX14:33

for K being Field

for f1, f2 being FinSequence of K holds

( dom (mlt (f1,f2)) = (dom f1) /\ (dom f2) & ( for i being Element of NAT st i in dom (mlt (f1,f2)) holds

(mlt (f1,f2)) . i = (f1 /. i) * (f2 /. i) ) )

for f1, f2 being FinSequence of K holds

( dom (mlt (f1,f2)) = (dom f1) /\ (dom f2) & ( for i being Element of NAT st i in dom (mlt (f1,f2)) holds

(mlt (f1,f2)) . i = (f1 /. i) * (f2 /. i) ) )

proof end;

theorem Th34: :: MATRIX14:34

for m being Element of NAT

for K being Field

for x, y being FinSequence of K

for i being Element of NAT st len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m holds

( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds

y . j = 0. K ) )

for K being Field

for x, y being FinSequence of K

for i being Element of NAT st len x = m & y = mlt (x,(Base_FinSeq (K,m,i))) & 1 <= i & i <= m holds

( y . i = x . i & ( for j being Element of NAT st j <> i & 1 <= j & j <= m holds

y . j = 0. K ) )

proof end;

theorem Th35: :: MATRIX14:35

for m, i being Element of NAT

for K being Field

for x being FinSequence of K st len x = m & 1 <= i & i <= m holds

( |(x,(Base_FinSeq (K,m,i)))| = x . i & |(x,(Base_FinSeq (K,m,i)))| = x /. i )

for K being Field

for x being FinSequence of K st len x = m & 1 <= i & i <= m holds

( |(x,(Base_FinSeq (K,m,i)))| = x . i & |(x,(Base_FinSeq (K,m,i)))| = x /. i )

proof end;

theorem Th36: :: MATRIX14:36

for K being Field

for m, i being Element of NAT st 1 <= i & i <= m holds

|((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K

for m, i being Element of NAT st 1 <= i & i <= m holds

|((Base_FinSeq (K,m,i)),(Base_FinSeq (K,m,i)))| = 1. K

proof end;

theorem Th37: :: MATRIX14:37

for n being Element of NAT

for K being Field

for a being Element of K

for P, Q being Matrix of n,K st n > 0 & a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds

P . i = Base_FinSeq (K,n,i) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds

Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds

Q . i = Base_FinSeq (K,n,i) ) holds

( P is invertible & Q = P ~ )

for K being Field

for a being Element of K

for P, Q being Matrix of n,K st n > 0 & a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds

P . i = Base_FinSeq (K,n,i) ) & Q * (1,1) = a & ( for j being Element of NAT st 1 < j & j <= n holds

Q * (1,j) = - (a * (P * (1,j))) ) & ( for i being Element of NAT st 1 < i & i <= n holds

Q . i = Base_FinSeq (K,n,i) ) holds

( P is invertible & Q = P ~ )

proof end;

theorem Th38: :: MATRIX14:38

for n being Element of NAT

for K being Field

for a being Element of K

for P being Matrix of n,K st n > 0 & a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds

P . i = Base_FinSeq (K,n,i) ) holds

P is invertible

for K being Field

for a being Element of K

for P being Matrix of n,K st n > 0 & a <> 0. K & P * (1,1) = a " & ( for i being Element of NAT st 1 < i & i <= n holds

P . i = Base_FinSeq (K,n,i) ) holds

P is invertible

proof end;

theorem Th39: :: MATRIX14:39

for n being Element of NAT

for K being Field

for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds

ex P being Matrix of n,K st

( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds

(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds

(A * P) * (i,1) = 0. K ) )

for K being Field

for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds

ex P being Matrix of n,K st

( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds

(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds

(A * P) * (i,1) = 0. K ) )

proof end;

theorem Th40: :: MATRIX14:40

for n being Element of NAT

for K being Field

for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds

ex P being Matrix of n,K st

( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds

(P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds

(P * A) * (1,j) = 0. K ) )

for K being Field

for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds

ex P being Matrix of n,K st

( P is invertible & (P * A) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds

(P * A) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n & A * (1,j) = 0. K holds

(P * A) * (1,j) = 0. K ) )

proof end;

theorem Th41: :: MATRIX14:41

for n being Element of NAT

for K being Field

for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds

ex P, Q being Matrix of n,K st

( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds

((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds

((P * A) * Q) * (1,j) = 0. K ) )

for K being Field

for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds

ex P, Q being Matrix of n,K st

( P is invertible & Q is invertible & ((P * A) * Q) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds

((P * A) * Q) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds

((P * A) * Q) * (1,j) = 0. K ) )

proof end;

theorem Th42: :: MATRIX14:42

for D being non empty set

for m, n, i, j being Element of NAT

for A being Matrix of m,n,D holds Swap (A,i,j) is Matrix of m,n,D

for m, n, i, j being Element of NAT

for A being Matrix of m,n,D holds Swap (A,i,j) is Matrix of m,n,D

proof end;

definition

let K be Field;

let n be Element of NAT ;

let i0 be Nat;

correctness

coherence

Swap ((1. (K,n)),1,i0) is Matrix of n,K;

end;
let n be Element of NAT ;

let i0 be Nat;

correctness

coherence

Swap ((1. (K,n)),1,i0) is Matrix of n,K;

proof end;

:: deftheorem defines SwapDiagonal MATRIX14:def 3 :

for K being Field

for n being Element of NAT

for i0 being Nat holds SwapDiagonal (K,n,i0) = Swap ((1. (K,n)),1,i0);

for K being Field

for n being Element of NAT

for i0 being Nat holds SwapDiagonal (K,n,i0) = Swap ((1. (K,n)),1,i0);

theorem Th43: :: MATRIX14:43

for K being Field

for n being Element of NAT

for i0 being Nat

for A being Matrix of n,K st 1 <= i0 & i0 <= n & A = SwapDiagonal (K,n,i0) holds

for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 holds

( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) )

for n being Element of NAT

for i0 being Nat

for A being Matrix of n,K st 1 <= i0 & i0 <= n & A = SwapDiagonal (K,n,i0) holds

for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i0 <> 1 holds

( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) )

proof end;

theorem Th44: :: MATRIX14:44

for K being Field

for n being Element of NAT

for A being Matrix of n,K

for i being Nat st 1 <= i & i <= n holds

(SwapDiagonal (K,n,1)) * (i,i) = 1. K

for n being Element of NAT

for A being Matrix of n,K

for i being Nat st 1 <= i & i <= n holds

(SwapDiagonal (K,n,1)) * (i,i) = 1. K

proof end;

theorem Th45: :: MATRIX14:45

for K being Field

for n being Element of NAT

for A being Matrix of n,K

for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i <> j holds

(SwapDiagonal (K,n,1)) * (i,j) = 0. K

for n being Element of NAT

for A being Matrix of n,K

for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n & i <> j holds

(SwapDiagonal (K,n,1)) * (i,j) = 0. K

proof end;

theorem Th46: :: MATRIX14:46

for K being Field

for n, i0 being Element of NAT

for A being Matrix of n,K st i0 = 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds

( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) holds

A = SwapDiagonal (K,n,i0)

for n, i0 being Element of NAT

for A being Matrix of n,K st i0 = 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds

( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) holds

A = SwapDiagonal (K,n,i0)

proof end;

theorem Th47: :: MATRIX14:47

for K being Field

for n, i0 being Element of NAT

for A being Matrix of n,K st 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds

( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) ) ) holds

A = SwapDiagonal (K,n,i0)

for n, i0 being Element of NAT

for A being Matrix of n,K st 1 <= i0 & i0 <= n & i0 <> 1 & ( for i, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds

( ( i = 1 & j = i0 implies A * (i,j) = 1. K ) & ( i = i0 & j = 1 implies A * (i,j) = 1. K ) & ( i = 1 & j = 1 implies A * (i,j) = 0. K ) & ( i = i0 & j = i0 implies A * (i,j) = 0. K ) & ( ( ( not i = 1 & not i = i0 ) or ( not j = 1 & not j = i0 ) ) implies ( ( i = j implies A * (i,j) = 1. K ) & ( i <> j implies A * (i,j) = 0. K ) ) ) ) ) holds

A = SwapDiagonal (K,n,i0)

proof end;

theorem Th48: :: MATRIX14:48

for n being Element of NAT

for K being Field

for A being Matrix of n,K

for i0 being Element of NAT st 1 <= i0 & i0 <= n holds

( ( for j being Element of NAT st 1 <= j & j <= n holds

( ((SwapDiagonal (K,n,i0)) * A) * (i0,j) = A * (1,j) & ((SwapDiagonal (K,n,i0)) * A) * (1,j) = A * (i0,j) ) ) & ( for i, j being Element of NAT st i <> 1 & i <> i0 & 1 <= i & i <= n & 1 <= j & j <= n holds

((SwapDiagonal (K,n,i0)) * A) * (i,j) = A * (i,j) ) )

for K being Field

for A being Matrix of n,K

for i0 being Element of NAT st 1 <= i0 & i0 <= n holds

( ( for j being Element of NAT st 1 <= j & j <= n holds

( ((SwapDiagonal (K,n,i0)) * A) * (i0,j) = A * (1,j) & ((SwapDiagonal (K,n,i0)) * A) * (1,j) = A * (i0,j) ) ) & ( for i, j being Element of NAT st i <> 1 & i <> i0 & 1 <= i & i <= n & 1 <= j & j <= n holds

((SwapDiagonal (K,n,i0)) * A) * (i,j) = A * (i,j) ) )

proof end;

theorem Th49: :: MATRIX14:49

for n being Element of NAT

for K being Field

for i0 being Element of NAT st 1 <= i0 & i0 <= n holds

( SwapDiagonal (K,n,i0) is invertible & (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) )

for K being Field

for i0 being Element of NAT st 1 <= i0 & i0 <= n holds

( SwapDiagonal (K,n,i0) is invertible & (SwapDiagonal (K,n,i0)) ~ = SwapDiagonal (K,n,i0) )

proof end;

theorem Th50: :: MATRIX14:50

for n being Element of NAT

for K being Field

for i0 being Element of NAT st 1 <= i0 & i0 <= n holds

(SwapDiagonal (K,n,i0)) @ = SwapDiagonal (K,n,i0)

for K being Field

for i0 being Element of NAT st 1 <= i0 & i0 <= n holds

(SwapDiagonal (K,n,i0)) @ = SwapDiagonal (K,n,i0)

proof end;

theorem Th51: :: MATRIX14:51

for n being Element of NAT

for K being Field

for A being Matrix of n,K

for j0 being Element of NAT st 1 <= j0 & j0 <= n holds

( ( for i being Element of NAT st 1 <= i & i <= n holds

( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds

(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) )

for K being Field

for A being Matrix of n,K

for j0 being Element of NAT st 1 <= j0 & j0 <= n holds

( ( for i being Element of NAT st 1 <= i & i <= n holds

( (A * (SwapDiagonal (K,n,j0))) * (i,j0) = A * (i,1) & (A * (SwapDiagonal (K,n,j0))) * (i,1) = A * (i,j0) ) ) & ( for i, j being Element of NAT st j <> 1 & j <> j0 & 1 <= i & i <= n & 1 <= j & j <= n holds

(A * (SwapDiagonal (K,n,j0))) * (i,j) = A * (i,j) ) )

proof end;

theorem Th52: :: MATRIX14:52

for n being Element of NAT

for K being Field

for A being Matrix of n,K holds

( A = 0. (K,n) iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds

A * (i,j) = 0. K )

for K being Field

for A being Matrix of n,K holds

( A = 0. (K,n) iff for i, j being Element of NAT st 1 <= i & i <= n & 1 <= j & j <= n holds

A * (i,j) = 0. K )

proof end;

theorem Th53: :: MATRIX14:53

for n being Element of NAT

for K being Field

for A being Matrix of n,K st A <> 0. (K,n) holds

ex B, C being Matrix of n,K st

( B is invertible & C is invertible & ((B * A) * C) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds

((B * A) * C) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds

((B * A) * C) * (1,j) = 0. K ) )

for K being Field

for A being Matrix of n,K st A <> 0. (K,n) holds

ex B, C being Matrix of n,K st

( B is invertible & C is invertible & ((B * A) * C) * (1,1) = 1. K & ( for i being Element of NAT st 1 < i & i <= n holds

((B * A) * C) * (i,1) = 0. K ) & ( for j being Element of NAT st 1 < j & j <= n holds

((B * A) * C) * (1,j) = 0. K ) )

proof end;

theorem Th54: :: MATRIX14:54

for n being Element of NAT

for K being Field

for A, B being Matrix of n,K st B * A = 1. (K,n) holds

ex B2 being Matrix of n,K st A * B2 = 1. (K,n)

for K being Field

for A, B being Matrix of n,K st B * A = 1. (K,n) holds

ex B2 being Matrix of n,K st A * B2 = 1. (K,n)

proof end;

theorem Th55: :: MATRIX14:55

for n being Element of NAT

for K being Field

for A being Matrix of n,K holds

( ex B1 being Matrix of n,K st B1 * A = 1. (K,n) iff ex B2 being Matrix of n,K st A * B2 = 1. (K,n) )

for K being Field

for A being Matrix of n,K holds

( ex B1 being Matrix of n,K st B1 * A = 1. (K,n) iff ex B2 being Matrix of n,K st A * B2 = 1. (K,n) )

proof end;

theorem :: MATRIX14:56

for n being Element of NAT

for K being Field

for A, B being Matrix of n,K st A * B = 1. (K,n) holds

( A is invertible & B is invertible )

for K being Field

for A, B being Matrix of n,K st A * B = 1. (K,n) holds

( A is invertible & B is invertible )

proof end;