:: MATRIX_3 semantic presentation

Lemma1: for b₁, b₂ being Nat st b₁ = b₁ + b₂ holds
b₂ = 0
by XCMPLX_1:3;

definition

let c₁ be Field;
let c₂, c₃ be Nat;
func 0. c₁,c₂,c₃ -> Matrix of a₂,a₃,a₁ equals :: MATRIX_3:def 1
a₂ |-> (a₃ |-> (0. a₁));
coherence by MATRIX_1:10;

end;

:: deftheorem Def1 defines 0. MATRIX_3:def 1 :

definition

let c₁ be Field;
let c₂ be Matrix of c₁;
func - c₂ -> Matrix of a₁ means :Def2: :: MATRIX_3:def 2
( len a₃ = len a₂ & width a₃ = width a₂ & ( for b₁, b₂ being Nat st [b₁,b₂] in Indices a₂ holds
a₃ * b₁,b₂ = - (a₂ * b₁,b₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines - MATRIX_3:def 2 :

definition

let c₁ be Field;
let c₂, c₃ be Matrix of c₁;
func c₂ + c₃ -> Matrix of a₁ means :Def3: :: MATRIX_3:def 3
( len a₄ = len a₂ & width a₄ = width a₂ & ( for b₁, b₂ being Nat st [b₁,b₂] in Indices a₂ holds
a₄ * b₁,b₂ = (a₂ * b₁,b₂) + (a₃ * b₁,b₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines + MATRIX_3:def 3 :

theorem Th1: :: MATRIX_3:1

canceled;

theorem Th2: :: MATRIX_3:2

canceled;

theorem Th3: :: MATRIX_3:3

for b₁, b₂ being Nat
for b₃ being Field
for b₄, b₅ being Nat st [b₄,b₅] in Indices (0. b₃,b₁,b₂) holds
(0. b₃,b₁,b₂) * b₄,b₅ = 0. b₃

proof end;

theorem Th4: :: MATRIX_3:4

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st len b₂ = len b₃ & width b₂ = width b₃ holds
b₂ + b₃ = b₃ + b₂

proof end;

theorem Th5: :: MATRIX_3:5

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st len b₂ = len b₃ & len b₂ = len b₄ & width b₂ = width b₃ & width b₂ = width b₄ holds
(b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th6: :: MATRIX_3:6

for b₁, b₂ being Nat
for b₃ being Field
for b₄ being Matrix of b₁,b₂,b₃ holds b₄ + (0. b₃,b₁,b₂) = b₄

proof end;

theorem Th7: :: MATRIX_3:7

for b₁, b₂ being Nat
for b₃ being Field
for b₄ being Matrix of b₁,b₂,b₃ holds b₄ + (- b₄) = 0. b₃,b₁,b₂

proof end;

definition

let c₁ be Field;
let c₂, c₃ be Matrix of c₁;
assume E5: width c₂ = len c₃ ;
func c₂ * c₃ -> Matrix of a₁ means :Def4: :: MATRIX_3:def 4
( len a₄ = len a₂ & width a₄ = width a₃ & ( for b₁, b₂ being Nat st [b₁,b₂] in Indices a₄ holds
a₄ * b₁,b₂ = (Line a₂,b₁) "*" (Col a₃,b₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines * MATRIX_3:def 4 :

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Field;
let c₅ be Matrix of c₁,c₂,c₄;
let c₆ be Matrix of width c₅,c₃,c₄;
redefine func * as c₅ * c₆ -> Matrix of len a₅, width a₆,a₄;
coherence

proof end;

end;

definition

let c₁ be Field;
let c₂ be Matrix of c₁;
let c₃ be Element of c₁;
func c₃ * c₂ -> Matrix of a₁ means :: MATRIX_3:def 5
( len a₄ = len a₂ & width a₄ = width a₂ & ( for b₁, b₂ being Nat st [b₁,b₂] in Indices a₂ holds
a₄ * b₁,b₂ = a₃ * (a₂ * b₁,b₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines * MATRIX_3:def 5 :

definition

let c₁ be Field;
let c₂ be Matrix of c₁;
let c₃ be Element of c₁;
func c₂ * c₃ -> Matrix of a₁ equals :: MATRIX_3:def 6
a₃ * a₂;
coherence ;

end;

:: deftheorem Def6 defines * MATRIX_3:def 6 :

theorem Th8: :: MATRIX_3:8

for b₁ being Field
for b₂, b₃ being FinSequence of b₁ st len b₂ = len b₃ holds
( len (mlt b₂,b₃) = len b₂ & len (mlt b₂,b₃) = len b₃ )

proof end;

theorem Th9: :: MATRIX_3:9

for b₁ being Nat
for b₂ being Field
for b₃, b₄ being Nat st [b₃,b₄] in Indices (1. b₂,b₁) & b₄ = b₃ holds
(Line (1. b₂,b₁),b₃) . b₄ = 1. b₂

proof end;

theorem Th10: :: MATRIX_3:10

for b₁ being Nat
for b₂ being Field
for b₃, b₄ being Nat st [b₃,b₄] in Indices (1. b₂,b₁) & b₄ <> b₃ holds
(Line (1. b₂,b₁),b₃) . b₄ = 0. b₂

proof end;

theorem Th11: :: MATRIX_3:11

for b₁ being Nat
for b₂ being Field
for b₃, b₄ being Nat st [b₃,b₄] in Indices (1. b₂,b₁) & b₃ = b₄ holds
(Col (1. b₂,b₁),b₄) . b₃ = 1. b₂

proof end;

theorem Th12: :: MATRIX_3:12

for b₁ being Nat
for b₂ being Field
for b₃, b₄ being Nat st [b₃,b₄] in Indices (1. b₂,b₁) & b₃ <> b₄ holds
(Col (1. b₂,b₁),b₄) . b₃ = 0. b₂

proof end;

Lemma6: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of b₁ st ( for b₃ being Nat st b₃ in dom b₂ holds
b₂ . b₃ = 0. b₁ ) holds
Sum b₂ = 0. b₁

proof end;

theorem Th13: :: MATRIX_3:13

for b₁ being Nat
for b₂ being non empty add-associative right_zeroed right_complementable LoopStr holds Sum (b₁ |-> (0. b₂)) = 0. b₂

proof end;

theorem Th14: :: MATRIX_3:14

for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂ being FinSequence of b₁
for b₃ being Nat st b₃ in dom b₂ & ( for b₄ being Nat st b₄ in dom b₂ & b₄ <> b₃ holds
b₂ . b₄ = 0. b₁ ) holds
Sum b₂ = b₂ . b₃

proof end;

theorem Th15: :: MATRIX_3:15

for b₁ being Field
for b₂, b₃ being FinSequence of b₁ holds len (mlt b₂,b₃) = min (len b₂),(len b₃)

proof end;

theorem Th16: :: MATRIX_3:16

for b₁ being Field
for b₂, b₃ being FinSequence of b₁
for b₄ being Nat st b₄ in dom b₂ & b₂ . b₄ = 1. b₁ & ( for b₅ being Nat st b₅ in dom b₂ & b₅ <> b₄ holds
b₂ . b₅ = 0. b₁ ) holds
for b₅ being Nat st b₅ in dom (mlt b₂,b₃) holds
( ( b₄ = b₅ implies (mlt b₂,b₃) . b₅ = b₃ . b₄ ) & ( b₄ <> b₅ implies (mlt b₂,b₃) . b₅ = 0. b₁ ) )

proof end;

theorem Th17: :: MATRIX_3:17

for b₁ being Nat
for b₂ being Field
for b₃, b₄ being Nat st [b₃,b₄] in Indices (1. b₂,b₁) holds
( ( b₃ = b₄ implies (Line (1. b₂,b₁),b₃) . b₄ = 1. b₂ ) & ( b₃ <> b₄ implies (Line (1. b₂,b₁),b₃) . b₄ = 0. b₂ ) )

proof end;

theorem Th18: :: MATRIX_3:18

for b₁ being Nat
for b₂ being Field
for b₃, b₄ being Nat st [b₃,b₄] in Indices (1. b₂,b₁) holds
( ( b₃ = b₄ implies (Col (1. b₂,b₁),b₄) . b₃ = 1. b₂ ) & ( b₃ <> b₄ implies (Col (1. b₂,b₁),b₄) . b₃ = 0. b₂ ) )

proof end;

theorem Th19: :: MATRIX_3:19

for b₁ being Field
for b₂, b₃ being FinSequence of b₁
for b₄ being Nat st b₄ in dom b₂ & b₄ in dom b₃ & b₂ . b₄ = 1. b₁ & ( for b₅ being Nat st b₅ in dom b₂ & b₅ <> b₄ holds
b₂ . b₅ = 0. b₁ ) holds
Sum (mlt b₂,b₃) = b₃ . b₄

proof end;

theorem Th20: :: MATRIX_3:20

for b₁ being Nat
for b₂ being Field
for b₃ being Matrix of b₁,b₂ holds (1. b₂,b₁) * b₃ = b₃

proof end;

theorem Th21: :: MATRIX_3:21

for b₁ being Nat
for b₂ being Field
for b₃ being Matrix of b₁,b₂ holds b₃ * (1. b₂,b₁) = b₃

proof end;

theorem Th22: :: MATRIX_3:22

for b₁ being Field
for b₂, b₃ being Element of b₁ holds <*<*b₂*>*> * <*<*b₃*>*> = <*<*(b₂ * b₃)*>*>

proof end;

theorem Th23: :: MATRIX_3:23

for b₁ being Field
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ holds (b₂,b₄ ][ b₆,b₈) * (b₃,b₅ ][ b₇,b₉) = ((b₂ * b₃) + (b₄ * b₇)),((b₂ * b₅) + (b₄ * b₉)) ][ ((b₆ * b₃) + (b₈ * b₇)),((b₆ * b₅) + (b₈ * b₉))

proof end;

theorem Th24: :: MATRIX_3:24

for b₁ being Field
for b₂, b₃ being Matrix of b₁ st width b₂ = len b₃ & width b₃ <> 0 holds
(b₂ * b₃) @ = (b₃ @ ) * (b₂ @ )

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Element of Fin c₁;
let c₄ be Element of Fin c₂;
redefine func [: as [:c₃,c₄:] -> Element of Fin [:a₁,a₂:];
coherence

proof end;

end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be BinOp of c₃;
let c₅ be Function of c₁,c₃;
let c₆ be Function of c₂,c₃;
redefine func * as c₄ * c₅,c₆ -> Function of [:a₁,a₂:],a₃;
coherence by FINSEQOP:84;

end;

theorem Th25: :: MATRIX_3:25

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being BinOp of b₃
for b₆ being Function of b₁,b₃
for b₇ being Function of b₂,b₃
for b₈ being Element of Fin b₁
for b₉ being Element of Fin b₂ st b₄ is commutative & b₄ is associative & ( [:b₉,b₈:] <> {} or b₄ has_a_unity ) & b₅ is commutative holds
b₄ $$ [:b₈,b₉:],(b₅ * b₆,b₇) = b₄ $$ [:b₉,b₈:],(b₅ * b₇,b₆)

proof end;

theorem Th26: :: MATRIX_3:26

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being BinOp of b₁
for b₆ being Function of b₂,b₁
for b₇ being Function of b₃,b₁ st b₄ is commutative & b₄ is associative & b₄ has_a_unity holds
for b₈ being Element of b₂
for b₉ being Element of b₃ holds b₄ $$ [:{b₈},{b₉}:],(b₅ * b₆,b₇) = b₄ $$ {b₈},(b₅ [:] b₆,(b₄ $$ {b₉},b₇))

proof end;

theorem Th27: :: MATRIX_3:27

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being BinOp of b₁
for b₆ being Function of b₂,b₁
for b₇ being Function of b₃,b₁
for b₈ being Element of Fin b₂
for b₉ being Element of Fin b₃ st b₄ is commutative & b₄ is associative & b₄ has_a_unity & b₄ has_an_inverseOp & b₅ is_distributive_wrt b₄ holds
for b₁₀ being Element of b₂ holds b₄ $$ [:{b₁₀},b₉:],(b₅ * b₆,b₇) = b₄ $$ {b₁₀},(b₅ [:] b₆,(b₄ $$ b₉,b₇))

proof end;

theorem Th28: :: MATRIX_3:28

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being BinOp of b₁
for b₆ being Function of b₂,b₁
for b₇ being Function of b₃,b₁
for b₈ being Element of Fin b₂
for b₉ being Element of Fin b₃ st b₄ has_a_unity & b₄ is commutative & b₄ is associative & b₄ has_an_inverseOp & b₅ is_distributive_wrt b₄ holds
b₄ $$ [:b₈,b₉:],(b₅ * b₆,b₇) = b₄ $$ b₈,(b₅ [:] b₆,(b₄ $$ b₉,b₇))

proof end;

theorem Th29: :: MATRIX_3:29

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being BinOp of b₁
for b₆ being Function of b₂,b₁
for b₇ being Function of b₃,b₁ st b₄ is commutative & b₄ is associative & b₄ has_a_unity & b₅ is commutative holds
for b₈ being Element of b₂
for b₉ being Element of b₃ holds b₄ $$ [:{b₈},{b₉}:],(b₅ * b₆,b₇) = b₄ $$ {b₉},(b₅ [;] (b₄ $$ {b₈},b₆),b₇)

proof end;

theorem Th30: :: MATRIX_3:30

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being BinOp of b₁
for b₆ being Function of b₂,b₁
for b₇ being Function of b₃,b₁
for b₈ being Element of Fin b₂
for b₉ being Element of Fin b₃ st b₄ has_a_unity & b₄ is commutative & b₄ is associative & b₄ has_an_inverseOp & b₅ is_distributive_wrt b₄ & b₅ is commutative holds
b₄ $$ [:b₈,b₉:],(b₅ * b₆,b₇) = b₄ $$ b₉,(b₅ [;] (b₄ $$ b₈,b₆),b₇)

proof end;

theorem Th31: :: MATRIX_3:31

for b₁, b₂, b₃ being non empty set
for b₄ being BinOp of b₁
for b₅ being Function of [:b₂,b₃:],b₁
for b₆ being Function of b₂,b₁
for b₇ being Element of Fin b₃ st b₄ has_a_unity & b₄ is commutative & b₄ is associative & b₄ has_an_inverseOp holds
for b₈ being Element of b₂ st ( for b₉ being Element of b₂ holds b₆ . b₉ = b₄ $$ b₇,((curry b₅) . b₉) ) holds
b₄ $$ [:{b₈},b₇:],b₅ = b₄ $$ {b₈},b₆

proof end;

theorem Th32: :: MATRIX_3:32

for b₁, b₂, b₃ being non empty set
for b₄ being BinOp of b₁
for b₅ being Function of [:b₂,b₃:],b₁
for b₆ being Function of b₂,b₁
for b₇ being Element of Fin b₂
for b₈ being Element of Fin b₃ st ( for b₉ being Element of b₂ holds b₆ . b₉ = b₄ $$ b₈,((curry b₅) . b₉) ) & b₄ has_a_unity & b₄ is commutative & b₄ is associative & b₄ has_an_inverseOp holds
b₄ $$ [:b₇,b₈:],b₅ = b₄ $$ b₇,b₆

proof end;

theorem Th33: :: MATRIX_3:33

for b₁, b₂, b₃ being non empty set
for b₄ being BinOp of b₁
for b₅ being Function of [:b₂,b₃:],b₁
for b₆ being Function of b₃,b₁
for b₇ being Element of Fin b₂ st b₄ has_a_unity & b₄ is commutative & b₄ is associative & b₄ has_an_inverseOp holds
for b₈ being Element of b₃ st ( for b₉ being Element of b₃ holds b₆ . b₉ = b₄ $$ b₇,((curry' b₅) . b₉) ) holds
b₄ $$ [:b₇,{b₈}:],b₅ = b₄ $$ {b₈},b₆

proof end;

theorem Th34: :: MATRIX_3:34

for b₁, b₂, b₃ being non empty set
for b₄ being BinOp of b₁
for b₅ being Function of [:b₂,b₃:],b₁
for b₆ being Function of b₃,b₁
for b₇ being Element of Fin b₂
for b₈ being Element of Fin b₃ st ( for b₉ being Element of b₃ holds b₆ . b₉ = b₄ $$ b₇,((curry' b₅) . b₉) ) & b₄ has_a_unity & b₄ is commutative & b₄ is associative & b₄ has_an_inverseOp holds
b₄ $$ [:b₇,b₈:],b₅ = b₄ $$ b₈,b₆

proof end;

theorem Th35: :: MATRIX_3:35

for b₁ being Field
for b₂, b₃, b₄ being Matrix of b₁ st width b₂ = len b₃ & width b₃ = len b₄ holds
(b₂ * b₃) * b₄ = b₂ * (b₃ * b₄)

proof end;

definition

let c₁ be Nat;
let c₂ be Field;
let c₃ be Matrix of c₁,c₂;
let c₄ be Element of Permutations c₁;
func Path_matrix c₄,c₃ -> FinSequence of a₂ means :Def7: :: MATRIX_3:def 7
( len a₅ = a₁ & ( for b₁, b₂ being Nat st b₁ in dom a₅ & b₂ = a₄ . b₁ holds
a₅ . b₁ = a₃ * b₁,b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Path_matrix MATRIX_3:def 7 :

definition

let c₁ be Nat;
let c₂ be Field;
let c₃ be Matrix of c₁,c₂;
func Path_product c₃ -> Function of Permutations a₁,the carrier of a₂ means :Def8: :: MATRIX_3:def 8
for b₁ being Element of Permutations a₁ holds a₄ . b₁ = - (the mult of a₂ $$ (Path_matrix b₁,a₃)),b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Path_product MATRIX_3:def 8 :

definition

let c₁ be Nat;
let c₂ be Field;
let c₃ be Matrix of c₁,c₂;
func Det c₃ -> Element of a₂ equals :: MATRIX_3:def 9
the add of a₂ $$ (FinOmega (Permutations a₁)),(Path_product a₃);
coherence ;

end;

:: deftheorem Def9 defines Det MATRIX_3:def 9 :

theorem Th36: :: MATRIX_3:36

for b₁ being Field
for b₂ being Element of b₁ holds Det <*<*b₂*>*> = b₂

proof end;

definition

let c₁ be Nat;
let c₂ be Field;
let c₃ be Matrix of c₁,c₂;
func diagonal_of_Matrix c₃ -> FinSequence of a₂ means :: MATRIX_3:def 10
( len a₄ = a₁ & ( for b₁ being Nat st b₁ in Seg a₁ holds
a₄ . b₁ = a₃ * b₁,b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines diagonal_of_Matrix MATRIX_3:def 10 :