:: by Xiquan Liang , Tao Sun and Dahai Hu

::

:: Received August 13, 2007

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

Lm1: for n, m being Nat

for K being Field

for k, l being Nat

for M, M1, M2 being Matrix of n,m,K

for pK, qK being FinSequence of K

for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,k,pK) & M2 = RLine (M1,l,qK) holds

( ( i = l implies M2 * (i,j) = M * (k,j) ) & ( i = k implies M2 * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies M2 * (i,j) = M * (i,j) ) )

proof end;

definition

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

ex b_{1} being Matrix of n,m,K st

( len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{1} * (i,j) = M * (k,j) ) & ( i = k implies b_{1} * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b_{1} * (i,j) = M * (i,j) ) ) ) )

for b_{1}, b_{2} being Matrix of n,m,K st len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{1} * (i,j) = M * (k,j) ) & ( i = k implies b_{1} * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b_{1} * (i,j) = M * (i,j) ) ) ) & len b_{2} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{2} * (i,j) = M * (k,j) ) & ( i = k implies b_{2} * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b_{2} * (i,j) = M * (i,j) ) ) ) holds

b_{1} = b_{2}

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

func InterchangeLine (M,l,k) -> Matrix of n,m,K means :Def1: :: MATRIX12:def 1

( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies it * (i,j) = M * (k,j) ) & ( i = k implies it * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies it * (i,j) = M * (i,j) ) ) ) );

existence ( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies it * (i,j) = M * (k,j) ) & ( i = k implies it * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies it * (i,j) = M * (i,j) ) ) ) );

ex b

( len b

( ( i = l implies b

proof end;

uniqueness for b

( ( i = l implies b

( ( i = l implies b

b

proof end;

:: deftheorem Def1 defines InterchangeLine MATRIX12:def 1 :

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat

for b_{7} being Matrix of n,m,K holds

( b_{7} = InterchangeLine (M,l,k) iff ( len b_{7} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{7} * (i,j) = M * (k,j) ) & ( i = k implies b_{7} * (i,j) = M * (l,j) ) & ( i <> l & i <> k implies b_{7} * (i,j) = M * (i,j) ) ) ) ) );

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat

for b

( b

( ( i = l implies b

theorem Th2: :: MATRIX12:2

for k, l, n, m being Nat

for K being Field

for M, M1 being Matrix of n,m,K

for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine (M,l,k) holds

( ( i = l implies Line (M1,i) = Line (M,k) ) & ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) )

for K being Field

for M, M1 being Matrix of n,m,K

for i being Nat st l in dom M & k in dom M & i in dom M & M1 = InterchangeLine (M,l,k) holds

( ( i = l implies Line (M1,i) = Line (M,k) ) & ( i = k implies Line (M1,i) = Line (M,l) ) & ( i <> l & i <> k implies Line (M1,i) = Line (M,i) ) )

proof end;

theorem Th3: :: MATRIX12:3

for n, m being Nat

for K being Field

for a being Element of K

for i, j being Nat

for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds

(a * (Line (M,i))) . j = a * (M * (i,j))

for K being Field

for a being Element of K

for i, j being Nat

for M being Matrix of n,m,K st i in dom M & j in Seg (width M) holds

(a * (Line (M,i))) . j = a * (M * (i,j))

proof end;

Lm2: for n, m being Nat

for K being Field

for a being Element of K

for l being Nat

for M, M1 being Matrix of n,m,K

for pK being FinSequence of K

for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) holds

( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )

proof end;

definition

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

ex b_{1} being Matrix of n,m,K st

( len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{1} * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) )

for b_{1}, b_{2} being Matrix of n,m,K st len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{1} * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) & len b_{2} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{2} * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b_{2} * (i,j) = M * (i,j) ) ) ) holds

b_{1} = b_{2}

end;
let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

func ScalarXLine (M,l,a) -> Matrix of n,m,K means :Def2: :: MATRIX12:def 2

( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies it * (i,j) = a * (M * (l,j)) ) & ( i <> l implies it * (i,j) = M * (i,j) ) ) ) );

existence ( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies it * (i,j) = a * (M * (l,j)) ) & ( i <> l implies it * (i,j) = M * (i,j) ) ) ) );

ex b

( len b

( ( i = l implies b

proof end;

uniqueness for b

( ( i = l implies b

( ( i = l implies b

b

proof end;

:: deftheorem Def2 defines ScalarXLine MATRIX12:def 2 :

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l being Nat

for a being Element of K

for b_{7} being Matrix of n,m,K holds

( b_{7} = ScalarXLine (M,l,a) iff ( len b_{7} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{7} * (i,j) = a * (M * (l,j)) ) & ( i <> l implies b_{7} * (i,j) = M * (i,j) ) ) ) ) );

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l being Nat

for a being Element of K

for b

( b

( ( i = l implies b

theorem Th4: :: MATRIX12:4

for l, n, m, i being Nat

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds

( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in dom M & i in dom M & M1 = ScalarXLine (M,l,a) holds

( ( i = l implies Line (M1,i) = a * (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )

proof end;

Lm3: for j, k, l, n, m, i being Nat

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K

for pK, qK being FinSequence of K st i in Seg n & j in Seg (width M) & k in dom M & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,l,((a * qK) + pK)) holds

( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )

proof end;

definition

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

assume A1: k in dom M ;

ex b_{1} being Matrix of n,m,K st

( len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{1} * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) )

for b_{1}, b_{2} being Matrix of n,m,K st len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{1} * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) & len b_{2} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{2} * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b_{2} * (i,j) = M * (i,j) ) ) ) holds

b_{1} = b_{2}

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

assume A1: k in dom M ;

func RlineXScalar (M,l,k,a) -> Matrix of n,m,K means :Def3: :: MATRIX12:def 3

( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies it * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies it * (i,j) = M * (i,j) ) ) ) );

existence ( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies it * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies it * (i,j) = M * (i,j) ) ) ) );

ex b

( len b

( ( i = l implies b

proof end;

uniqueness for b

( ( i = l implies b

( ( i = l implies b

b

proof end;

:: deftheorem Def3 defines RlineXScalar MATRIX12:def 3 :

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat

for a being Element of K st k in dom M holds

for b_{8} being Matrix of n,m,K holds

( b_{8} = RlineXScalar (M,l,k,a) iff ( len b_{8} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( i = l implies b_{8} * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies b_{8} * (i,j) = M * (i,j) ) ) ) ) );

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat

for a being Element of K st k in dom M holds

for b

( b

( ( i = l implies b

theorem Th5: :: MATRIX12:5

for k, l, n, m, i being Nat

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds

( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds

( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )

proof end;

notation

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

synonym ILine (M,l,k) for InterchangeLine (M,l,k);

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

synonym ILine (M,l,k) for InterchangeLine (M,l,k);

notation

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

synonym SXLine (M,l,a) for ScalarXLine (M,l,a);

end;
let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

synonym SXLine (M,l,a) for ScalarXLine (M,l,a);

notation

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

synonym RLineXS (M,l,k,a) for RlineXScalar (M,l,k,a);

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

synonym RLineXS (M,l,k,a) for RlineXScalar (M,l,k,a);

theorem Th6: :: MATRIX12:6

for k, l, n being Nat

for K being Field

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds

(ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k)

for K being Field

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds

(ILine ((1. (K,n)),l,k)) * A = ILine (A,l,k)

proof end;

theorem Th7: :: MATRIX12:7

for n being Nat

for K being Field

for l being Nat

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) holds

(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)

for K being Field

for l being Nat

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) holds

(SXLine ((1. (K,n)),l,a)) * A = SXLine (A,l,a)

proof end;

theorem Th8: :: MATRIX12:8

for k, l, n being Nat

for K being Field

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds

(RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)

for K being Field

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds

(RLineXS ((1. (K,n)),l,k,a)) * A = RLineXS (A,l,k,a)

proof end;

theorem :: MATRIX12:10

for k, l, n, m being Nat

for K being Field

for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l)

for K being Field

for M being Matrix of n,m,K holds ILine (M,l,k) = ILine (M,k,l)

proof end;

theorem Th11: :: MATRIX12:11

for k, l, n, m being Nat

for K being Field

for M being Matrix of n,m,K st l in dom M & k in dom M holds

ILine ((ILine (M,l,k)),l,k) = M

for K being Field

for M being Matrix of n,m,K st l in dom M & k in dom M holds

ILine ((ILine (M,l,k)),l,k) = M

proof end;

theorem Th12: :: MATRIX12:12

for k, l, n being Nat

for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds

( ILine ((1. (K,n)),l,k) is invertible & (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) )

for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) holds

( ILine ((1. (K,n)),l,k) is invertible & (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) )

proof end;

Lm4: for n being Nat

for K being Field

for i, j, l, k being Nat

for a being Element of K st [i,j] in Indices (1. (K,n)) & l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l holds

(1. (K,n)) * (i,j) = (RLineXS ((RLineXS ((1. (K,n)),l,k,(- a))),l,k,a)) * (i,j)

proof end;

theorem Th13: :: MATRIX12:13

for k, l, n being Nat

for K being Field

for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l holds

( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) )

for K being Field

for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l holds

( RLineXS ((1. (K,n)),l,k,a) is invertible & (RLineXS ((1. (K,n)),l,k,a)) ~ = RLineXS ((1. (K,n)),l,k,(- a)) )

proof end;

theorem Th14: :: MATRIX12:14

for l, n being Nat

for K being Field

for a being Element of K st l in dom (1. (K,n)) & a <> 0. K holds

( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) )

for K being Field

for a being Element of K st l in dom (1. (K,n)) & a <> 0. K holds

( SXLine ((1. (K,n)),l,a) is invertible & (SXLine ((1. (K,n)),l,a)) ~ = SXLine ((1. (K,n)),l,(a ")) )

proof end;

definition

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

assume that

A1: l in Seg (width M) and

A2: k in Seg (width M) and

A3: n > 0 and

A4: m > 0 ;

ex b_{1} being Matrix of n,m,K st

( len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{1} * (i,j) = M * (i,k) ) & ( j = k implies b_{1} * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b_{1} * (i,j) = M * (i,j) ) ) ) )

for b_{1}, b_{2} being Matrix of n,m,K st len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{1} * (i,j) = M * (i,k) ) & ( j = k implies b_{1} * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b_{1} * (i,j) = M * (i,j) ) ) ) & len b_{2} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{2} * (i,j) = M * (i,k) ) & ( j = k implies b_{2} * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b_{2} * (i,j) = M * (i,j) ) ) ) holds

b_{1} = b_{2}

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

assume that

A1: l in Seg (width M) and

A2: k in Seg (width M) and

A3: n > 0 and

A4: m > 0 ;

func InterchangeCol (M,l,k) -> Matrix of n,m,K means :Def4: :: MATRIX12:def 4

( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies it * (i,j) = M * (i,k) ) & ( j = k implies it * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies it * (i,j) = M * (i,j) ) ) ) );

existence ( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies it * (i,j) = M * (i,k) ) & ( j = k implies it * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies it * (i,j) = M * (i,j) ) ) ) );

ex b

( len b

( ( j = l implies b

proof end;

uniqueness for b

( ( j = l implies b

( ( j = l implies b

b

proof end;

:: deftheorem Def4 defines InterchangeCol MATRIX12:def 4 :

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds

for b_{7} being Matrix of n,m,K holds

( b_{7} = InterchangeCol (M,l,k) iff ( len b_{7} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{7} * (i,j) = M * (i,k) ) & ( j = k implies b_{7} * (i,j) = M * (i,l) ) & ( j <> l & j <> k implies b_{7} * (i,j) = M * (i,j) ) ) ) ) );

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds

for b

( b

( ( j = l implies b

definition

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

assume that

A1: l in Seg (width M) and

A2: n > 0 and

A3: m > 0 ;

ex b_{1} being Matrix of n,m,K st

( len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{1} * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) )

for b_{1}, b_{2} being Matrix of n,m,K st len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{1} * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) & len b_{2} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{2} * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b_{2} * (i,j) = M * (i,j) ) ) ) holds

b_{1} = b_{2}

end;
let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

assume that

A1: l in Seg (width M) and

A2: n > 0 and

A3: m > 0 ;

func ScalarXCol (M,l,a) -> Matrix of n,m,K means :Def5: :: MATRIX12:def 5

( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies it * (i,j) = a * (M * (i,l)) ) & ( j <> l implies it * (i,j) = M * (i,j) ) ) ) );

existence ( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies it * (i,j) = a * (M * (i,l)) ) & ( j <> l implies it * (i,j) = M * (i,j) ) ) ) );

ex b

( len b

( ( j = l implies b

proof end;

uniqueness for b

( ( j = l implies b

( ( j = l implies b

b

proof end;

:: deftheorem Def5 defines ScalarXCol MATRIX12:def 5 :

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l being Nat

for a being Element of K st l in Seg (width M) & n > 0 & m > 0 holds

for b_{7} being Matrix of n,m,K holds

( b_{7} = ScalarXCol (M,l,a) iff ( len b_{7} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{7} * (i,j) = a * (M * (i,l)) ) & ( j <> l implies b_{7} * (i,j) = M * (i,j) ) ) ) ) );

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l being Nat

for a being Element of K st l in Seg (width M) & n > 0 & m > 0 holds

for b

( b

( ( j = l implies b

definition

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

assume that

A1: l in Seg (width M) and

A2: k in Seg (width M) and

A3: n > 0 and

A4: m > 0 ;

ex b_{1} being Matrix of n,m,K st

( len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{1} * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) )

for b_{1}, b_{2} being Matrix of n,m,K st len b_{1} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{1} * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b_{1} * (i,j) = M * (i,j) ) ) ) & len b_{2} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{2} * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b_{2} * (i,j) = M * (i,j) ) ) ) holds

b_{1} = b_{2}

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

assume that

A1: l in Seg (width M) and

A2: k in Seg (width M) and

A3: n > 0 and

A4: m > 0 ;

func RcolXScalar (M,l,k,a) -> Matrix of n,m,K means :Def6: :: MATRIX12:def 6

( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies it * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies it * (i,j) = M * (i,j) ) ) ) );

existence ( len it = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies it * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies it * (i,j) = M * (i,j) ) ) ) );

ex b

( len b

( ( j = l implies b

proof end;

uniqueness for b

( ( j = l implies b

( ( j = l implies b

b

proof end;

:: deftheorem Def6 defines RcolXScalar MATRIX12:def 6 :

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat

for a being Element of K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds

for b_{8} being Matrix of n,m,K holds

( b_{8} = RcolXScalar (M,l,k,a) iff ( len b_{8} = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds

( ( j = l implies b_{8} * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies b_{8} * (i,j) = M * (i,j) ) ) ) ) );

for n, m being Nat

for K being Field

for M being Matrix of n,m,K

for l, k being Nat

for a being Element of K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 holds

for b

( b

( ( j = l implies b

notation

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

synonym ICol (M,l,k) for InterchangeCol (M,l,k);

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

synonym ICol (M,l,k) for InterchangeCol (M,l,k);

notation

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

synonym SXCol (M,l,a) for ScalarXCol (M,l,a);

end;
let K be Field;

let M be Matrix of n,m,K;

let l be Nat;

let a be Element of K;

synonym SXCol (M,l,a) for ScalarXCol (M,l,a);

notation

let n, m be Nat;

let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

synonym RColXS (M,l,k,a) for RcolXScalar (M,l,k,a);

end;
let K be Field;

let M be Matrix of n,m,K;

let l, k be Nat;

let a be Element of K;

synonym RColXS (M,l,k,a) for RcolXScalar (M,l,k,a);

theorem Th15: :: MATRIX12:15

for k, l, n, m being Nat

for K being Field

for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds

(ILine (M1,l,k)) @ = ICol (M,l,k)

for K being Field

for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds

(ILine (M1,l,k)) @ = ICol (M,l,k)

proof end;

theorem Th16: :: MATRIX12:16

for l, n, m being Nat

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds

(SXLine (M1,l,a)) @ = SXCol (M,l,a)

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds

(SXLine (M1,l,a)) @ = SXCol (M,l,a)

proof end;

theorem Th17: :: MATRIX12:17

for k, l, n, m being Nat

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds

(RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)

for K being Field

for a being Element of K

for M, M1 being Matrix of n,m,K st l in Seg (width M) & k in Seg (width M) & n > 0 & m > 0 & M1 = M @ holds

(RLineXS (M1,l,k,a)) @ = RColXS (M,l,k,a)

proof end;

theorem :: MATRIX12:18

for k, l, n being Nat

for K being Field

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds

A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k)

for K being Field

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds

A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k)

proof end;

theorem :: MATRIX12:19

for l, n being Nat

for K being Field

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) & n > 0 holds

A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a)

for K being Field

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) & n > 0 holds

A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a)

proof end;

theorem :: MATRIX12:20

for k, l, n being Nat

for K being Field

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds

A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)

for K being Field

for a being Element of K

for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds

A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)

proof end;

theorem :: MATRIX12:21

for k, l, n being Nat

for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds

(ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k)

for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds

(ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k)

proof end;

theorem :: MATRIX12:22

for k, l, n being Nat

for K being Field

for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 holds

(RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a))

for K being Field

for a being Element of K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & k <> l & n > 0 holds

(RColXS ((1. (K,n)),l,k,a)) ~ = RColXS ((1. (K,n)),l,k,(- a))

proof end;

theorem :: MATRIX12:23

for l, n being Nat

for K being Field

for a being Element of K st l in dom (1. (K,n)) & a <> 0. K & n > 0 holds

(SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a "))

for K being Field

for a being Element of K st l in dom (1. (K,n)) & a <> 0. K & n > 0 holds

(SXCol ((1. (K,n)),l,a)) ~ = SXCol ((1. (K,n)),l,(a "))

proof end;