:: by Yatsuka Nakamura

::

:: Received January 4, 2006

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

theorem Th5: :: MATRIX_7:5

for D being non empty set

for f being FinSequence of D

for k2 being Nat st 1 <= k2 & k2 < len f holds

f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))

for f being FinSequence of D

for k2 being Nat st 1 <= k2 & k2 < len f holds

f = (mid (f,1,k2)) ^ (mid (f,(k2 + 1),(len f)))

proof end;

theorem Th6: :: MATRIX_7:6

for D being non empty set

for f being FinSequence of D st 2 <= len f holds

f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))

for f being FinSequence of D st 2 <= len f holds

f = (f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f)))

proof end;

theorem Th7: :: MATRIX_7:7

for D being non empty set

for f being FinSequence of D st 1 <= len f holds

f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))

for f being FinSequence of D st 1 <= len f holds

f = (f | ((len f) -' 1)) ^ (mid (f,(len f),(len f)))

proof end;

Lm1: <*1,2*> <> <*2,1*>

by FINSEQ_1:77;

theorem Th8: :: MATRIX_7:8

for a being Element of (Group_of_Perm 2) st ex q being Element of Permutations 2 st

( q = a & q is being_transposition ) holds

a = <*2,1*>

( q = a & q is being_transposition ) holds

a = <*2,1*>

proof end;

theorem :: MATRIX_7:9

for n being Nat

for a, b being Element of (Group_of_Perm n)

for pa, pb being Element of Permutations n st a = pa & b = pb holds

a * b = pb * pa by MATRIX_1:def 13;

for a, b being Element of (Group_of_Perm n)

for pa, pb being Element of Permutations n st a = pa & b = pb holds

a * b = pb * pa by MATRIX_1:def 13;

theorem Th10: :: MATRIX_7:10

for a, b being Element of (Group_of_Perm 2) st ex p being Element of Permutations 2 st

( p = a & p is being_transposition ) & ex q being Element of Permutations 2 st

( q = b & q is being_transposition ) holds

a * b = <*1,2*>

( p = a & p is being_transposition ) & ex q being Element of Permutations 2 st

( q = b & q is being_transposition ) holds

a * b = <*1,2*>

proof end;

theorem Th11: :: MATRIX_7:11

for l being FinSequence of (Group_of_Perm 2) st (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds

ex q being Element of Permutations 2 st

( l . i = q & q is being_transposition ) ) holds

Product l = <*1,2*>

ex q being Element of Permutations 2 st

( l . i = q & q is being_transposition ) ) holds

Product l = <*1,2*>

proof end;

theorem :: MATRIX_7:12

for K being Field

for M being Matrix of 2,K holds Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))

for M being Matrix of 2,K holds Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))

proof end;

definition

let n be Nat;

let K be commutative Ring;

let M be Matrix of n,K;

let a be Element of K;

:: original: *

redefine func a * M -> Matrix of n,K;

coherence

a * M is Matrix of n,K

end;
let K be commutative Ring;

let M be Matrix of n,K;

let a be Element of K;

:: original: *

redefine func a * M -> Matrix of n,K;

coherence

a * M is Matrix of n,K

proof end;

theorem Th14: :: MATRIX_7:14

for K being Ring

for n being Nat

for p being Element of Permutations n

for i being Nat st i in Seg n holds

p . i in Seg n

for n being Nat

for p being Element of Permutations n

for i being Nat st i in Seg n holds

p . i in Seg n

proof end;

definition

let x be object ;

let y be set ;

let a, b be object ;

correctness

coherence

( ( x in y implies a is object ) & ( not x in y implies b is object ) );

consistency

for b_{1} being object holds verum;

;

end;
let y be set ;

let a, b be object ;

correctness

coherence

( ( x in y implies a is object ) & ( not x in y implies b is object ) );

consistency

for b

;

:: deftheorem Def1 defines IFIN MATRIX_7:def 1 :

for x being object

for y being set

for a, b being object holds

( ( x in y implies IFIN (x,y,a,b) = a ) & ( not x in y implies IFIN (x,y,a,b) = b ) );

for x being object

for y being set

for a, b being object holds

( ( x in y implies IFIN (x,y,a,b) = a ) & ( not x in y implies IFIN (x,y,a,b) = b ) );

definition

let n be Nat;

let K be Field;

let M be Matrix of n,K;

( M is diagonal iff for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

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

end;
let K be Field;

let M be Matrix of n,K;

:: original: diagonal

redefine attr M is diagonal means :: MATRIX_7:def 2

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

M * (i,j) = 0. K;

compatibility redefine attr M is diagonal means :: MATRIX_7:def 2

for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

M * (i,j) = 0. K;

( M is diagonal iff for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

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

proof end;

:: deftheorem defines diagonal MATRIX_7:def 2 :

for n being Nat

for K being Field

for M being Matrix of n,K holds

( M is diagonal iff for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

M * (i,j) = 0. K );

for n being Nat

for K being Field

for M being Matrix of n,K holds

( M is diagonal iff for i, j being Nat st i in Seg n & j in Seg n & i <> j holds

M * (i,j) = 0. K );

theorem :: MATRIX_7:17

for K being Field

for n being Nat

for A being Matrix of n,K st n >= 1 & A is V196(b_{1}) holds

Det A = the multF of K $$ (diagonal_of_Matrix A)

for n being Nat

for A being Matrix of n,K st n >= 1 & A is V196(b

Det A = the multF of K $$ (diagonal_of_Matrix A)

proof end;

definition

let n be Nat;

let p be Element of Permutations n;

:: original: "

redefine func p " -> Element of Permutations n;

coherence

p " is Element of Permutations n by Th18;

end;
let p be Element of Permutations n;

:: original: "

redefine func p " -> Element of Permutations n;

coherence

p " is Element of Permutations n by Th18;

::$CT

theorem :: MATRIX_7:20

for G being Group

for f1, f2 being FinSequence of G holds (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")

for f1, f2 being FinSequence of G holds (Product (f1 ^ f2)) " = ((Product f2) ") * ((Product f1) ")

proof end;

definition

let G be Group;

let f be FinSequence of G;

ex b_{1} being FinSequence of G st

( len b_{1} = len f & ( for i being Nat st i in dom f holds

b_{1} /. i = (f /. i) " ) )

for b_{1}, b_{2} being FinSequence of G st len b_{1} = len f & ( for i being Nat st i in dom f holds

b_{1} /. i = (f /. i) " ) & len b_{2} = len f & ( for i being Nat st i in dom f holds

b_{2} /. i = (f /. i) " ) holds

b_{1} = b_{2}

end;
let f be FinSequence of G;

::$CD

func f " -> FinSequence of G means :Def3: :: MATRIX_7:def 4

( len it = len f & ( for i being Nat st i in dom f holds

it /. i = (f /. i) " ) );

existence ( len it = len f & ( for i being Nat st i in dom f holds

it /. i = (f /. i) " ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines " MATRIX_7:def 4 :

for G being Group

for f, b_{3} being FinSequence of G holds

( b_{3} = f " iff ( len b_{3} = len f & ( for i being Nat st i in dom f holds

b_{3} /. i = (f /. i) " ) ) );

for G being Group

for f, b

( b

b

theorem Th26: :: MATRIX_7:27

for n being Nat

for ITP being Element of Permutations n

for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds

ITP " = ITG "

for ITP being Element of Permutations n

for ITG being Element of (Group_of_Perm n) st ITG = ITP & n >= 1 holds

ITP " = ITG "

proof end;

Lm2: for n being Nat

for IT being Element of Permutations n st IT is even & n >= 1 holds

IT " is even

proof end;

theorem Th27: :: MATRIX_7:28

for n being Nat

for IT being Element of Permutations n st n >= 1 holds

( IT is even iff IT " is even )

for IT being Element of Permutations n st n >= 1 holds

( IT is even iff IT " is even )

proof end;

theorem Th28: :: MATRIX_7:29

for n being Nat

for K being commutative Ring

for p being Element of Permutations n

for x being Element of K st n >= 1 holds

- (x,p) = - (x,(p "))

for K being commutative Ring

for p being Element of Permutations n

for x being Element of K st n >= 1 holds

- (x,p) = - (x,(p "))

proof end;

theorem :: MATRIX_7:30

for K being commutative Ring

for f1, f2 being FinSequence of K holds the multF of K $$ (f1 ^ f2) = ( the multF of K $$ f1) * ( the multF of K $$ f2) by FINSOP_1:5;

for f1, f2 being FinSequence of K holds the multF of K $$ (f1 ^ f2) = ( the multF of K $$ f1) * ( the multF of K $$ f2) by FINSOP_1:5;

theorem Th30: :: MATRIX_7:31

for K being commutative Ring

for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds

the multF of K $$ R1 = the multF of K $$ R2

for R1, R2 being FinSequence of K st R1,R2 are_fiberwise_equipotent holds

the multF of K $$ R1 = the multF of K $$ R2

proof end;

theorem Th31: :: MATRIX_7:32

for n being Nat

for K being commutative Ring

for p being Element of Permutations n

for f, g being FinSequence of K st len f = n & g = f * p holds

f,g are_fiberwise_equipotent

for K being commutative Ring

for p being Element of Permutations n

for f, g being FinSequence of K st len f = n & g = f * p holds

f,g are_fiberwise_equipotent

proof end;

theorem :: MATRIX_7:33

theorem Th33: :: MATRIX_7:34

for n being Nat

for K being Ring

for p being Element of Permutations n

for f being FinSequence of K st n >= 1 & len f = n holds

f * p is FinSequence of K

for K being Ring

for p being Element of Permutations n

for f being FinSequence of K st n >= 1 & len f = n holds

f * p is FinSequence of K

proof end;

theorem Th34: :: MATRIX_7:35

for n being Nat

for K being commutative Ring

for p being Element of Permutations n

for A being Matrix of n,K st n >= 1 holds

Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")

for K being commutative Ring

for p being Element of Permutations n

for A being Matrix of n,K st n >= 1 holds

Path_matrix ((p "),(A @)) = (Path_matrix (p,A)) * (p ")

proof end;

theorem Th35: :: MATRIX_7:36

for n being Nat

for K being commutative Ring

for p being Element of Permutations n

for A being Matrix of n,K st n >= 1 holds

(Path_product (A @)) . (p ") = (Path_product A) . p

for K being commutative Ring

for p being Element of Permutations n

for A being Matrix of n,K st n >= 1 holds

(Path_product (A @)) . (p ") = (Path_product A) . p

proof end;

theorem :: MATRIX_7:37

for n being Nat

for K being commutative Ring

for A being Matrix of n,K st n >= 1 holds

Det A = Det (A @)

for K being commutative Ring

for A being Matrix of n,K st n >= 1 holds

Det A = Det (A @)

proof end;