:: MATRIX_9 semantic presentation
begin
theorem Th1: :: MATRIX_9:1
for a, A being set st a in A holds
{a} in Fin A
proof
let a, A be set ; ::_thesis: ( a in A implies {a} in Fin A )
assume a in A ; ::_thesis: {a} in Fin A
then {a} c= A by ZFMISC_1:31;
hence {a} in Fin A by FINSUB_1:def_5; ::_thesis: verum
end;
registration
let n be Nat;
cluster non empty finite for Element of Fin (Permutations n);
existence
not for b1 being Element of Fin (Permutations n) holds b1 is empty
proof
idseq n in Permutations n by MATRIX_2:def_9;
then {(idseq n)} in Fin (Permutations n) by Th1;
hence not for b1 being Element of Fin (Permutations n) holds b1 is empty ; ::_thesis: verum
end;
end;
scheme :: MATRIX_9:sch 1
NonEmptyFiniteX{ F1() -> Element of NAT , F2() -> non empty Element of Fin (Permutations F1()), P1[ set ] } :
P1[F2()]
provided
A1: for x being Element of Permutations F1() st x in F2() holds
P1[{x}] and
A2: for x being Element of Permutations F1()
for B being non empty Element of Fin (Permutations F1()) st x in F2() & B c= F2() & not x in B & P1[B] holds
P1[B \/ {x}]
proof
defpred S1[ set ] means ( $1 is empty or P1[$1] );
A3: for x, B being set st x in F2() & B c= F2() & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in F2() & B c= F2() & S1[B] implies S1[B \/ {x}] )
assume that
A4: x in F2() and
A5: B c= F2() and
A6: S1[B] ; ::_thesis: S1[B \/ {x}]
A7: F2() c= Permutations F1() by FINSUB_1:def_5;
then reconsider x = x as Element of Permutations F1() by A4;
A8: B c= Permutations F1() by A5, A7, XBOOLE_1:1;
percases ( x in B or ( not B is empty & not x in B ) or B is empty ) ;
supposeA9: x in B ; ::_thesis: S1[B \/ {x}]
then reconsider B = B as non empty Element of Fin (Permutations F1()) by A5, A8, FINSUB_1:def_5;
{x} c= B by A9, ZFMISC_1:31;
hence S1[B \/ {x}] by A6, XBOOLE_1:12; ::_thesis: verum
end;
supposeA10: ( not B is empty & not x in B ) ; ::_thesis: S1[B \/ {x}]
then reconsider B = B as non empty Element of Fin (Permutations F1()) by A5, A8, FINSUB_1:def_5;
P1[B \/ {x}] by A2, A4, A5, A6, A10;
hence S1[B \/ {x}] ; ::_thesis: verum
end;
suppose B is empty ; ::_thesis: S1[B \/ {x}]
then P1[B \/ {x}] by A1, A4;
hence S1[B \/ {x}] ; ::_thesis: verum
end;
end;
end;
A11: S1[ {} ] ;
A12: F2() is finite ;
S1[F2()] from FINSET_1:sch_2(A12, A11, A3);
hence P1[F2()] ; ::_thesis: verum
end;
Lm1: <*1,2*> <> <*2,1*>
by FINSEQ_1:77;
Lm2: <*2,1*> in Permutations 2
by MATRIX_7:3, TARSKI:def_2;
registration
let n be Nat;
cluster Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total finite FinSequence-like for Element of bool [:(Seg n),(Seg n):];
existence
ex b1 being Function of (Seg n),(Seg n) st
( b1 is one-to-one & b1 is FinSequence-like )
proof
take f = id (Seg n); ::_thesis: ( f is one-to-one & f is FinSequence-like )
dom f = Seg n by RELAT_1:45;
hence ( f is one-to-one & f is FinSequence-like ) by FINSEQ_1:def_2; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster id (Seg n) -> FinSequence-like ;
coherence
id (Seg n) is FinSequence-like
proof
dom (id (Seg n)) = Seg n by RELAT_1:45;
hence id (Seg n) is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum
end;
end;
theorem Th2: :: MATRIX_9:2
( (Rev (idseq 2)) . 1 = 2 & (Rev (idseq 2)) . 2 = 1 )
proof
reconsider f = idseq 2 as one-to-one FinSequence-like Function of (Seg 2),(Seg 2) ;
f . 1 = (Rev f) . (len f) by FINSEQ_5:62;
then A1: (idseq 2) . 1 = (Rev (idseq 2)) . 2 by CARD_1:def_7;
f . (len f) = (Rev f) . 1 by FINSEQ_5:62;
then A2: f . 2 = (Rev f) . 1 by CARD_1:def_7;
A3: dom (Rev f) = dom f by FINSEQ_5:57;
then A4: dom (Rev f) = Seg 2 by RELAT_1:45;
then ( 1 in dom f & 2 in dom f ) by A3;
hence ( (Rev (idseq 2)) . 1 = 2 & (Rev (idseq 2)) . 2 = 1 ) by A1, A2, A3, A4, FUNCT_1:18; ::_thesis: verum
end;
theorem Th3: :: MATRIX_9:3
for f being one-to-one Function st dom f = Seg 2 & rng f = Seg 2 & not f = id (Seg 2) holds
f = Rev (id (Seg 2))
proof
let f be one-to-one Function; ::_thesis: ( dom f = Seg 2 & rng f = Seg 2 & not f = id (Seg 2) implies f = Rev (id (Seg 2)) )
A1: dom (idseq 2) = Seg 2 by RELAT_1:45;
assume that
A2: dom f = Seg 2 and
A3: rng f = Seg 2 ; ::_thesis: ( f = id (Seg 2) or f = Rev (id (Seg 2)) )
A4: 1 in dom f by A2;
then f . 1 in rng f by FUNCT_1:3;
then A5: ( f . 1 = 1 or f . 1 = 2 ) by A3, FINSEQ_1:2, TARSKI:def_2;
A6: 2 in dom f by A2;
then f . 2 in rng f by FUNCT_1:3;
then A7: ( f . 2 = 2 or f . 2 = 1 ) by A3, FINSEQ_1:2, TARSKI:def_2;
percases ( ( f . 1 = 1 & f . 2 = 2 ) or ( f . 1 = 2 & f . 2 = 1 ) ) by A4, A5, A6, A7, FUNCT_1:def_4;
supposeA8: ( f . 1 = 1 & f . 2 = 2 ) ; ::_thesis: ( f = id (Seg 2) or f = Rev (id (Seg 2)) )
for x being set st x in Seg 2 holds
f . x = x
proof
let x be set ; ::_thesis: ( x in Seg 2 implies f . x = x )
assume x in Seg 2 ; ::_thesis: f . x = x
then ( x = 1 or x = 2 ) by FINSEQ_1:2, TARSKI:def_2;
hence f . x = x by A8; ::_thesis: verum
end;
hence ( f = id (Seg 2) or f = Rev (id (Seg 2)) ) by A2, FUNCT_1:17; ::_thesis: verum
end;
supposeA9: ( f . 1 = 2 & f . 2 = 1 ) ; ::_thesis: ( f = id (Seg 2) or f = Rev (id (Seg 2)) )
A10: for x being set st x in Seg 2 holds
f . x = (Rev (id (Seg 2))) . x
proof
let x be set ; ::_thesis: ( x in Seg 2 implies f . x = (Rev (id (Seg 2))) . x )
assume x in Seg 2 ; ::_thesis: f . x = (Rev (id (Seg 2))) . x
then ( x = 1 or x = 2 ) by FINSEQ_1:2, TARSKI:def_2;
hence f . x = (Rev (id (Seg 2))) . x by A9, Th2; ::_thesis: verum
end;
dom f = dom (Rev (id (Seg 2))) by A1, A2, FINSEQ_5:57;
hence ( f = id (Seg 2) or f = Rev (id (Seg 2)) ) by A2, A10, FUNCT_1:2; ::_thesis: verum
end;
end;
end;
begin
theorem Th4: :: MATRIX_9:4
for n being Nat holds Rev (idseq n) in Permutations n
proof
let n be Nat; ::_thesis: Rev (idseq n) in Permutations n
reconsider f = idseq n as one-to-one FinSequence-like Function of (Seg n),(Seg n) ;
dom f = dom (Rev f) by FINSEQ_5:57;
then A1: dom (Rev f) = Seg n by RELAT_1:45;
A2: rng (idseq n) = Seg n by FUNCT_2:def_3;
then rng (Rev f) c= Seg n by FINSEQ_5:57;
then reconsider g = Rev f as FinSequence-like Function of (Seg n),(Seg n) by A1, FUNCT_2:2;
rng f = rng (Rev f) by FINSEQ_5:57;
then g is onto by A2, FUNCT_2:def_3;
hence Rev (idseq n) in Permutations n by MATRIX_2:def_9; ::_thesis: verum
end;
theorem Th5: :: MATRIX_9:5
for n being Nat
for f being FinSequence st n <> 0 & f in Permutations n holds
Rev f in Permutations n
proof
let n be Nat; ::_thesis: for f being FinSequence st n <> 0 & f in Permutations n holds
Rev f in Permutations n
let f be FinSequence; ::_thesis: ( n <> 0 & f in Permutations n implies Rev f in Permutations n )
assume that
A1: n <> 0 and
A2: f in Permutations n ; ::_thesis: Rev f in Permutations n
A3: f is Permutation of (Seg n) by A2, MATRIX_2:def_9;
dom f = dom (Rev f) by FINSEQ_5:57;
then A4: dom (Rev f) = Seg n by A1, A3, FUNCT_2:def_1;
A5: rng f = rng (Rev f) by FINSEQ_5:57;
then rng (Rev f) = Seg n by A3, FUNCT_2:def_3;
then reconsider g = Rev f as FinSequence-like Function of (Seg n),(Seg n) by A4, FUNCT_2:2;
rng f = Seg n by A3, FUNCT_2:def_3;
then g is onto by A5, FUNCT_2:def_3;
hence Rev f in Permutations n by A3, MATRIX_2:def_9; ::_thesis: verum
end;
theorem Th6: :: MATRIX_9:6
Permutations 2 = {(idseq 2),(Rev (idseq 2))}
proof
now__::_thesis:_for_p_being_set_st_p_in_Permutations_2_holds_
p_in_{(idseq_2),(Rev_(idseq_2))}
let p be set ; ::_thesis: ( p in Permutations 2 implies p in {(idseq 2),(Rev (idseq 2))} )
assume p in Permutations 2 ; ::_thesis: p in {(idseq 2),(Rev (idseq 2))}
then reconsider q = p as Permutation of (Seg 2) by MATRIX_2:def_9;
A1: rng q = Seg 2 by FUNCT_2:def_3;
A2: dom q = Seg 2 by FUNCT_2:52;
then reconsider q = q as FinSequence by FINSEQ_1:def_2;
( q = idseq 2 or q = Rev (idseq 2) ) by A1, A2, Th3;
hence p in {(idseq 2),(Rev (idseq 2))} by TARSKI:def_2; ::_thesis: verum
end;
then A3: Permutations 2 c= {(idseq 2),(Rev (idseq 2))} by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_{(idseq_2),(Rev_(idseq_2))}_holds_
x_in_Permutations_2
let x be set ; ::_thesis: ( x in {(idseq 2),(Rev (idseq 2))} implies x in Permutations 2 )
assume x in {(idseq 2),(Rev (idseq 2))} ; ::_thesis: x in Permutations 2
then ( x = idseq 2 or x = Rev (idseq 2) ) by TARSKI:def_2;
hence x in Permutations 2 by Th4, MATRIX_2:def_9; ::_thesis: verum
end;
then {(idseq 2),(Rev (idseq 2))} c= Permutations 2 by TARSKI:def_3;
hence Permutations 2 = {(idseq 2),(Rev (idseq 2))} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func PPath_product M -> Function of (Permutations n), the carrier of K means :Def1: :: MATRIX_9:def 1
for p being Element of Permutations n holds it . p = the multF of K $$ (Path_matrix (p,M));
existence
ex b1 being Function of (Permutations n), the carrier of K st
for p being Element of Permutations n holds b1 . p = the multF of K $$ (Path_matrix (p,M))
proof
deffunc H1( Element of Permutations n) -> Element of the carrier of K = the multF of K $$ (Path_matrix ($1,M));
consider f being Function of (Permutations n), the carrier of K such that
A1: for p being Element of Permutations n holds f . p = H1(p) from FUNCT_2:sch_4();
take f ; ::_thesis: for p being Element of Permutations n holds f . p = the multF of K $$ (Path_matrix (p,M))
thus for p being Element of Permutations n holds f . p = the multF of K $$ (Path_matrix (p,M)) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (Permutations n), the carrier of K st ( for p being Element of Permutations n holds b1 . p = the multF of K $$ (Path_matrix (p,M)) ) & ( for p being Element of Permutations n holds b2 . p = the multF of K $$ (Path_matrix (p,M)) ) holds
b1 = b2
proof
let f1, f2 be Function of (Permutations n), the carrier of K; ::_thesis: ( ( for p being Element of Permutations n holds f1 . p = the multF of K $$ (Path_matrix (p,M)) ) & ( for p being Element of Permutations n holds f2 . p = the multF of K $$ (Path_matrix (p,M)) ) implies f1 = f2 )
assume that
A2: for p being Element of Permutations n holds f1 . p = the multF of K $$ (Path_matrix (p,M)) and
A3: for p being Element of Permutations n holds f2 . p = the multF of K $$ (Path_matrix (p,M)) ; ::_thesis: f1 = f2
now__::_thesis:_for_p_being_Element_of_Permutations_n_holds_f1_._p_=_f2_._p
let p be Element of Permutations n; ::_thesis: f1 . p = f2 . p
f1 . p = the multF of K $$ (Path_matrix (p,M)) by A2;
hence f1 . p = f2 . p by A3; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines PPath_product MATRIX_9:def_1_:_
for n being Nat
for K being Field
for M being Matrix of n,K
for b4 being Function of (Permutations n), the carrier of K holds
( b4 = PPath_product M iff for p being Element of Permutations n holds b4 . p = the multF of K $$ (Path_matrix (p,M)) );
definition
let n be Nat;
let K be Field;
let M be Matrix of n,K;
func Per M -> Element of K equals :: MATRIX_9:def 2
the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M));
coherence
the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) is Element of K ;
end;
:: deftheorem defines Per MATRIX_9:def_2_:_
for n being Nat
for K being Field
for M being Matrix of n,K holds Per M = the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M));
theorem :: MATRIX_9:7
for K being Field
for a being Element of K holds Per <*<*a*>*> = a
proof
let K be Field; ::_thesis: for a being Element of K holds Per <*<*a*>*> = a
let a be Element of K; ::_thesis: Per <*<*a*>*> = a
set M = <*<*a*>*>;
A1: (PPath_product <*<*a*>*>) . (idseq 1) = a
proof
reconsider p = idseq 1 as Element of Permutations 1 by MATRIX_2:def_9;
A2: len (Path_matrix (p,<*<*a*>*>)) = 1 by MATRIX_3:def_7;
then A3: dom (Path_matrix (p,<*<*a*>*>)) = Seg 1 by FINSEQ_1:def_3;
then A4: 1 in dom (Path_matrix (p,<*<*a*>*>)) ;
then 1 = p . 1 by A3, FUNCT_1:18;
then (Path_matrix (p,<*<*a*>*>)) . 1 = <*<*a*>*> * (1,1) by A4, MATRIX_3:def_7;
then (Path_matrix (p,<*<*a*>*>)) . 1 = a by MATRIX_2:5;
then A5: Path_matrix (p,<*<*a*>*>) = <*a*> by A2, FINSEQ_1:40;
( (PPath_product <*<*a*>*>) . p = the multF of K $$ (Path_matrix (p,<*<*a*>*>)) & <*a*> = 1 |-> a ) by Def1, FINSEQ_2:59;
hence (PPath_product <*<*a*>*>) . (idseq 1) = a by A5, FINSOP_1:16; ::_thesis: verum
end;
( FinOmega (Permutations 1) = {(idseq 1)} & idseq 1 in Permutations 1 ) by MATRIX_2:19, MATRIX_2:def_14, TARSKI:def_1;
hence Per <*<*a*>*> = a by A1, SETWISEO:17; ::_thesis: verum
end;
theorem :: MATRIX_9:8
for K being Field
for n being Element of NAT st n >= 1 holds
Per (0. (K,n,n)) = 0. K
proof
let K be Field; ::_thesis: for n being Element of NAT st n >= 1 holds
Per (0. (K,n,n)) = 0. K
let n be Element of NAT ; ::_thesis: ( n >= 1 implies Per (0. (K,n,n)) = 0. K )
set B = FinOmega (Permutations n);
set f = PPath_product (0. (K,n,n));
set F = the addF of K;
set Y = the carrier of K;
set X = Permutations n;
reconsider G0 = (Fin (Permutations n)) --> (0. K) as Function of (Fin (Permutations n)), the carrier of K ;
A1: for e being Element of the carrier of K st e is_a_unity_wrt the addF of K holds
G0 . {} = e
proof
let e be Element of the carrier of K; ::_thesis: ( e is_a_unity_wrt the addF of K implies G0 . {} = e )
0. K is_a_unity_wrt the addF of K by FVSUM_1:6;
then A2: the addF of K . ((0. K),e) = e by BINOP_1:3;
assume e is_a_unity_wrt the addF of K ; ::_thesis: G0 . {} = e
then the addF of K . ((0. K),e) = 0. K by BINOP_1:3;
hence G0 . {} = e by A2, FINSUB_1:7, FUNCOP_1:7; ::_thesis: verum
end;
assume A3: n >= 1 ; ::_thesis: Per (0. (K,n,n)) = 0. K
A4: for x being set st x in dom (PPath_product (0. (K,n,n))) holds
(PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
proof
let x be set ; ::_thesis: ( x in dom (PPath_product (0. (K,n,n))) implies (PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x )
assume x in dom (PPath_product (0. (K,n,n))) ; ::_thesis: (PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x
for p being Element of Permutations n holds ((Permutations n) --> (0. K)) . p = the multF of K $$ (Path_matrix (p,(0. (K,n,n))))
proof
defpred S1[ Element of NAT ] means the multF of K $$ (($1 + 1) |-> (0. K)) = 0. K;
let p be Element of Permutations n; ::_thesis: ((Permutations n) --> (0. K)) . p = the multF of K $$ (Path_matrix (p,(0. (K,n,n))))
A5: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A6: ((k + 1) + 1) |-> (0. K) = ((k + 1) |-> (0. K)) ^ <*(0. K)*> by FINSEQ_2:60;
assume S1[k] ; ::_thesis: S1[k + 1]
then the multF of K $$ (((k + 1) + 1) |-> (0. K)) = (0. K) * (0. K) by A6, FINSOP_1:4
.= 0. K by VECTSP_1:6 ;
hence S1[k + 1] ; ::_thesis: verum
end;
A7: for i, j being Nat st i in dom (n |-> (0. K)) & j = p . i holds
(n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)
proof
let i, j be Nat; ::_thesis: ( i in dom (n |-> (0. K)) & j = p . i implies (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) )
assume that
A8: i in dom (n |-> (0. K)) and
A9: j = p . i ; ::_thesis: (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j)
A10: i in Seg n by A8, FUNCOP_1:13;
then j in Seg n by A9, MATRIX_7:14;
then A11: j in Seg (width (0. (K,n,n))) by A3, MATRIX_1:23;
i in dom (0. (K,n,n)) by A10, MATRIX_7:13;
then [i,j] in [:(dom (0. (K,n,n))),(Seg (width (0. (K,n,n)))):] by A11, ZFMISC_1:def_2;
then A12: [i,j] in Indices (0. (K,n,n)) by MATRIX_1:def_4;
(n |-> (0. K)) . i = 0. K by A10, FUNCOP_1:7;
hence (n |-> (0. K)) . i = (0. (K,n,n)) * (i,j) by A12, MATRIX_3:1; ::_thesis: verum
end;
len (n |-> (0. K)) = n by CARD_1:def_7;
then A13: Path_matrix (p,(0. (K,n,n))) = n |-> (0. K) by A7, MATRIX_3:def_7;
A14: (n -' 1) + 1 = n by A3, XREAL_1:235;
1 |-> (0. K) = <*(0. K)*> by FINSEQ_2:59;
then A15: S1[ 0 ] by FINSOP_1:11;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A5);
then the multF of K $$ (Path_matrix (p,(0. (K,n,n)))) = 0. K by A13, A14;
hence ((Permutations n) --> (0. K)) . p = the multF of K $$ (Path_matrix (p,(0. (K,n,n)))) by FUNCOP_1:7; ::_thesis: verum
end;
hence (PPath_product (0. (K,n,n))) . x = ((Permutations n) --> (0. K)) . x by Def1; ::_thesis: verum
end;
dom ((Permutations n) --> (0. K)) = Permutations n by FUNCOP_1:13;
then dom (PPath_product (0. (K,n,n))) = dom ((Permutations n) --> (0. K)) by FUNCT_2:def_1;
then A16: PPath_product (0. (K,n,n)) = (Permutations n) --> (0. K) by A4, FUNCT_1:2;
A17: for x being Element of Permutations n holds G0 . {x} = (PPath_product (0. (K,n,n))) . x
proof
let x be Element of Permutations n; ::_thesis: G0 . {x} = (PPath_product (0. (K,n,n))) . x
G0 . {.x.} = 0. K by FUNCOP_1:7;
hence G0 . {x} = (PPath_product (0. (K,n,n))) . x by A16, FUNCOP_1:7; ::_thesis: verum
end;
A18: for B9 being Element of Fin (Permutations n) st B9 c= FinOmega (Permutations n) & B9 <> {} holds
for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x))
proof
let B9 be Element of Fin (Permutations n); ::_thesis: ( B9 c= FinOmega (Permutations n) & B9 <> {} implies for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) )
assume that
B9 c= FinOmega (Permutations n) and
B9 <> {} ; ::_thesis: for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x))
thus for x being Element of Permutations n st x in (FinOmega (Permutations n)) \ B9 holds
G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) ::_thesis: verum
proof
let x be Element of Permutations n; ::_thesis: ( x in (FinOmega (Permutations n)) \ B9 implies G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) )
assume x in (FinOmega (Permutations n)) \ B9 ; ::_thesis: G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x))
A19: ( G0 . (B9 \/ {.x.}) = 0. K & G0 . B9 = 0. K ) by FUNCOP_1:7;
( (PPath_product (0. (K,n,n))) . x = 0. K & 0. K is_a_unity_wrt the addF of K ) by A16, FUNCOP_1:7, FVSUM_1:6;
hence G0 . (B9 \/ {x}) = the addF of K . ((G0 . B9),((PPath_product (0. (K,n,n))) . x)) by A19, BINOP_1:3; ::_thesis: verum
end;
end;
( FinOmega (Permutations n) <> {} & G0 . (FinOmega (Permutations n)) = 0. K ) by FUNCOP_1:7, MATRIX_2:26, MATRIX_2:def_14;
hence Per (0. (K,n,n)) = 0. K by A1, A17, A18, SETWISEO:def_3; ::_thesis: verum
end;
theorem Th9: :: MATRIX_9:9
for K being Field
for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
proof
let K be Field; ::_thesis: for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
let a, b, c, d be Element of K; ::_thesis: for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
let p be Element of Permutations 2; ::_thesis: ( p = idseq 2 implies Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*> )
assume A1: p = idseq 2 ; ::_thesis: Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*>
A2: len (Path_matrix (p,((a,b) ][ (c,d)))) = 2 by MATRIX_3:def_7;
then A3: dom (Path_matrix (p,((a,b) ][ (c,d)))) = Seg 2 by FINSEQ_1:def_3;
then A4: 2 in dom (Path_matrix (p,((a,b) ][ (c,d)))) ;
then 2 = p . 2 by A1, A3, FUNCT_1:18;
then A5: (Path_matrix (p,((a,b) ][ (c,d)))) . 2 = ((a,b) ][ (c,d)) * (2,2) by A4, MATRIX_3:def_7
.= d by MATRIX_2:6 ;
A6: 1 in dom (Path_matrix (p,((a,b) ][ (c,d)))) by A3;
then 1 = p . 1 by A1, A3, FUNCT_1:18;
then (Path_matrix (p,((a,b) ][ (c,d)))) . 1 = ((a,b) ][ (c,d)) * (1,1) by A6, MATRIX_3:def_7
.= a by MATRIX_2:6 ;
hence Path_matrix (p,((a,b) ][ (c,d))) = <*a,d*> by A2, A5, FINSEQ_1:44; ::_thesis: verum
end;
theorem Th10: :: MATRIX_9:10
for K being Field
for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = Rev (idseq 2) holds
Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>
proof
let K be Field; ::_thesis: for a, b, c, d being Element of K
for p being Element of Permutations 2 st p = Rev (idseq 2) holds
Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>
let a, b, c, d be Element of K; ::_thesis: for p being Element of Permutations 2 st p = Rev (idseq 2) holds
Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>
let p be Element of Permutations 2; ::_thesis: ( p = Rev (idseq 2) implies Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*> )
assume A1: p = Rev (idseq 2) ; ::_thesis: Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*>
A2: len (Path_matrix (p,((a,b) ][ (c,d)))) = 2 by MATRIX_3:def_7;
then A3: dom (Path_matrix (p,((a,b) ][ (c,d)))) = Seg 2 by FINSEQ_1:def_3;
then 1 in dom (Path_matrix (p,((a,b) ][ (c,d)))) ;
then A4: (Path_matrix (p,((a,b) ][ (c,d)))) . 1 = ((a,b) ][ (c,d)) * (1,2) by A1, Th2, MATRIX_3:def_7
.= b by MATRIX_2:6 ;
2 in dom (Path_matrix (p,((a,b) ][ (c,d)))) by A3;
then (Path_matrix (p,((a,b) ][ (c,d)))) . 2 = ((a,b) ][ (c,d)) * (2,1) by A1, Th2, MATRIX_3:def_7
.= c by MATRIX_2:6 ;
hence Path_matrix (p,((a,b) ][ (c,d))) = <*b,c*> by A2, A4, FINSEQ_1:44; ::_thesis: verum
end;
theorem Th11: :: MATRIX_9:11
for K being Field
for a, b being Element of K holds the multF of K $$ <*a,b*> = a * b
proof
let K be Field; ::_thesis: for a, b being Element of K holds the multF of K $$ <*a,b*> = a * b
let a, b be Element of K; ::_thesis: the multF of K $$ <*a,b*> = a * b
the multF of K $$ <*a,b*> = Product <*a,b*> by GROUP_4:def_2
.= a * b by GROUP_4:10 ;
hence the multF of K $$ <*a,b*> = a * b ; ::_thesis: verum
end;
begin
registration
cluster Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective finite odd for Element of bool [:(Seg 2),(Seg 2):];
existence
ex b1 being Permutation of (Seg 2) st b1 is odd
proof
reconsider g = <*2,1*> as Permutation of (Seg 2) by Lm2, MATRIX_2:def_9;
for l being FinSequence of (Group_of_Perm 2) holds
( not (len l) mod 2 = 0 or not g = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 2 holds
( not l . i = q or not q is being_transposition ) ) ) ) by Lm1, MATRIX_7:11;
then g is odd by MATRIX_2:def_12;
hence ex b1 being Permutation of (Seg 2) st b1 is odd ; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite even for Element of bool [:(Seg n),(Seg n):];
existence
ex b1 being Permutation of (Seg n) st b1 is even
proof
reconsider f = id (Seg n) as Permutation of (Seg n) ;
f is even by MATRIX_2:25;
hence ex b1 being Permutation of (Seg n) st b1 is even ; ::_thesis: verum
end;
end;
theorem Th12: :: MATRIX_9:12
<*2,1*> is odd Permutation of (Seg 2)
proof
reconsider g = <*2,1*> as Permutation of (Seg 2) by Lm2, MATRIX_2:def_9;
for l being FinSequence of (Group_of_Perm 2) holds
( not (len l) mod 2 = 0 or not g = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 2 holds
( not l . i = q or not q is being_transposition ) ) ) ) by Lm1, MATRIX_7:11;
hence <*2,1*> is odd Permutation of (Seg 2) by MATRIX_2:def_12; ::_thesis: verum
end;
theorem :: MATRIX_9:13
for K being Field
for a, b, c, d being Element of K holds Det ((a,b) ][ (c,d)) = (a * d) - (b * c)
proof
let K be Field; ::_thesis: for a, b, c, d being Element of K holds Det ((a,b) ][ (c,d)) = (a * d) - (b * c)
let a, b, c, d be Element of K; ::_thesis: Det ((a,b) ][ (c,d)) = (a * d) - (b * c)
reconsider rid2 = Rev (idseq 2) as Element of Permutations 2 by Th4;
set M = (a,b) ][ (c,d);
reconsider id2 = idseq 2 as Permutation of (Seg 2) ;
reconsider Id2 = idseq 2 as Element of Permutations 2 by MATRIX_2:def_9;
set F = the addF of K;
set f = Path_product ((a,b) ][ (c,d));
A1: ( rid2 = <*2,1*> & len (Permutations 2) = 2 ) by FINSEQ_2:52, FINSEQ_5:61, MATRIX_2:18;
A2: (Path_product ((a,b) ][ (c,d))) . rid2 = - (( the multF of K $$ (Path_matrix (rid2,((a,b) ][ (c,d))))),rid2) by MATRIX_3:def_8
.= - ( the multF of K $$ (Path_matrix (rid2,((a,b) ][ (c,d))))) by A1, Th12, MATRIX_2:def_13
.= - ( the multF of K $$ <*b,c*>) by Th10
.= - (b * c) by Th11 ;
len (Permutations 2) = 2 by MATRIX_2:18;
then A3: Id2 is even by MATRIX_2:25;
1 in Seg 2 ;
then A4: id2 <> rid2 by Th2, FUNCT_1:18;
A5: (Path_product ((a,b) ][ (c,d))) . id2 = - (( the multF of K $$ (Path_matrix (Id2,((a,b) ][ (c,d))))),Id2) by MATRIX_3:def_8
.= the multF of K $$ (Path_matrix (Id2,((a,b) ][ (c,d)))) by A3, MATRIX_2:def_13
.= the multF of K $$ <*a,d*> by Th9
.= a * d by Th11 ;
FinOmega (Permutations 2) = Permutations 2 by MATRIX_2:26, MATRIX_2:def_14;
then Det ((a,b) ][ (c,d)) = the addF of K $$ ({.Id2,rid2.},(Path_product ((a,b) ][ (c,d)))) by Th6, MATRIX_3:def_9
.= (a * d) - (b * c) by A5, A4, A2, SETWOP_2:1 ;
hence Det ((a,b) ][ (c,d)) = (a * d) - (b * c) ; ::_thesis: verum
end;
theorem :: MATRIX_9:14
for K being Field
for a, b, c, d being Element of K holds Per ((a,b) ][ (c,d)) = (a * d) + (b * c)
proof
let K be Field; ::_thesis: for a, b, c, d being Element of K holds Per ((a,b) ][ (c,d)) = (a * d) + (b * c)
let a, b, c, d be Element of K; ::_thesis: Per ((a,b) ][ (c,d)) = (a * d) + (b * c)
reconsider rid2 = Rev (idseq 2) as Element of Permutations 2 by Th4;
set M = (a,b) ][ (c,d);
reconsider Id2 = idseq 2 as Element of Permutations 2 by MATRIX_2:def_9;
reconsider id2 = Id2 as Permutation of (Seg 2) ;
set f = PPath_product ((a,b) ][ (c,d));
1 in Seg 2 ;
then A1: ( FinOmega (Permutations 2) = Permutations 2 & id2 <> rid2 ) by Th2, FUNCT_1:18, MATRIX_2:26, MATRIX_2:def_14;
A2: (PPath_product ((a,b) ][ (c,d))) . rid2 = the multF of K $$ (Path_matrix (rid2,((a,b) ][ (c,d)))) by Def1
.= the multF of K $$ <*b,c*> by Th10
.= b * c by Th11 ;
(PPath_product ((a,b) ][ (c,d))) . id2 = the multF of K $$ (Path_matrix (Id2,((a,b) ][ (c,d)))) by Def1
.= the multF of K $$ <*a,d*> by Th9
.= a * d by Th11 ;
hence Per ((a,b) ][ (c,d)) = (a * d) + (b * c) by A2, A1, Th6, SETWOP_2:1; ::_thesis: verum
end;
theorem Th15: :: MATRIX_9:15
Rev (idseq 3) = <*3,2,1*>
proof
reconsider h = <*2,3*> as FinSequence of NAT ;
( <*1*> ^ h = <*1,2,3*> & Rev h = <*3,2*> ) by FINSEQ_1:43, FINSEQ_5:61;
hence Rev (idseq 3) = <*3,2,1*> by FINSEQ_2:53, FINSEQ_6:24; ::_thesis: verum
end;
theorem :: MATRIX_9:16
for D being non empty set
for x, y, z being Element of D
for f being FinSequence of D st f = <*x,y,z*> holds
Rev f = <*z,y,x*>
proof
let D be non empty set ; ::_thesis: for x, y, z being Element of D
for f being FinSequence of D st f = <*x,y,z*> holds
Rev f = <*z,y,x*>
let x, y, z be Element of D; ::_thesis: for f being FinSequence of D st f = <*x,y,z*> holds
Rev f = <*z,y,x*>
let f be FinSequence of D; ::_thesis: ( f = <*x,y,z*> implies Rev f = <*z,y,x*> )
reconsider h = <*y,z*> as FinSequence of D ;
assume f = <*x,y,z*> ; ::_thesis: Rev f = <*z,y,x*>
then A1: f = <*x*> ^ h by FINSEQ_1:43;
Rev h = <*z,y*> by FINSEQ_5:61;
hence Rev f = <*z,y,x*> by A1, FINSEQ_6:24; ::_thesis: verum
end;
theorem Th17: :: MATRIX_9:17
for n being Nat
for f, g being FinSequence st f ^ g in Permutations n holds
f ^ (Rev g) in Permutations n
proof
let n be Nat; ::_thesis: for f, g being FinSequence st f ^ g in Permutations n holds
f ^ (Rev g) in Permutations n
let f, g be FinSequence; ::_thesis: ( f ^ g in Permutations n implies f ^ (Rev g) in Permutations n )
A1: rng g = rng (Rev g) by FINSEQ_5:57;
set h = f ^ (Rev g);
assume f ^ g in Permutations n ; ::_thesis: f ^ (Rev g) in Permutations n
then A2: f ^ g is Permutation of (Seg n) by MATRIX_2:def_9;
then A3: g is one-to-one by FINSEQ_3:91;
dom (f ^ g) = Seg n by A2, FUNCT_2:52;
then A4: Seg n = Seg ((len f) + (len g)) by FINSEQ_1:def_7;
len g = len (Rev g) by FINSEQ_5:def_3;
then A5: dom (f ^ (Rev g)) = Seg n by A4, FINSEQ_1:def_7;
A6: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31
.= rng (f ^ (Rev g)) by A1, FINSEQ_1:31 ;
A7: rng (f ^ g) = Seg n by A2, FUNCT_2:def_3;
then reconsider h = f ^ (Rev g) as FinSequence-like Function of (Seg n),(Seg n) by A6, A5, FUNCT_2:2;
A8: h is onto by A7, A6, FUNCT_2:def_3;
( rng f misses rng g & f is one-to-one ) by A2, FINSEQ_3:91;
then h is one-to-one by A1, A3, FINSEQ_3:91;
hence f ^ (Rev g) in Permutations n by A8, MATRIX_2:def_9; ::_thesis: verum
end;
theorem Th18: :: MATRIX_9:18
for n being Nat
for f, g being FinSequence st f ^ g in Permutations n holds
g ^ f in Permutations n
proof
let n be Nat; ::_thesis: for f, g being FinSequence st f ^ g in Permutations n holds
g ^ f in Permutations n
let f, g be FinSequence; ::_thesis: ( f ^ g in Permutations n implies g ^ f in Permutations n )
A1: Seg (len (f ^ g)) = dom (f ^ g) by FINSEQ_1:def_3;
len (f ^ g) = (len f) + (len g) by FINSEQ_1:22
.= len (g ^ f) by FINSEQ_1:22 ;
then A2: dom (f ^ g) = dom (g ^ f) by A1, FINSEQ_1:def_3;
A3: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31
.= rng (g ^ f) by FINSEQ_1:31 ;
assume f ^ g in Permutations n ; ::_thesis: g ^ f in Permutations n
then A4: f ^ g is Permutation of (Seg n) by MATRIX_2:def_9;
then A5: rng (f ^ g) = Seg n by FUNCT_2:def_3;
A6: g is one-to-one by A4, FINSEQ_3:91;
dom (f ^ g) = Seg n by A4, FUNCT_2:52;
then reconsider h = g ^ f as FinSequence-like Function of (Seg n),(Seg n) by A5, A2, A3, FUNCT_2:2;
( rng f misses rng g & f is one-to-one ) by A4, FINSEQ_3:91;
then A7: h is one-to-one by A6, FINSEQ_3:91;
h is onto by A5, A3, FUNCT_2:def_3;
hence g ^ f in Permutations n by A7, MATRIX_2:def_9; ::_thesis: verum
end;
theorem Th19: :: MATRIX_9:19
Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
proof
now__::_thesis:_for_x_being_set_st_x_in_{<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}_holds_
x_in_Permutations_3
let x be set ; ::_thesis: ( x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} implies x in Permutations 3 )
A1: idseq 3 in Permutations 3 by MATRIX_2:def_9;
A2: <*3,1,2*> in Permutations 3
proof
reconsider h = <*1,2*> as FinSequence of NAT ;
<*3*> ^ h = <*3,1,2*> by FINSEQ_1:43;
hence <*3,1,2*> in Permutations 3 by A1, Th18, FINSEQ_2:53; ::_thesis: verum
end;
A3: <*2,3,1*> in Permutations 3
proof
reconsider h = <*2,3*> as FinSequence of NAT ;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:53;
f = <*1*> ^ h by FINSEQ_1:43;
hence <*2,3,1*> in Permutations 3 by A1, Th18, FINSEQ_2:53; ::_thesis: verum
end;
A4: <*1,3,2*> in Permutations 3
proof
reconsider h = <*2,3*> as FinSequence of NAT ;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:53;
Rev h = <*3,2*> by FINSEQ_5:61;
then ( f = <*1*> ^ h & <*1*> ^ (Rev h) = <*1,3,2*> ) by FINSEQ_1:43;
hence <*1,3,2*> in Permutations 3 by A1, Th17, FINSEQ_2:53; ::_thesis: verum
end;
A5: <*2,1,3*> in Permutations 3
proof
reconsider h = <*1,2*> as FinSequence of NAT ;
<*3*> ^ h in Permutations 3 by A1, Th18, FINSEQ_2:53;
then ( Rev h = <*2,1*> & <*3*> ^ (Rev h) in Permutations 3 ) by Th17, FINSEQ_5:61;
hence <*2,1,3*> in Permutations 3 by Th18; ::_thesis: verum
end;
assume x in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ; ::_thesis: x in Permutations 3
then x in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by ENUMSET1:12;
then ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def_3;
then ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} ) by ENUMSET1:5;
then A6: ( x in {<*1,2,3*>,<*3,2,1*>} or x in {<*1,3,2*>,<*2,3,1*>} or x in {<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def_3;
Rev (idseq 3) in Permutations 3 by Th4;
hence x in Permutations 3 by A6, A1, A4, A3, A5, A2, Th15, FINSEQ_2:53, TARSKI:def_2; ::_thesis: verum
end;
then A7: {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} c= Permutations 3 by TARSKI:def_3;
now__::_thesis:_for_p_being_set_st_p_in_Permutations_3_holds_
p_in_{<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
let p be set ; ::_thesis: ( p in Permutations 3 implies p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} )
assume p in Permutations 3 ; ::_thesis: p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
then reconsider q = p as Permutation of (Seg 3) by MATRIX_2:def_9;
A8: rng q = Seg 3 by FUNCT_2:def_3;
A9: 3 in Seg 3 ;
then q . 3 in Seg 3 by A8, FUNCT_2:4;
then A10: ( q . 3 = 1 or q . 3 = 2 or q . 3 = 3 ) by ENUMSET1:def_1, FINSEQ_3:1;
A11: 2 in Seg 3 ;
then q . 2 in Seg 3 by A8, FUNCT_2:4;
then A12: ( q . 2 = 1 or q . 2 = 2 or q . 2 = 3 ) by ENUMSET1:def_1, FINSEQ_3:1;
A13: dom q = Seg 3 by FUNCT_2:52;
A14: ( ( not ( q . 1 = 1 & q . 2 = 2 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 2 & q . 3 = 1 ) & not ( q . 1 = 1 & q . 2 = 3 & q . 3 = 2 ) & not ( q . 1 = 2 & q . 2 = 3 & q . 3 = 1 ) & not ( q . 1 = 2 & q . 2 = 1 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 1 & q . 3 = 2 ) ) or q = <*1,2,3*> or q = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or q = <*2,1,3*> or q = <*3,1,2*> )
proof
reconsider q = q as FinSequence by A13, FINSEQ_1:def_2;
len q = 3 by A13, FINSEQ_1:def_3;
hence ( ( not ( q . 1 = 1 & q . 2 = 2 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 2 & q . 3 = 1 ) & not ( q . 1 = 1 & q . 2 = 3 & q . 3 = 2 ) & not ( q . 1 = 2 & q . 2 = 3 & q . 3 = 1 ) & not ( q . 1 = 2 & q . 2 = 1 & q . 3 = 3 ) & not ( q . 1 = 3 & q . 2 = 1 & q . 3 = 2 ) ) or q = <*1,2,3*> or q = <*3,2,1*> or q = <*1,3,2*> or q = <*2,3,1*> or q = <*2,1,3*> or q = <*3,1,2*> ) by FINSEQ_1:45; ::_thesis: verum
end;
A15: 1 in Seg 3 ;
then q . 1 in Seg 3 by A8, FUNCT_2:4;
then ( q . 1 = 1 or q . 1 = 2 or q . 1 = 3 ) by ENUMSET1:def_1, FINSEQ_3:1;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>} or q in {<*2,1,3*>,<*3,1,2*>} ) by A13, A15, A11, A9, A12, A10, A14, FUNCT_1:def_4, TARSKI:def_2;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} ) by XBOOLE_0:def_3;
then ( p in {<*1,2,3*>,<*3,2,1*>} or q in {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} ) by ENUMSET1:5;
then p in {<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by XBOOLE_0:def_3;
hence p in {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by ENUMSET1:12; ::_thesis: verum
end;
then Permutations 3 c= {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by TARSKI:def_3;
hence Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th20: :: MATRIX_9:20
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*>
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*>
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*>
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies for p being Element of Permutations 3 st p = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*> )
[1,1] in Indices M by MATRIX_1:37;
then consider r being FinSequence of the carrier of K such that
A1: r = M . 1 and
A2: M * (1,1) = r . 1 by MATRIX_1:def_5;
assume A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: for p being Element of Permutations 3 st p = <*1,2,3*> holds
Path_matrix (p,M) = <*a,e,i*>
then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 1 = a by A1, FINSEQ_1:45;
[3,3] in Indices M by MATRIX_1:37;
then consider z being FinSequence of the carrier of K such that
A5: z = M . 3 and
A6: M * (3,3) = z . 3 by MATRIX_1:def_5;
M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;
then A7: z . 3 = i by A5, FINSEQ_1:45;
[2,2] in Indices M by MATRIX_1:37;
then consider y being FinSequence of the carrier of K such that
A8: y = M . 2 and
A9: M * (2,2) = y . 2 by MATRIX_1:def_5;
M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;
then A10: y . 2 = e by A8, FINSEQ_1:45;
let p be Element of Permutations 3; ::_thesis: ( p = <*1,2,3*> implies Path_matrix (p,M) = <*a,e,i*> )
assume A11: p = <*1,2,3*> ; ::_thesis: Path_matrix (p,M) = <*a,e,i*>
then A12: 1 = p . 1 by FINSEQ_1:45;
A13: 3 = p . 3 by A11, FINSEQ_1:45;
A14: 2 = p . 2 by A11, FINSEQ_1:45;
A15: len (Path_matrix (p,M)) = 3 by MATRIX_3:def_7;
then A16: dom (Path_matrix (p,M)) = Seg 3 by FINSEQ_1:def_3;
then 2 in dom (Path_matrix (p,M)) ;
then A17: (Path_matrix (p,M)) . 2 = e by A14, A9, A10, MATRIX_3:def_7;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = i by A13, A6, A7, MATRIX_3:def_7;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = a by A12, A2, A4, MATRIX_3:def_7;
hence Path_matrix (p,M) = <*a,e,i*> by A15, A17, A18, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th21: :: MATRIX_9:21
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,2,1*> holds
Path_matrix (p,M) = <*c,e,g*>
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,2,1*> holds
Path_matrix (p,M) = <*c,e,g*>
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,2,1*> holds
Path_matrix (p,M) = <*c,e,g*>
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies for p being Element of Permutations 3 st p = <*3,2,1*> holds
Path_matrix (p,M) = <*c,e,g*> )
[1,3] in Indices M by MATRIX_1:37;
then consider r being FinSequence of the carrier of K such that
A1: r = M . 1 and
A2: M * (1,3) = r . 3 by MATRIX_1:def_5;
assume A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: for p being Element of Permutations 3 st p = <*3,2,1*> holds
Path_matrix (p,M) = <*c,e,g*>
then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 3 = c by A1, FINSEQ_1:45;
[3,1] in Indices M by MATRIX_1:37;
then consider z being FinSequence of the carrier of K such that
A5: z = M . 3 and
A6: M * (3,1) = z . 1 by MATRIX_1:def_5;
M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;
then A7: z . 1 = g by A5, FINSEQ_1:45;
[2,2] in Indices M by MATRIX_1:37;
then consider y being FinSequence of the carrier of K such that
A8: y = M . 2 and
A9: M * (2,2) = y . 2 by MATRIX_1:def_5;
M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;
then A10: y . 2 = e by A8, FINSEQ_1:45;
let p be Element of Permutations 3; ::_thesis: ( p = <*3,2,1*> implies Path_matrix (p,M) = <*c,e,g*> )
assume A11: p = <*3,2,1*> ; ::_thesis: Path_matrix (p,M) = <*c,e,g*>
then A12: 3 = p . 1 by FINSEQ_1:45;
A13: 1 = p . 3 by A11, FINSEQ_1:45;
A14: 2 = p . 2 by A11, FINSEQ_1:45;
A15: len (Path_matrix (p,M)) = 3 by MATRIX_3:def_7;
then A16: dom (Path_matrix (p,M)) = Seg 3 by FINSEQ_1:def_3;
then 2 in dom (Path_matrix (p,M)) ;
then A17: (Path_matrix (p,M)) . 2 = e by A14, A9, A10, MATRIX_3:def_7;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = g by A13, A6, A7, MATRIX_3:def_7;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = c by A12, A2, A4, MATRIX_3:def_7;
hence Path_matrix (p,M) = <*c,e,g*> by A15, A17, A18, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th22: :: MATRIX_9:22
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,3,2*> holds
Path_matrix (p,M) = <*a,f,h*>
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,3,2*> holds
Path_matrix (p,M) = <*a,f,h*>
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*1,3,2*> holds
Path_matrix (p,M) = <*a,f,h*>
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies for p being Element of Permutations 3 st p = <*1,3,2*> holds
Path_matrix (p,M) = <*a,f,h*> )
[1,1] in Indices M by MATRIX_1:37;
then consider r being FinSequence of the carrier of K such that
A1: r = M . 1 and
A2: M * (1,1) = r . 1 by MATRIX_1:def_5;
assume A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: for p being Element of Permutations 3 st p = <*1,3,2*> holds
Path_matrix (p,M) = <*a,f,h*>
then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 1 = a by A1, FINSEQ_1:45;
[3,2] in Indices M by MATRIX_1:37;
then consider z being FinSequence of the carrier of K such that
A5: z = M . 3 and
A6: M * (3,2) = z . 2 by MATRIX_1:def_5;
M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;
then A7: z . 2 = h by A5, FINSEQ_1:45;
[2,3] in Indices M by MATRIX_1:37;
then consider y being FinSequence of the carrier of K such that
A8: y = M . 2 and
A9: M * (2,3) = y . 3 by MATRIX_1:def_5;
M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;
then A10: y . 3 = f by A8, FINSEQ_1:45;
let p be Element of Permutations 3; ::_thesis: ( p = <*1,3,2*> implies Path_matrix (p,M) = <*a,f,h*> )
assume A11: p = <*1,3,2*> ; ::_thesis: Path_matrix (p,M) = <*a,f,h*>
then A12: 1 = p . 1 by FINSEQ_1:45;
A13: 2 = p . 3 by A11, FINSEQ_1:45;
A14: 3 = p . 2 by A11, FINSEQ_1:45;
A15: len (Path_matrix (p,M)) = 3 by MATRIX_3:def_7;
then A16: dom (Path_matrix (p,M)) = Seg 3 by FINSEQ_1:def_3;
then 2 in dom (Path_matrix (p,M)) ;
then A17: (Path_matrix (p,M)) . 2 = f by A14, A9, A10, MATRIX_3:def_7;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = h by A13, A6, A7, MATRIX_3:def_7;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = a by A12, A2, A4, MATRIX_3:def_7;
hence Path_matrix (p,M) = <*a,f,h*> by A15, A17, A18, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th23: :: MATRIX_9:23
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies for p being Element of Permutations 3 st p = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*> )
[1,2] in Indices M by MATRIX_1:37;
then consider r being FinSequence of the carrier of K such that
A1: r = M . 1 and
A2: M * (1,2) = r . 2 by MATRIX_1:def_5;
assume A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: for p being Element of Permutations 3 st p = <*2,3,1*> holds
Path_matrix (p,M) = <*b,f,g*>
then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 2 = b by A1, FINSEQ_1:45;
[3,1] in Indices M by MATRIX_1:37;
then consider z being FinSequence of the carrier of K such that
A5: z = M . 3 and
A6: M * (3,1) = z . 1 by MATRIX_1:def_5;
M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;
then A7: z . 1 = g by A5, FINSEQ_1:45;
[2,3] in Indices M by MATRIX_1:37;
then consider y being FinSequence of the carrier of K such that
A8: y = M . 2 and
A9: M * (2,3) = y . 3 by MATRIX_1:def_5;
M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;
then A10: y . 3 = f by A8, FINSEQ_1:45;
let p be Element of Permutations 3; ::_thesis: ( p = <*2,3,1*> implies Path_matrix (p,M) = <*b,f,g*> )
assume A11: p = <*2,3,1*> ; ::_thesis: Path_matrix (p,M) = <*b,f,g*>
then A12: 2 = p . 1 by FINSEQ_1:45;
A13: 1 = p . 3 by A11, FINSEQ_1:45;
A14: 3 = p . 2 by A11, FINSEQ_1:45;
A15: len (Path_matrix (p,M)) = 3 by MATRIX_3:def_7;
then A16: dom (Path_matrix (p,M)) = Seg 3 by FINSEQ_1:def_3;
then 2 in dom (Path_matrix (p,M)) ;
then A17: (Path_matrix (p,M)) . 2 = f by A14, A9, A10, MATRIX_3:def_7;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = g by A13, A6, A7, MATRIX_3:def_7;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = b by A12, A2, A4, MATRIX_3:def_7;
hence Path_matrix (p,M) = <*b,f,g*> by A15, A17, A18, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th24: :: MATRIX_9:24
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,1,3*> holds
Path_matrix (p,M) = <*b,d,i*>
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,1,3*> holds
Path_matrix (p,M) = <*b,d,i*>
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*2,1,3*> holds
Path_matrix (p,M) = <*b,d,i*>
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies for p being Element of Permutations 3 st p = <*2,1,3*> holds
Path_matrix (p,M) = <*b,d,i*> )
[1,2] in Indices M by MATRIX_1:37;
then consider r being FinSequence of the carrier of K such that
A1: r = M . 1 and
A2: M * (1,2) = r . 2 by MATRIX_1:def_5;
assume A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: for p being Element of Permutations 3 st p = <*2,1,3*> holds
Path_matrix (p,M) = <*b,d,i*>
then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 2 = b by A1, FINSEQ_1:45;
[3,3] in Indices M by MATRIX_1:37;
then consider z being FinSequence of the carrier of K such that
A5: z = M . 3 and
A6: M * (3,3) = z . 3 by MATRIX_1:def_5;
M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;
then A7: z . 3 = i by A5, FINSEQ_1:45;
[2,1] in Indices M by MATRIX_1:37;
then consider y being FinSequence of the carrier of K such that
A8: y = M . 2 and
A9: M * (2,1) = y . 1 by MATRIX_1:def_5;
M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;
then A10: y . 1 = d by A8, FINSEQ_1:45;
let p be Element of Permutations 3; ::_thesis: ( p = <*2,1,3*> implies Path_matrix (p,M) = <*b,d,i*> )
assume A11: p = <*2,1,3*> ; ::_thesis: Path_matrix (p,M) = <*b,d,i*>
then A12: 2 = p . 1 by FINSEQ_1:45;
A13: 3 = p . 3 by A11, FINSEQ_1:45;
A14: 1 = p . 2 by A11, FINSEQ_1:45;
A15: len (Path_matrix (p,M)) = 3 by MATRIX_3:def_7;
then A16: dom (Path_matrix (p,M)) = Seg 3 by FINSEQ_1:def_3;
then 2 in dom (Path_matrix (p,M)) ;
then A17: (Path_matrix (p,M)) . 2 = d by A14, A9, A10, MATRIX_3:def_7;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = i by A13, A6, A7, MATRIX_3:def_7;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = b by A12, A2, A4, MATRIX_3:def_7;
hence Path_matrix (p,M) = <*b,d,i*> by A15, A17, A18, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th25: :: MATRIX_9:25
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*> )
[1,3] in Indices M by MATRIX_1:37;
then consider r being FinSequence of the carrier of K such that
A1: r = M . 1 and
A2: M * (1,3) = r . 3 by MATRIX_1:def_5;
assume A3: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: for p being Element of Permutations 3 st p = <*3,1,2*> holds
Path_matrix (p,M) = <*c,d,h*>
then M . 1 = <*a,b,c*> by FINSEQ_1:45;
then A4: r . 3 = c by A1, FINSEQ_1:45;
[3,2] in Indices M by MATRIX_1:37;
then consider z being FinSequence of the carrier of K such that
A5: z = M . 3 and
A6: M * (3,2) = z . 2 by MATRIX_1:def_5;
M . 3 = <*g,h,i*> by A3, FINSEQ_1:45;
then A7: z . 2 = h by A5, FINSEQ_1:45;
[2,1] in Indices M by MATRIX_1:37;
then consider y being FinSequence of the carrier of K such that
A8: y = M . 2 and
A9: M * (2,1) = y . 1 by MATRIX_1:def_5;
M . 2 = <*d,e,f*> by A3, FINSEQ_1:45;
then A10: y . 1 = d by A8, FINSEQ_1:45;
let p be Element of Permutations 3; ::_thesis: ( p = <*3,1,2*> implies Path_matrix (p,M) = <*c,d,h*> )
assume A11: p = <*3,1,2*> ; ::_thesis: Path_matrix (p,M) = <*c,d,h*>
then A12: 3 = p . 1 by FINSEQ_1:45;
A13: 2 = p . 3 by A11, FINSEQ_1:45;
A14: 1 = p . 2 by A11, FINSEQ_1:45;
A15: len (Path_matrix (p,M)) = 3 by MATRIX_3:def_7;
then A16: dom (Path_matrix (p,M)) = Seg 3 by FINSEQ_1:def_3;
then 2 in dom (Path_matrix (p,M)) ;
then A17: (Path_matrix (p,M)) . 2 = d by A14, A9, A10, MATRIX_3:def_7;
3 in dom (Path_matrix (p,M)) by A16;
then A18: (Path_matrix (p,M)) . 3 = h by A13, A6, A7, MATRIX_3:def_7;
1 in dom (Path_matrix (p,M)) by A16;
then (Path_matrix (p,M)) . 1 = c by A12, A2, A4, MATRIX_3:def_7;
hence Path_matrix (p,M) = <*c,d,h*> by A15, A17, A18, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th26: :: MATRIX_9:26
for K being Field
for a, b, c being Element of K holds the multF of K $$ <*a,b,c*> = (a * b) * c
proof
let K be Field; ::_thesis: for a, b, c being Element of K holds the multF of K $$ <*a,b,c*> = (a * b) * c
let a, b, c be Element of K; ::_thesis: the multF of K $$ <*a,b,c*> = (a * b) * c
the multF of K $$ <*a,b,c*> = Product <*a,b,c*> by GROUP_4:def_2
.= (a * b) * c by FVSUM_1:79 ;
hence the multF of K $$ <*a,b,c*> = (a * b) * c ; ::_thesis: verum
end;
theorem Th27: :: MATRIX_9:27
( <*1,3,2*> in Permutations 3 & <*2,3,1*> in Permutations 3 & <*2,1,3*> in Permutations 3 & <*3,1,2*> in Permutations 3 & <*1,2,3*> in Permutations 3 & <*3,2,1*> in Permutations 3 )
proof
set h = <*1,2*>;
reconsider f = <*1,2,3*> as one-to-one FinSequence-like Function of (Seg 3),(Seg 3) by FINSEQ_2:53;
A1: <*3*> ^ <*1,2*> = <*3,1,2*> by FINSEQ_1:43;
A2: <*1,3,2*> in Permutations 3
proof
set h = <*2,3*>;
Rev <*2,3*> = <*3,2*> by FINSEQ_5:61;
then A3: <*1*> ^ (Rev <*2,3*>) = <*1,3,2*> by FINSEQ_1:43;
( f = <*1*> ^ <*2,3*> & f in Permutations 3 ) by FINSEQ_1:43, FINSEQ_2:53, MATRIX_2:def_9;
hence <*1,3,2*> in Permutations 3 by A3, Th17; ::_thesis: verum
end;
A4: idseq 3 in Permutations 3 by MATRIX_2:def_9;
then <*3*> ^ <*1,2*> in Permutations 3 by Th18, FINSEQ_2:53;
then A5: <*3*> ^ (Rev <*1,2*>) in Permutations 3 by Th17;
( f = <*1*> ^ <*2,3*> & Rev <*1,2*> = <*2,1*> ) by FINSEQ_1:43, FINSEQ_5:61;
hence ( <*1,3,2*> in Permutations 3 & <*2,3,1*> in Permutations 3 & <*2,1,3*> in Permutations 3 & <*3,1,2*> in Permutations 3 & <*1,2,3*> in Permutations 3 & <*3,2,1*> in Permutations 3 ) by A4, A2, A5, A1, Th5, Th15, Th18, FINSEQ_2:53; ::_thesis: verum
end;
Lm3: <*1,2,3*> <> <*3,2,1*>
by FINSEQ_1:78;
Lm4: <*1,2,3*> <> <*1,3,2*>
by FINSEQ_1:78;
Lm5: <*1,2,3*> <> <*2,1,3*>
by FINSEQ_1:78;
Lm6: ( <*1,2,3*> <> <*2,3,1*> & <*1,2,3*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm7: ( <*3,2,1*> <> <*2,3,1*> & <*3,2,1*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm8: ( <*3,2,1*> <> <*2,1,3*> & <*1,3,2*> <> <*2,1,3*> )
by FINSEQ_1:78;
Lm9: ( <*1,3,2*> <> <*2,3,1*> & <*1,3,2*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm10: ( <*3,2,1*> <> <*1,3,2*> & <*2,3,1*> <> <*3,1,2*> )
by FINSEQ_1:78;
Lm11: ( <*2,3,1*> <> <*2,1,3*> & <*2,1,3*> <> <*3,1,2*> )
by FINSEQ_1:78;
theorem Th28: :: MATRIX_9:28
<*2,3,1*> " = <*3,1,2*>
proof
set f = <*2,3,1*>;
set g = <*3,1,2*>;
rng <*2,3,1*> = {2,3,1} by FINSEQ_2:128
.= {1,2,3} by ENUMSET1:59 ;
then A1: ( dom <*2,3,1*> = {1,2,3} & rng <*2,3,1*> = dom <*3,1,2*> ) by FINSEQ_3:1, FINSEQ_1:89;
then A2: dom (<*3,1,2*> * <*2,3,1*>) = {1,2,3} by RELAT_1:27;
A3: for x being set st x in dom (<*3,1,2*> * <*2,3,1*>) holds
(<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x
proof
let x be set ; ::_thesis: ( x in dom (<*3,1,2*> * <*2,3,1*>) implies (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x )
assume A4: x in dom (<*3,1,2*> * <*2,3,1*>) ; ::_thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x
percases ( x = 1 or x = 2 or x = 3 ) by A2, A4, ENUMSET1:def_1;
supposeA5: x = 1 ; ::_thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x
then <*3,1,2*> . (<*2,3,1*> . x) = <*3,1,2*> . 2 by FINSEQ_1:45
.= 1 by FINSEQ_1:45
.= (id {1,2,3}) . x by A2, A4, A5, FUNCT_1:18 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A4, FUNCT_1:12; ::_thesis: verum
end;
supposeA6: x = 2 ; ::_thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x
then <*3,1,2*> . (<*2,3,1*> . x) = <*3,1,2*> . 3 by FINSEQ_1:45
.= 2 by FINSEQ_1:45
.= (id {1,2,3}) . x by A2, A4, A6, FUNCT_1:18 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A4, FUNCT_1:12; ::_thesis: verum
end;
supposeA7: x = 3 ; ::_thesis: (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x
then <*3,1,2*> . (<*2,3,1*> . x) = <*3,1,2*> . 1 by FINSEQ_1:45
.= 3 by FINSEQ_1:45
.= (id {1,2,3}) . x by A2, A4, A7, FUNCT_1:18 ;
hence (<*3,1,2*> * <*2,3,1*>) . x = (id {1,2,3}) . x by A4, FUNCT_1:12; ::_thesis: verum
end;
end;
end;
( <*2,3,1*> is one-to-one & dom (<*3,1,2*> * <*2,3,1*>) = dom (id {1,2,3}) ) by A2, FINSEQ_3:95, RELAT_1:45;
hence <*2,3,1*> " = <*3,1,2*> by A1, A3, FUNCT_1:2, FUNCT_1:41; ::_thesis: verum
end;
theorem :: MATRIX_9:29
for a being Element of (Group_of_Perm 3) st a = <*2,3,1*> holds
a " = <*3,1,2*>
proof
let a be Element of (Group_of_Perm 3); ::_thesis: ( a = <*2,3,1*> implies a " = <*3,1,2*> )
reconsider a1 = a as Element of Permutations 3 by MATRIX_2:def_10;
assume a = <*2,3,1*> ; ::_thesis: a " = <*3,1,2*>
then a1 " = <*3,1,2*> by Th28;
hence a " = <*3,1,2*> by MATRIX_7:27; ::_thesis: verum
end;
begin
theorem Th30: :: MATRIX_9:30
for p being Permutation of (Seg 3) st p = <*1,3,2*> holds
p is being_transposition
proof
let p be Permutation of (Seg 3); ::_thesis: ( p = <*1,3,2*> implies p is being_transposition )
assume A1: p = <*1,3,2*> ; ::_thesis: p is being_transposition
then A2: dom p = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
proof
take i = 2; ::_thesis: ex j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
take j = 3; ::_thesis: ( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
thus ( i in dom p & j in dom p ) by A2, ENUMSET1:def_1; ::_thesis: ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k
proof
let k be Nat; ::_thesis: ( k <> i & k <> j & k in dom p implies p . k = k )
assume ( k <> i & k <> j & k in dom p ) ; ::_thesis: p . k = k
then k = 1 by A2, ENUMSET1:def_1;
hence p . k = k by A1, FINSEQ_1:45; ::_thesis: verum
end;
hence ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) by A1, FINSEQ_1:45; ::_thesis: verum
end;
hence p is being_transposition by MATRIX_2:def_11; ::_thesis: verum
end;
theorem Th31: :: MATRIX_9:31
for p being Permutation of (Seg 3) st p = <*2,1,3*> holds
p is being_transposition
proof
let p be Permutation of (Seg 3); ::_thesis: ( p = <*2,1,3*> implies p is being_transposition )
assume A1: p = <*2,1,3*> ; ::_thesis: p is being_transposition
then A2: dom p = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
proof
take i = 1; ::_thesis: ex j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
take j = 2; ::_thesis: ( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
thus ( i in dom p & j in dom p ) by A2, ENUMSET1:def_1; ::_thesis: ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k
proof
let k be Nat; ::_thesis: ( k <> i & k <> j & k in dom p implies p . k = k )
assume ( k <> i & k <> j & k in dom p ) ; ::_thesis: p . k = k
then k = 3 by A2, ENUMSET1:def_1;
hence p . k = k by A1, FINSEQ_1:45; ::_thesis: verum
end;
hence ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) by A1, FINSEQ_1:45; ::_thesis: verum
end;
hence p is being_transposition by MATRIX_2:def_11; ::_thesis: verum
end;
theorem :: MATRIX_9:32
for p being Permutation of (Seg 3) st p = <*3,2,1*> holds
p is being_transposition
proof
let p be Permutation of (Seg 3); ::_thesis: ( p = <*3,2,1*> implies p is being_transposition )
assume A1: p = <*3,2,1*> ; ::_thesis: p is being_transposition
then A2: dom p = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
proof
take i = 1; ::_thesis: ex j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
take j = 3; ::_thesis: ( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
thus ( i in dom p & j in dom p ) by A2, ENUMSET1:def_1; ::_thesis: ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )
for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k
proof
let k be Nat; ::_thesis: ( k <> i & k <> j & k in dom p implies p . k = k )
assume ( k <> i & k <> j & k in dom p ) ; ::_thesis: p . k = k
then k = 2 by A2, ENUMSET1:def_1;
hence p . k = k by A1, FINSEQ_1:45; ::_thesis: verum
end;
hence ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) by A1, FINSEQ_1:45; ::_thesis: verum
end;
hence p is being_transposition by MATRIX_2:def_11; ::_thesis: verum
end;
theorem Th33: :: MATRIX_9:33
for n being Nat
for p being Permutation of (Seg n) st p = id (Seg n) holds
not p is being_transposition
proof
let n be Nat; ::_thesis: for p being Permutation of (Seg n) st p = id (Seg n) holds
not p is being_transposition
let p be Permutation of (Seg n); ::_thesis: ( p = id (Seg n) implies not p is being_transposition )
assume A1: p = id (Seg n) ; ::_thesis: not p is being_transposition
then dom p = Seg n by FUNCT_1:17;
then for i, j being Nat holds
( not i in dom p or not j in dom p or not i <> j or not p . i = j or not p . j = i or ex k being Nat st
( k <> i & k <> j & k in dom p & not p . k = k ) ) by A1, FUNCT_1:17;
hence not p is being_transposition by MATRIX_2:def_11; ::_thesis: verum
end;
theorem Th34: :: MATRIX_9:34
for p being Permutation of (Seg 3) st p = <*3,1,2*> holds
not p is being_transposition
proof
let p be Permutation of (Seg 3); ::_thesis: ( p = <*3,1,2*> implies not p is being_transposition )
assume A1: p = <*3,1,2*> ; ::_thesis: not p is being_transposition
then A2: dom p = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
for i, j being Nat holds
( not i in dom p or not j in dom p or not i <> j or not p . i = j or not p . j = i or ex k being Nat st
( k <> i & k <> j & k in dom p & not p . k = k ) )
proof
given i, j being Nat such that A3: i in dom p and
A4: ( j in dom p & i <> j ) and
p . i = j and
p . j = i and
A5: for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ; ::_thesis: contradiction
ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
proof
A6: ( i = 1 or i = 2 or i = 3 ) by A2, A3, ENUMSET1:def_1;
percases ( ( i = 1 & j = 2 ) or ( i = 2 & j = 3 ) or ( i = 1 & j = 3 ) or ( i = 2 & j = 1 ) or ( i = 3 & j = 1 ) or ( i = 3 & j = 2 ) ) by A2, A4, A6, ENUMSET1:def_1;
supposeA7: ( i = 1 & j = 2 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 3 ; ::_thesis: ( 3 <> i & 3 <> j & 3 in dom p )
thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A7, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA8: ( i = 2 & j = 3 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 1 ; ::_thesis: ( 1 <> i & 1 <> j & 1 in dom p )
thus ( 1 <> i & 1 <> j & 1 in dom p ) by A2, A8, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA9: ( i = 1 & j = 3 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 2 ; ::_thesis: ( 2 <> i & 2 <> j & 2 in dom p )
thus ( 2 <> i & 2 <> j & 2 in dom p ) by A2, A9, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA10: ( i = 2 & j = 1 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 3 ; ::_thesis: ( 3 <> i & 3 <> j & 3 in dom p )
thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A10, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA11: ( i = 3 & j = 1 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 2 ; ::_thesis: ( 2 <> i & 2 <> j & 2 in dom p )
thus ( 2 <> i & 2 <> j & 2 in dom p ) by A2, A11, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA12: ( i = 3 & j = 2 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 1 ; ::_thesis: ( 1 <> i & 1 <> j & 1 in dom p )
thus ( 1 <> i & 1 <> j & 1 in dom p ) by A2, A12, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
then consider k being Nat such that
A13: ( k <> i & k <> j ) and
A14: k in dom p ;
A15: p . k = k by A5, A13, A14;
percases ( k = 1 or k = 2 or k = 3 ) by A2, A14, ENUMSET1:def_1;
suppose k = 1 ; ::_thesis: contradiction
hence contradiction by A1, A15, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: contradiction
hence contradiction by A1, A15, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 3 ; ::_thesis: contradiction
hence contradiction by A1, A15, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
hence not p is being_transposition by MATRIX_2:def_11; ::_thesis: verum
end;
theorem Th35: :: MATRIX_9:35
for p being Permutation of (Seg 3) st p = <*2,3,1*> holds
not p is being_transposition
proof
let p be Permutation of (Seg 3); ::_thesis: ( p = <*2,3,1*> implies not p is being_transposition )
assume A1: p = <*2,3,1*> ; ::_thesis: not p is being_transposition
then A2: dom p = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
for i, j being Nat holds
( not i in dom p or not j in dom p or not i <> j or not p . i = j or not p . j = i or ex k being Nat st
( k <> i & k <> j & k in dom p & not p . k = k ) )
proof
given i, j being Nat such that A3: i in dom p and
A4: ( j in dom p & i <> j ) and
p . i = j and
p . j = i and
A5: for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ; ::_thesis: contradiction
ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
proof
A6: ( i = 1 or i = 2 or i = 3 ) by A2, A3, ENUMSET1:def_1;
percases ( ( i = 1 & j = 2 ) or ( i = 2 & j = 3 ) or ( i = 1 & j = 3 ) or ( i = 2 & j = 1 ) or ( i = 3 & j = 1 ) or ( i = 3 & j = 2 ) ) by A2, A4, A6, ENUMSET1:def_1;
supposeA7: ( i = 1 & j = 2 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 3 ; ::_thesis: ( 3 <> i & 3 <> j & 3 in dom p )
thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A7, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA8: ( i = 2 & j = 3 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 1 ; ::_thesis: ( 1 <> i & 1 <> j & 1 in dom p )
thus ( 1 <> i & 1 <> j & 1 in dom p ) by A2, A8, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA9: ( i = 1 & j = 3 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 2 ; ::_thesis: ( 2 <> i & 2 <> j & 2 in dom p )
thus ( 2 <> i & 2 <> j & 2 in dom p ) by A2, A9, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA10: ( i = 2 & j = 1 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 3 ; ::_thesis: ( 3 <> i & 3 <> j & 3 in dom p )
thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A10, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA11: ( i = 3 & j = 1 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 2 ; ::_thesis: ( 2 <> i & 2 <> j & 2 in dom p )
thus ( 2 <> i & 2 <> j & 2 in dom p ) by A2, A11, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA12: ( i = 3 & j = 2 ) ; ::_thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )
take 1 ; ::_thesis: ( 1 <> i & 1 <> j & 1 in dom p )
thus ( 1 <> i & 1 <> j & 1 in dom p ) by A2, A12, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
then consider k being Nat such that
A13: ( k <> i & k <> j ) and
A14: k in dom p ;
A15: p . k = k by A5, A13, A14;
percases ( k = 1 or k = 2 or k = 3 ) by A2, A14, ENUMSET1:def_1;
suppose k = 1 ; ::_thesis: contradiction
hence contradiction by A1, A15, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: contradiction
hence contradiction by A1, A15, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 3 ; ::_thesis: contradiction
hence contradiction by A1, A15, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
hence not p is being_transposition by MATRIX_2:def_11; ::_thesis: verum
end;
begin
theorem Th36: :: MATRIX_9:36
for n being Nat
for f being Permutation of (Seg n) holds f is FinSequence of Seg n
proof
let n be Nat; ::_thesis: for f being Permutation of (Seg n) holds f is FinSequence of Seg n
let f be Permutation of (Seg n); ::_thesis: f is FinSequence of Seg n
A1: rng f c= Seg n by RELAT_1:def_19;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: f is FinSequence of Seg n
hence f is FinSequence of Seg n by A1, FINSEQ_1:def_4; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: f is FinSequence of Seg n
then dom f = Seg n by FUNCT_2:def_1;
then f is FinSequence by FINSEQ_1:def_2;
hence f is FinSequence of Seg n by A1, FINSEQ_1:def_4; ::_thesis: verum
end;
end;
end;
theorem Th37: :: MATRIX_9:37
( <*2,1,3*> * <*1,3,2*> = <*2,3,1*> & <*1,3,2*> * <*2,1,3*> = <*3,1,2*> & <*2,1,3*> * <*3,2,1*> = <*3,1,2*> & <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
proof
set F = <*2,3,1*>;
set G = <*3,1,2*>;
set f = <*1,3,2*>;
set g = <*2,1,3*>;
set h = <*3,2,1*>;
A1: dom <*1,3,2*> = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
then A2: 1 in dom <*1,3,2*> by ENUMSET1:def_1;
A3: <*1,3,2*> is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
A4: <*2,1,3*> is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
A5: 2 in dom <*1,3,2*> by A1, ENUMSET1:def_1;
A6: dom <*3,1,2*> = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
then A7: 1 in dom <*3,1,2*> by ENUMSET1:def_1;
A8: 3 in dom <*3,1,2*> by A6, ENUMSET1:def_1;
A9: 2 in dom <*3,1,2*> by A6, ENUMSET1:def_1;
A10: 3 in dom <*1,3,2*> by A1, ENUMSET1:def_1;
A11: dom <*2,1,3*> = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
then A12: 1 in dom <*2,1,3*> by ENUMSET1:def_1;
A13: 3 in dom <*2,1,3*> by A11, ENUMSET1:def_1;
A14: 2 in dom <*2,1,3*> by A11, ENUMSET1:def_1;
A15: dom <*3,2,1*> = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
then A16: 1 in dom <*3,2,1*> by ENUMSET1:def_1;
A17: 3 in dom <*3,2,1*> by A15, ENUMSET1:def_1;
A18: 2 in dom <*3,2,1*> by A15, ENUMSET1:def_1;
A19: <*1,3,2*> is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
A20: <*3,1,2*> is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
A21: dom <*2,3,1*> = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89;
then A22: 1 in dom <*2,3,1*> by ENUMSET1:def_1;
A23: 3 in dom <*2,3,1*> by A21, ENUMSET1:def_1;
A24: 2 in dom <*2,3,1*> by A21, ENUMSET1:def_1;
A25: <*3,2,1*> is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
A26: <*2,3,1*> is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
then reconsider f = <*1,3,2*>, g = <*2,1,3*>, h = <*3,2,1*>, F = <*2,3,1*>, G = <*3,1,2*> as FinSequence of Seg 3 by A4, A25, A20, A19, Th36;
A27: 3 = len g by FINSEQ_1:45;
then reconsider gf = g * f as FinSequence of Seg 3 by A3, FINSEQ_2:46;
A28: gf . 1 = g . (f . 1) by A2, FUNCT_1:13
.= g . 1 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A29: g is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
then reconsider gg = g * g as FinSequence of Seg 3 by A27, FINSEQ_2:46;
A30: gg . 1 = g . (g . 1) by A12, FUNCT_1:13
.= g . 2 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A31: 3 = len f by FINSEQ_1:45;
then reconsider fg = f * g as FinSequence of Seg 3 by A4, FINSEQ_2:46;
A32: fg . 2 = f . (g . 2) by A14, FUNCT_1:13
.= f . 1 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A33: gf . 3 = g . (f . 3) by A10, FUNCT_1:13
.= g . 2 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A34: gf . 2 = g . (f . 2) by A5, FUNCT_1:13
.= g . 3 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A35: f is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
then reconsider ff = f * f as FinSequence of Seg 3 by A31, FINSEQ_2:46;
len gf = 3 by A27, A35, FINSEQ_2:43;
hence <*2,1,3*> * <*1,3,2*> = <*2,3,1*> by A28, A34, A33, FINSEQ_1:45; ::_thesis: ( <*1,3,2*> * <*2,1,3*> = <*3,1,2*> & <*2,1,3*> * <*3,2,1*> = <*3,1,2*> & <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A36: fg . 1 = f . (g . 1) by A12, FUNCT_1:13
.= f . 2 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A37: fg . 3 = f . (g . 3) by A13, FUNCT_1:13
.= f . 3 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
len fg = 3 by A31, A29, FINSEQ_2:43;
hence <*1,3,2*> * <*2,1,3*> = <*3,1,2*> by A36, A32, A37, FINSEQ_1:45; ::_thesis: ( <*2,1,3*> * <*3,2,1*> = <*3,1,2*> & <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A38: ff . 2 = f . (f . 2) by A5, FUNCT_1:13
.= f . 3 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A39: gg . 3 = g . (g . 3) by A13, FUNCT_1:13
.= g . 3 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A40: gg . 2 = g . (g . 2) by A14, FUNCT_1:13
.= g . 1 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A41: h is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
then reconsider gh = g * h as FinSequence of Seg 3 by A27, FINSEQ_2:46;
A42: gh . 1 = g . (h . 1) by A16, FUNCT_1:13
.= g . 3 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A43: gh . 3 = g . (h . 3) by A17, FUNCT_1:13
.= g . 1 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A44: gh . 2 = g . (h . 2) by A18, FUNCT_1:13
.= g . 2 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A45: 3 = len h by FINSEQ_1:45;
then reconsider hf = h * f as FinSequence of Seg 3 by A19, FINSEQ_2:46;
reconsider hh = h * h as FinSequence of Seg 3 by A45, A41, FINSEQ_2:46;
A46: hh . 1 = h . (h . 1) by A16, FUNCT_1:13
.= h . 3 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
reconsider fh = f * h as FinSequence of Seg 3 by A25, A31, FINSEQ_2:46;
A47: fh . 1 = f . (h . 1) by A16, FUNCT_1:13
.= f . 3 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A48: fh . 3 = f . (h . 3) by A17, FUNCT_1:13
.= f . 1 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
reconsider fF = f * F as FinSequence of Seg 3 by A26, A31, FINSEQ_2:46;
A49: fF . 1 = f . (F . 1) by A22, FUNCT_1:13
.= f . 2 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A50: fF . 2 = f . (F . 2) by A24, FUNCT_1:13
.= f . 3 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
reconsider hg = h * g as FinSequence of Seg 3 by A45, A29, FINSEQ_2:46;
A51: hg . 1 = h . (g . 1) by A12, FUNCT_1:13
.= h . 2 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A52: hg . 2 = h . (g . 2) by A14, FUNCT_1:13
.= h . 1 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A53: hh . 3 = h . (h . 3) by A17, FUNCT_1:13
.= h . 1 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A54: hh . 2 = h . (h . 2) by A18, FUNCT_1:13
.= h . 2 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
len gh = 3 by A27, A41, FINSEQ_2:43;
hence <*2,1,3*> * <*3,2,1*> = <*3,1,2*> by A42, A44, A43, FINSEQ_1:45; ::_thesis: ( <*3,2,1*> * <*2,1,3*> = <*2,3,1*> & <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A55: ff . 3 = f . (f . 3) by A10, FUNCT_1:13
.= f . 2 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A56: hg . 3 = h . (g . 3) by A13, FUNCT_1:13
.= h . 3 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
len hg = 3 by A45, A29, FINSEQ_2:43;
hence <*3,2,1*> * <*2,1,3*> = <*2,3,1*> by A51, A52, A56, FINSEQ_1:45; ::_thesis: ( <*3,2,1*> * <*3,2,1*> = <*1,2,3*> & <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
len hh = 3 by A45, A41, FINSEQ_2:43;
hence <*3,2,1*> * <*3,2,1*> = <*1,2,3*> by A46, A54, A53, FINSEQ_1:45; ::_thesis: ( <*2,1,3*> * <*2,1,3*> = <*1,2,3*> & <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
len gg = 3 by A27, A29, FINSEQ_2:43;
hence <*2,1,3*> * <*2,1,3*> = <*1,2,3*> by A30, A40, A39, FINSEQ_1:45; ::_thesis: ( <*1,3,2*> * <*1,3,2*> = <*1,2,3*> & <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A57: ff . 1 = f . (f . 1) by A2, FUNCT_1:13
.= f . 1 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A58: fF . 3 = f . (F . 3) by A23, FUNCT_1:13
.= f . 1 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
len ff = 3 by A31, A35, FINSEQ_2:43;
hence <*1,3,2*> * <*1,3,2*> = <*1,2,3*> by A57, A38, A55, FINSEQ_1:45; ::_thesis: ( <*1,3,2*> * <*2,3,1*> = <*3,2,1*> & <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A59: F is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
then len fF = 3 by A31, FINSEQ_2:43;
hence <*1,3,2*> * <*2,3,1*> = <*3,2,1*> by A49, A50, A58, FINSEQ_1:45; ::_thesis: ( <*2,3,1*> * <*2,3,1*> = <*3,1,2*> & <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A60: fh . 2 = f . (h . 2) by A18, FUNCT_1:13
.= f . 2 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A61: 3 = len F by FINSEQ_1:45;
then reconsider FF = F * F as FinSequence of Seg 3 by A26, FINSEQ_2:46;
reconsider FG = F * G as FinSequence of Seg 3 by A20, A61, FINSEQ_2:46;
A62: FG . 1 = F . (G . 1) by A7, FUNCT_1:13
.= F . 3 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A63: FG . 2 = F . (G . 2) by A9, FUNCT_1:13
.= F . 1 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A64: FF . 3 = F . (F . 3) by A23, FUNCT_1:13
.= F . 1 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A65: FG . 3 = F . (G . 3) by A8, FUNCT_1:13
.= F . 2 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A66: FF . 2 = F . (F . 2) by A24, FUNCT_1:13
.= F . 3 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A67: FF . 1 = F . (F . 1) by A22, FUNCT_1:13
.= F . 2 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A68: 3 = len G by FINSEQ_1:45;
then reconsider GF = G * F as FinSequence of Seg 3 by A26, FINSEQ_2:46;
reconsider GG = G * G as FinSequence of Seg 3 by A20, A68, FINSEQ_2:46;
A69: GG . 1 = G . (G . 1) by A7, FUNCT_1:13
.= G . 3 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A70: GG . 2 = G . (G . 2) by A9, FUNCT_1:13
.= G . 1 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A71: GF . 3 = G . (F . 3) by A23, FUNCT_1:13
.= G . 1 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
A72: GG . 3 = G . (G . 3) by A8, FUNCT_1:13
.= G . 2 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
A73: GF . 2 = G . (F . 2) by A24, FUNCT_1:13
.= G . 3 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
A74: GF . 1 = G . (F . 1) by A22, FUNCT_1:13
.= G . 2 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
len FF = 3 by A61, A59, FINSEQ_2:43;
hence <*2,3,1*> * <*2,3,1*> = <*3,1,2*> by A67, A66, A64, FINSEQ_1:45; ::_thesis: ( <*2,3,1*> * <*3,1,2*> = <*1,2,3*> & <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A75: G is Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
then len FG = 3 by A61, FINSEQ_2:43;
hence <*2,3,1*> * <*3,1,2*> = <*1,2,3*> by A62, A63, A65, FINSEQ_1:45; ::_thesis: ( <*3,1,2*> * <*2,3,1*> = <*1,2,3*> & <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A76: hf . 3 = h . (f . 3) by A10, FUNCT_1:13
.= h . 2 by FINSEQ_1:45
.= 2 by FINSEQ_1:45 ;
len GF = 3 by A68, A59, FINSEQ_2:43;
hence <*3,1,2*> * <*2,3,1*> = <*1,2,3*> by A74, A73, A71, FINSEQ_1:45; ::_thesis: ( <*3,1,2*> * <*3,1,2*> = <*2,3,1*> & <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
len GG = 3 by A68, A75, FINSEQ_2:43;
hence <*3,1,2*> * <*3,1,2*> = <*2,3,1*> by A69, A70, A72, FINSEQ_1:45; ::_thesis: ( <*1,3,2*> * <*3,2,1*> = <*2,3,1*> & <*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
A77: hf . 2 = h . (f . 2) by A5, FUNCT_1:13
.= h . 3 by FINSEQ_1:45
.= 1 by FINSEQ_1:45 ;
len fh = 3 by A31, A41, FINSEQ_2:43;
hence <*1,3,2*> * <*3,2,1*> = <*2,3,1*> by A47, A60, A48, FINSEQ_1:45; ::_thesis: <*3,2,1*> * <*1,3,2*> = <*3,1,2*>
A78: hf . 1 = h . (f . 1) by A2, FUNCT_1:13
.= h . 1 by FINSEQ_1:45
.= 3 by FINSEQ_1:45 ;
len hf = 3 by A45, A35, FINSEQ_2:43;
hence <*3,2,1*> * <*1,3,2*> = <*3,1,2*> by A78, A77, A76, FINSEQ_1:45; ::_thesis: verum
end;
theorem Th38: :: MATRIX_9:38
for p being Permutation of (Seg 3) holds
( not p is being_transposition or p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )
proof
let p be Permutation of (Seg 3); ::_thesis: ( not p is being_transposition or p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )
p in Permutations 3 by MATRIX_2:def_9;
then A1: ( p = <*1,2,3*> or p = <*2,1,3*> or p = <*2,3,1*> or p = <*3,1,2*> or p = <*3,2,1*> or p = <*1,3,2*> ) by Th19, ENUMSET1:def_4;
assume p is being_transposition ; ::_thesis: ( p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> )
hence ( p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*> ) by A1, Th33, Th34, Th35, FINSEQ_2:53; ::_thesis: verum
end;
theorem Th39: :: MATRIX_9:39
for n being Nat
for f, g being Element of Permutations n holds f * g in Permutations n
proof
let n be Nat; ::_thesis: for f, g being Element of Permutations n holds f * g in Permutations n
let f, g be Element of Permutations n; ::_thesis: f * g in Permutations n
reconsider F = f, G = g as Permutation of (Seg n) by MATRIX_2:def_9;
F * G is Permutation of (Seg n) ;
hence f * g in Permutations n by MATRIX_2:def_9; ::_thesis: verum
end;
Lm12: <*1,2,3*> is even Permutation of (Seg 3)
by FINSEQ_2:53, MATRIX_2:25;
Lm13: <*2,3,1*> is even Permutation of (Seg 3)
proof
reconsider f = <*2,3,1*> as Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
ex l being FinSequence of (Group_of_Perm 3) st
( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) )
proof
reconsider l1 = <*2,1,3*>, l2 = <*1,3,2*> as Element of (Group_of_Perm 3) by Th27, MATRIX_2:def_10;
reconsider l = <*l2,l1*> as FinSequence of (Group_of_Perm 3) ;
take l ; ::_thesis: ( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) )
A1: len l = 2 * 1 by FINSEQ_1:44;
hence (len l) mod 2 = 0 by NAT_D:13; ::_thesis: ( f = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) )
reconsider L2 = l2, L1 = l1 as Element of Permutations 3 by Th27;
Product l = l2 * l1 by GROUP_4:10
.= L1 * L2 by MATRIX_2:def_10
.= <*2,3,1*> by Th37 ;
hence f = Product l ; ::_thesis: for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
A2: dom l = {1,2} by A1, FINSEQ_1:2, FINSEQ_1:def_3;
for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
proof
let i be Nat; ::_thesis: ( i in dom l implies ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) )
assume A3: i in dom l ; ::_thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
percases ( i = 2 or i = 1 ) by A2, A3, TARSKI:def_2;
supposeA4: i = 2 ; ::_thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
then reconsider q = l . i as Element of Permutations 3 by Th27, FINSEQ_1:44;
A5: len (Permutations 3) = 3 by MATRIX_2:18;
l . i = <*2,1,3*> by A4, FINSEQ_1:44;
then q is being_transposition by A5, Th31;
hence ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: verum
end;
supposeA6: i = 1 ; ::_thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
then reconsider q = l . i as Element of Permutations 3 by Th27, FINSEQ_1:44;
A7: len (Permutations 3) = 3 by MATRIX_2:18;
l . i = <*1,3,2*> by A6, FINSEQ_1:44;
then q is being_transposition by A7, Th30;
hence ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: verum
end;
end;
end;
hence for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: verum
end;
hence <*2,3,1*> is even Permutation of (Seg 3) by MATRIX_2:def_12; ::_thesis: verum
end;
Lm14: <*3,1,2*> is even Permutation of (Seg 3)
proof
reconsider f = <*3,1,2*> as Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
ex l being FinSequence of (Group_of_Perm 3) st
( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) )
proof
reconsider l1 = <*2,1,3*>, l2 = <*1,3,2*> as Element of (Group_of_Perm 3) by Th27, MATRIX_2:def_10;
reconsider l = <*l1,l2*> as FinSequence of (Group_of_Perm 3) ;
take l ; ::_thesis: ( (len l) mod 2 = 0 & f = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) )
A1: len l = 2 * 1 by FINSEQ_1:44;
hence (len l) mod 2 = 0 by NAT_D:13; ::_thesis: ( f = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) )
reconsider L2 = l2, L1 = l1 as Element of Permutations 3 by Th27;
Product l = l1 * l2 by GROUP_4:10
.= L2 * L1 by MATRIX_2:def_10
.= <*3,1,2*> by Th37 ;
hence f = Product l ; ::_thesis: for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
A2: dom l = {1,2} by A1, FINSEQ_1:2, FINSEQ_1:def_3;
for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
proof
let i be Nat; ::_thesis: ( i in dom l implies ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) )
assume A3: i in dom l ; ::_thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
percases ( i = 2 or i = 1 ) by A2, A3, TARSKI:def_2;
supposeA4: i = 2 ; ::_thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
then reconsider q = l . i as Element of Permutations 3 by Th27, FINSEQ_1:44;
A5: len (Permutations 3) = 3 by MATRIX_2:18;
l . i = <*1,3,2*> by A4, FINSEQ_1:44;
then q is being_transposition by A5, Th30;
hence ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: verum
end;
supposeA6: i = 1 ; ::_thesis: ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition )
then reconsider q = l . i as Element of Permutations 3 by Th27, FINSEQ_1:44;
A7: len (Permutations 3) = 3 by MATRIX_2:18;
l . i = <*2,1,3*> by A6, FINSEQ_1:44;
then q is being_transposition by A7, Th31;
hence ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: verum
end;
end;
end;
hence for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: verum
end;
hence <*3,1,2*> is even Permutation of (Seg 3) by MATRIX_2:def_12; ::_thesis: verum
end;
theorem :: MATRIX_9:40
for n being Nat
for l being FinSequence of (Group_of_Perm n) st (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) holds
Product l is even Permutation of (Seg n)
proof
let n be Nat; ::_thesis: for l being FinSequence of (Group_of_Perm n) st (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) holds
Product l is even Permutation of (Seg n)
let l be FinSequence of (Group_of_Perm n); ::_thesis: ( (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) implies Product l is even Permutation of (Seg n) )
Product l in the carrier of (Group_of_Perm n) ;
then Product l in Permutations n by MATRIX_2:def_10;
then reconsider Pf = Product l as Permutation of (Seg n) by MATRIX_2:def_9;
assume A1: ( (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) ) ; ::_thesis: Product l is even Permutation of (Seg n)
ex l being FinSequence of the carrier of (Group_of_Perm n) st
( (len l) mod 2 = 0 & Pf = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) )
proof
consider l being FinSequence of the carrier of (Group_of_Perm n) such that
A2: ( (len l) mod 2 = 0 & Pf = Product l ) and
A3: for i being Element of NAT st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) by A1;
take l ; ::_thesis: ( (len l) mod 2 = 0 & Pf = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) )
thus ( (len l) mod 2 = 0 & Pf = Product l ) by A2; ::_thesis: for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition )
let i be Nat; ::_thesis: ( i in dom l implies ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) )
thus ( i in dom l implies ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) by A3; ::_thesis: verum
end;
hence Product l is even Permutation of (Seg n) by MATRIX_2:def_12; ::_thesis: verum
end;
Lm15: for p being Permutation of (Seg 3) holds p * <*1,2,3*> = p
proof
let p be Permutation of (Seg 3); ::_thesis: p * <*1,2,3*> = p
p is Element of Permutations 3 by MATRIX_2:def_9;
hence p * <*1,2,3*> = p by FINSEQ_2:53, MATRIX_2:21; ::_thesis: verum
end;
Lm16: for p being Permutation of (Seg 3) holds <*1,2,3*> * p = p
proof
let p be Permutation of (Seg 3); ::_thesis: <*1,2,3*> * p = p
p is Element of Permutations 3 by MATRIX_2:def_9;
hence <*1,2,3*> * p = p by FINSEQ_2:53, MATRIX_2:21; ::_thesis: verum
end;
theorem Th41: :: MATRIX_9:41
for l being FinSequence of (Group_of_Perm 3) st (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> holds
Product l = <*3,1,2*>
proof
defpred S1[ Nat] means for f being FinSequence of (Group_of_Perm 3) st len f = 2 * $1 & ( for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ) & not Product f = <*1,2,3*> & not Product f = <*2,3,1*> holds
Product f = <*3,1,2*>;
let l be FinSequence of (Group_of_Perm 3); ::_thesis: ( (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> implies Product l = <*3,1,2*> )
assume that
A1: (len l) mod 2 = 0 and
A2: for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> )
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
let f be FinSequence of (Group_of_Perm 3); ::_thesis: ( len f = 2 * (k + 1) & ( for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ) & not Product f = <*1,2,3*> & not Product f = <*2,3,1*> implies Product f = <*3,1,2*> )
assume that
A5: len f = 2 * (k + 1) and
A6: for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
reconsider k = k as Element of NAT by ORDINAL1:def_12;
set l = 2 * k;
A7: 1 <= (2 * k) + 1 by NAT_1:11;
rng (f | (Seg (2 * k))) c= the carrier of (Group_of_Perm 3) by RELAT_1:def_19;
then reconsider g = f | (Seg (2 * k)) as FinSequence of (Group_of_Perm 3) by FINSEQ_1:def_4;
A8: 2 * k <= (2 * k) + 1 by NAT_1:11;
A9: (f | (Seg ((2 * k) + 1))) | (Seg (2 * k)) = (f | ((2 * k) + 1)) | (2 * k)
.= f | (2 * k) by A8, FINSEQ_5:77
.= f | (Seg (2 * k)) ;
A10: dom g c= dom f by RELAT_1:60;
A11: for i being Element of NAT st i in dom g holds
ex q being Element of Permutations 3 st
( g . i = q & q is being_transposition )
proof
let i be Element of NAT ; ::_thesis: ( i in dom g implies ex q being Element of Permutations 3 st
( g . i = q & q is being_transposition ) )
assume A12: i in dom g ; ::_thesis: ex q being Element of Permutations 3 st
( g . i = q & q is being_transposition )
then consider q being Element of Permutations 3 such that
A13: ( f . i = q & q is being_transposition ) by A6, A10;
take q ; ::_thesis: ( g . i = q & q is being_transposition )
thus ( g . i = q & q is being_transposition ) by A12, A13, FUNCT_1:47; ::_thesis: verum
end;
set h = f | (Seg ((2 * k) + 1));
len f = ((2 * k) + 1) + 1 by A5;
then len (f | (Seg ((2 * k) + 1))) = (2 * k) + 1 by FINSEQ_3:53;
then A14: f | (Seg ((2 * k) + 1)) = ((f | (Seg ((2 * k) + 1))) | (Seg (2 * k))) ^ <*((f | (Seg ((2 * k) + 1))) . ((2 * k) + 1))*> by FINSEQ_3:55;
A15: dom f = Seg (2 * (k + 1)) by A5, FINSEQ_1:def_3;
(2 * k) + 1 <= (2 * k) + 2 by XREAL_1:6;
then 1 <= (2 * k) + 2 by A7, XXREAL_0:2;
then A16: (2 * k) + 2 in dom f by A15;
then consider q1 being Element of Permutations 3 such that
A17: f . ((2 * k) + 2) = q1 and
A18: q1 is being_transposition by A6;
A19: f . (((2 * k) + 1) + 1) = f /. ((2 * k) + 2) by A16, PARTFUN1:def_6;
(2 * k) + 1 <= (2 * k) + 2 by XREAL_1:6;
then A20: (2 * k) + 1 in dom f by A15, A7;
then consider q2 being Element of Permutations 3 such that
A21: f . ((2 * k) + 1) = q2 and
A22: q2 is being_transposition by A6;
reconsider q12 = q1 * q2 as Element of Permutations 3 by Th39;
(f | (Seg ((2 * k) + 1))) . ((2 * k) + 1) = f . ((2 * k) + 1) by FINSEQ_1:4, FUNCT_1:49;
then A23: (f | (Seg ((2 * k) + 1))) . ((2 * k) + 1) = f /. ((2 * k) + 1) by A20, PARTFUN1:def_6;
f = (f | (Seg ((2 * k) + 1))) ^ <*(f . (((2 * k) + 1) + 1))*> by A5, FINSEQ_3:55;
then f = g ^ (<*(f /. ((2 * k) + 1))*> ^ <*(f /. ((2 * k) + 2))*>) by A14, A9, A23, A19, FINSEQ_1:32;
then A24: Product f = (Product g) * (Product (<*(f /. ((2 * k) + 1))*> ^ <*(f /. ((2 * k) + 2))*>)) by GROUP_4:5
.= (Product g) * ((Product <*(f /. ((2 * k) + 1))*>) * (f /. ((2 * k) + 2))) by GROUP_4:6
.= (Product g) * ((f /. ((2 * k) + 1)) * (f /. ((2 * k) + 2))) by GROUP_4:9 ;
reconsider Pg = Product g as Element of Permutations 3 by MATRIX_2:def_10;
Product g in the carrier of (Group_of_Perm 3) ;
then Product g in Permutations 3 by MATRIX_2:def_10;
then A25: Product g is Permutation of (Seg 3) by MATRIX_2:def_9;
A26: len (Permutations 3) = 3 by MATRIX_2:18;
then A27: ( q1 = <*2,1,3*> or q1 = <*1,3,2*> or q1 = <*3,2,1*> ) by A18, Th38;
A28: q1 = f /. ((2 * k) + 2) by A16, A17, PARTFUN1:def_6;
q1 * q2 in Permutations 3 by Th39;
then A29: q1 * q2 is Permutation of (Seg 3) by MATRIX_2:def_9;
q2 = f /. ((2 * k) + 1) by A20, A21, PARTFUN1:def_6;
then A30: (f /. ((2 * k) + 1)) * (f /. ((2 * k) + 2)) = q1 * q2 by A28, MATRIX_7:9;
then A31: Product f = q12 * Pg by A24, MATRIX_7:9;
2 * k <= (2 * k) + 2 by NAT_1:11;
then Seg (2 * k) c= Seg (2 * (k + 1)) by FINSEQ_1:5;
then dom g = Seg (2 * k) by A15, RELAT_1:62;
then A32: len g = 2 * k by FINSEQ_1:def_3;
then A33: ( Product g = <*1,2,3*> or Product g = <*2,3,1*> or Product g = <*3,1,2*> ) by A4, A11;
( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
proof
percases ( ( Pg = <*1,2,3*> & q1 * q2 = <*2,3,1*> ) or ( Pg = <*2,3,1*> & q1 * q2 = <*2,3,1*> ) or ( Pg = <*2,3,1*> & q1 * q2 = <*3,1,2*> ) or q1 * q2 = <*1,2,3*> or ( Pg = <*1,2,3*> & q1 * q2 = <*3,1,2*> ) or ( Pg = <*3,1,2*> & q1 * q2 = <*2,3,1*> ) or ( Pg = <*3,1,2*> & q1 * q2 = <*3,1,2*> ) ) by A4, A32, A11, A22, A26, A27, Th37, Th38;
suppose ( Pg = <*1,2,3*> & q1 * q2 = <*2,3,1*> ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A29, A31, Lm15; ::_thesis: verum
end;
suppose ( Pg = <*2,3,1*> & q1 * q2 = <*2,3,1*> ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A24, A30, Th37, MATRIX_7:9; ::_thesis: verum
end;
suppose ( Pg = <*2,3,1*> & q1 * q2 = <*3,1,2*> ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A31, Th37; ::_thesis: verum
end;
suppose q1 * q2 = <*1,2,3*> ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A33, A25, A31, Lm16; ::_thesis: verum
end;
suppose ( Pg = <*1,2,3*> & q1 * q2 = <*3,1,2*> ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A29, A31, Lm15; ::_thesis: verum
end;
suppose ( Pg = <*3,1,2*> & q1 * q2 = <*2,3,1*> ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A31, Th37; ::_thesis: verum
end;
suppose ( Pg = <*3,1,2*> & q1 * q2 = <*3,1,2*> ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A24, A30, Th37, MATRIX_7:9; ::_thesis: verum
end;
end;
end;
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) ; ::_thesis: verum
end;
A34: S1[ 0 ]
proof
set G = Group_of_Perm 3;
let f be FinSequence of (Group_of_Perm 3); ::_thesis: ( len f = 2 * 0 & ( for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ) & not Product f = <*1,2,3*> & not Product f = <*2,3,1*> implies Product f = <*3,1,2*> )
assume that
A35: len f = 2 * 0 and
for i being Element of NAT st i in dom f holds
ex q being Element of Permutations 3 st
( f . i = q & q is being_transposition ) ; ::_thesis: ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> )
A36: 1_ (Group_of_Perm 3) = <*1,2,3*> by FINSEQ_2:53, MATRIX_2:24;
f = <*> the carrier of (Group_of_Perm 3) by A35;
hence ( Product f = <*1,2,3*> or Product f = <*2,3,1*> or Product f = <*3,1,2*> ) by A36, GROUP_4:8; ::_thesis: verum
end;
A37: for s being Nat holds S1[s] from NAT_1:sch_2(A34, A3);
ex t being Nat st
( len l = (2 * t) + 0 & 0 < 2 ) by A1, NAT_D:def_2;
hence ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> ) by A2, A37; ::_thesis: verum
end;
Lm17: for l being FinSequence of (Group_of_Perm 3) st (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> holds
Product l = <*3,1,2*>
proof
let l be FinSequence of (Group_of_Perm 3); ::_thesis: ( (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> implies Product l = <*3,1,2*> )
assume that
A1: (len l) mod 2 = 0 and
A2: for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ; ::_thesis: ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> )
for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) by A2;
hence ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> ) by A1, Th41; ::_thesis: verum
end;
registration
cluster Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite odd for Element of bool [:(Seg 3),(Seg 3):];
existence
ex b1 being Permutation of (Seg 3) st b1 is odd
proof
reconsider f = <*3,2,1*> as Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
for l being FinSequence of (Group_of_Perm 3) holds
( not (len l) mod 2 = 0 or not f = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 3 holds
( not l . i = q or not q is being_transposition ) ) ) ) by Lm3, Lm7, Lm17;
then f is odd by MATRIX_2:def_12;
hence ex b1 being Permutation of (Seg 3) st b1 is odd ; ::_thesis: verum
end;
end;
theorem Th42: :: MATRIX_9:42
<*3,2,1*> is odd Permutation of (Seg 3)
proof
reconsider f = <*3,2,1*> as Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
for l being FinSequence of (Group_of_Perm 3) holds
( not (len l) mod 2 = 0 or not f = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 3 holds
( not l . i = q or not q is being_transposition ) ) ) ) by Lm3, Lm7, Lm17;
hence <*3,2,1*> is odd Permutation of (Seg 3) by MATRIX_2:def_12; ::_thesis: verum
end;
theorem Th43: :: MATRIX_9:43
<*2,1,3*> is odd Permutation of (Seg 3)
proof
reconsider f = <*2,1,3*> as Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
for l being FinSequence of (Group_of_Perm 3) holds
( not (len l) mod 2 = 0 or not f = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 3 holds
( not l . i = q or not q is being_transposition ) ) ) ) by Lm5, Lm11, Lm17;
hence <*2,1,3*> is odd Permutation of (Seg 3) by MATRIX_2:def_12; ::_thesis: verum
end;
theorem Th44: :: MATRIX_9:44
<*1,3,2*> is odd Permutation of (Seg 3)
proof
reconsider f = <*1,3,2*> as Permutation of (Seg 3) by Th27, MATRIX_2:def_9;
for l being FinSequence of (Group_of_Perm 3) holds
( not (len l) mod 2 = 0 or not f = Product l or ex i being Nat st
( i in dom l & ( for q being Element of Permutations 3 holds
( not l . i = q or not q is being_transposition ) ) ) ) by Lm4, Lm9, Lm17;
hence <*1,3,2*> is odd Permutation of (Seg 3) by MATRIX_2:def_12; ::_thesis: verum
end;
theorem :: MATRIX_9:45
for p being odd Permutation of (Seg 3) holds
( p = <*3,2,1*> or p = <*1,3,2*> or p = <*2,1,3*> )
proof
let p be odd Permutation of (Seg 3); ::_thesis: ( p = <*3,2,1*> or p = <*1,3,2*> or p = <*2,1,3*> )
p in Permutations 3 by MATRIX_2:def_9;
hence ( p = <*3,2,1*> or p = <*1,3,2*> or p = <*2,1,3*> ) by Lm12, Lm13, Lm14, Th19, ENUMSET1:def_4; ::_thesis: verum
end;
begin
theorem :: MATRIX_9:46
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as Element of Permutations 3 by Th27;
reconsider id3 = idseq 3 as Permutation of (Seg 3) ;
reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_2:def_9;
A1: id3 is even by MATRIX_2:25;
reconsider rid3 = Rev (idseq 3) as Element of Permutations 3 by Th4;
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) )
assume A2: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
FinOmega (Permutations 3) = Permutations 3 by MATRIX_2:26, MATRIX_2:def_14;
then reconsider X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin (Permutations 3) by Th15, Th19, FINSEQ_2:53;
reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin (Permutations 3) ;
set F = the addF of K;
A3: ( FinOmega (Permutations 3) = X & X = {Id3,rid3,a3} \/ {a4,a5,a6} ) by Th15, Th19, ENUMSET1:13, FINSEQ_2:53, MATRIX_2:def_14;
now__::_thesis:_for_x_being_set_st_x_in_B1_holds_
x_in_B1_\_B2
let x be set ; ::_thesis: ( x in B1 implies x in B1 \ B2 )
assume A4: x in B1 ; ::_thesis: x in B1 \ B2
then ( x = Id3 or x = rid3 or x = a3 ) by ENUMSET1:def_1;
then not x in B2 by Lm5, Lm6, Lm7, Lm8, Lm9, Th15, ENUMSET1:def_1, FINSEQ_2:53;
hence x in B1 \ B2 by A4, XBOOLE_0:def_5; ::_thesis: verum
end;
then A5: B1 c= B1 \ B2 by TARSKI:def_3;
for x being set st x in B1 \ B2 holds
x in B1 by XBOOLE_0:def_5;
then B1 \ B2 c= B1 by TARSKI:def_3;
then B1 \ B2 = B1 by A5, XBOOLE_0:def_10;
then A6: B1 misses B2 by XBOOLE_1:83;
set r = Path_product M;
A7: 3 = len (Permutations 3) by MATRIX_2:18;
then Id3 is even by MATRIX_2:25;
then reconsider r1 = (Path_product M) . id3, r2 = (Path_product M) . rid3, r3 = (Path_product M) . a3, r4 = (Path_product M) . a4, r5 = (Path_product M) . a5, r6 = (Path_product M) . a6 as Element of K by FUNCT_2:5;
A8: (Path_product M) . id3 = - (( the multF of K $$ (Path_matrix (Id3,M))),Id3) by MATRIX_3:def_8
.= the multF of K $$ (Path_matrix (Id3,M)) by A1, A7, MATRIX_2:def_13
.= the multF of K $$ <*a,e,i*> by A2, Th20, FINSEQ_2:53
.= (a * e) * i by Th26 ;
A9: (Path_product M) . a6 = - (( the multF of K $$ (Path_matrix (a6,M))),a6) by MATRIX_3:def_8
.= the multF of K $$ (Path_matrix (a6,M)) by A7, Lm14, MATRIX_2:def_13
.= the multF of K $$ <*c,d,h*> by A2, Th25
.= (c * d) * h by Th26 ;
A10: (Path_product M) . a5 = - (( the multF of K $$ (Path_matrix (a5,M))),a5) by MATRIX_3:def_8
.= - ( the multF of K $$ (Path_matrix (a5,M))) by A7, Th43, MATRIX_2:def_13
.= - ( the multF of K $$ <*b,d,i*>) by A2, Th24
.= - ((b * d) * i) by Th26 ;
A11: (Path_product M) . a4 = - (( the multF of K $$ (Path_matrix (a4,M))),a4) by MATRIX_3:def_8
.= the multF of K $$ (Path_matrix (a4,M)) by A7, Lm13, MATRIX_2:def_13
.= the multF of K $$ <*b,f,g*> by A2, Th23
.= (b * f) * g by Th26 ;
A12: (Path_product M) . a3 = - (( the multF of K $$ (Path_matrix (a3,M))),a3) by MATRIX_3:def_8
.= - ( the multF of K $$ (Path_matrix (a3,M))) by A7, Th44, MATRIX_2:def_13
.= - ( the multF of K $$ <*a,f,h*>) by A2, Th22
.= - ((a * f) * h) by Th26 ;
A13: (Path_product M) . rid3 = - (( the multF of K $$ (Path_matrix (rid3,M))),rid3) by MATRIX_3:def_8
.= - ( the multF of K $$ (Path_matrix (rid3,M))) by A7, Th15, Th42, MATRIX_2:def_13
.= - ( the multF of K $$ <*c,e,g*>) by A2, Th15, Th21
.= - ((c * e) * g) by Th26 ;
A14: ( the addF of K $$ (B1,(Path_product M)) = (r1 + r2) + r3 & the addF of K $$ (B2,(Path_product M)) = (r4 + r5) + r6 ) by Lm3, Lm4, Lm10, Lm11, Th15, FINSEQ_2:53, SETWOP_2:3;
Det M = the addF of K $$ ((FinOmega (Permutations 3)),(Path_product M)) by MATRIX_3:def_9
.= the addF of K . (( the addF of K $$ (B1,(Path_product M))),( the addF of K $$ (B2,(Path_product M)))) by A3, A6, SETWOP_2:4
.= ((r1 + r2) + r3) + (r4 + (r5 + r6)) by A14, RLVECT_1:def_3
.= (((r1 + r2) + r3) + r4) + (r5 + r6) by RLVECT_1:def_3
.= ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) by A8, A13, A12, A11, A10, A9, RLVECT_1:def_3 ;
hence Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h) ; ::_thesis: verum
end;
theorem :: MATRIX_9:47
for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)
proof
let K be Field; ::_thesis: for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)
reconsider rid3 = Rev (idseq 3) as Element of Permutations 3 by Th4;
let a, b, c, d, e, f, g, h, i be Element of K; ::_thesis: for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)
let M be Matrix of 3,K; ::_thesis: ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h) )
assume A1: M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> ; ::_thesis: Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)
reconsider a3 = <*1,3,2*>, a4 = <*2,3,1*>, a5 = <*2,1,3*>, a6 = <*3,1,2*> as Element of Permutations 3 by Th27;
reconsider id3 = idseq 3 as Permutation of (Seg 3) ;
reconsider Id3 = idseq 3 as Element of Permutations 3 by MATRIX_2:def_9;
reconsider B1 = {.Id3,rid3,a3.}, B2 = {.a4,a5,a6.} as Element of Fin (Permutations 3) ;
set r = PPath_product M;
A2: (PPath_product M) . id3 = the multF of K $$ (Path_matrix (Id3,M)) by Def1
.= the multF of K $$ <*a,e,i*> by A1, Th20, FINSEQ_2:53
.= (a * e) * i by Th26 ;
A3: (PPath_product M) . a6 = the multF of K $$ (Path_matrix (a6,M)) by Def1
.= the multF of K $$ <*c,d,h*> by A1, Th25
.= (c * d) * h by Th26 ;
A4: (PPath_product M) . a5 = the multF of K $$ (Path_matrix (a5,M)) by Def1
.= the multF of K $$ <*b,d,i*> by A1, Th24
.= (b * d) * i by Th26 ;
A5: (PPath_product M) . a4 = the multF of K $$ (Path_matrix (a4,M)) by Def1
.= the multF of K $$ <*b,f,g*> by A1, Th23
.= (b * f) * g by Th26 ;
now__::_thesis:_for_x_being_set_st_x_in_B1_holds_
x_in_B1_\_B2
let x be set ; ::_thesis: ( x in B1 implies x in B1 \ B2 )
assume A6: x in B1 ; ::_thesis: x in B1 \ B2
then ( x = Id3 or x = rid3 or x = a3 ) by ENUMSET1:def_1;
then not x in B2 by Lm5, Lm6, Lm7, Lm8, Lm9, Th15, ENUMSET1:def_1, FINSEQ_2:53;
hence x in B1 \ B2 by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then A7: B1 c= B1 \ B2 by TARSKI:def_3;
for x being set st x in B1 \ B2 holds
x in B1 by XBOOLE_0:def_5;
then B1 \ B2 c= B1 by TARSKI:def_3;
then B1 \ B2 = B1 by A7, XBOOLE_0:def_10;
then A8: B1 misses B2 by XBOOLE_1:83;
set F = the addF of K;
id3 in Permutations 3 by MATRIX_2:def_9;
then reconsider r1 = (PPath_product M) . id3, r2 = (PPath_product M) . rid3, r3 = (PPath_product M) . a3, r4 = (PPath_product M) . a4, r5 = (PPath_product M) . a5, r6 = (PPath_product M) . a6 as Element of K by FUNCT_2:5;
FinOmega (Permutations 3) = Permutations 3 by MATRIX_2:26, MATRIX_2:def_14;
then reconsider X = {Id3,rid3,a3,a4,a5,a6} as Element of Fin (Permutations 3) by Th15, Th19, FINSEQ_2:53;
A9: ( the addF of K $$ (B1,(PPath_product M)) = (r1 + r2) + r3 & the addF of K $$ (B2,(PPath_product M)) = (r4 + r5) + r6 ) by Lm3, Lm4, Lm10, Lm11, Th15, FINSEQ_2:53, SETWOP_2:3;
A10: (PPath_product M) . rid3 = the multF of K $$ (Path_matrix (rid3,M)) by Def1
.= the multF of K $$ <*c,e,g*> by A1, Th15, Th21
.= (c * e) * g by Th26 ;
A11: (PPath_product M) . a3 = the multF of K $$ (Path_matrix (a3,M)) by Def1
.= the multF of K $$ <*a,f,h*> by A1, Th22
.= (a * f) * h by Th26 ;
( FinOmega (Permutations 3) = X & X = {Id3,rid3,a3} \/ {a4,a5,a6} ) by Th15, Th19, ENUMSET1:13, FINSEQ_2:53, MATRIX_2:def_14;
then Per M = the addF of K . (( the addF of K $$ (B1,(PPath_product M))),( the addF of K $$ (B2,(PPath_product M)))) by A8, SETWOP_2:4
.= ((r1 + r2) + r3) + (r4 + (r5 + r6)) by A9, RLVECT_1:def_3
.= (((r1 + r2) + r3) + r4) + (r5 + r6) by RLVECT_1:def_3
.= ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h) by A2, A10, A11, A5, A4, A3, RLVECT_1:def_3 ;
hence Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h) ; ::_thesis: verum
end;
theorem Th48: :: MATRIX_9:48
for i, n being Element of NAT
for p being Element of Permutations n st i in Seg n holds
ex k being Element of NAT st
( k in Seg n & i = p . k )
proof
let i, n be Element of NAT ; ::_thesis: for p being Element of Permutations n st i in Seg n holds
ex k being Element of NAT st
( k in Seg n & i = p . k )
let p be Element of Permutations n; ::_thesis: ( i in Seg n implies ex k being Element of NAT st
( k in Seg n & i = p . k ) )
A1: p is Permutation of (Seg n) by MATRIX_2:def_9;
then A2: dom p = Seg n by FUNCT_2:52;
then reconsider s = p as FinSequence by FINSEQ_1:def_2;
assume i in Seg n ; ::_thesis: ex k being Element of NAT st
( k in Seg n & i = p . k )
then i in rng s by A1, FUNCT_2:def_3;
then ex k being Nat st
( k in dom s & i = s . k ) by FINSEQ_2:10;
hence ex k being Element of NAT st
( k in Seg n & i = p . k ) by A2; ::_thesis: verum
end;
theorem Th49: :: MATRIX_9:49
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
proof
let n be Nat; ::_thesis: for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
let K be Field; ::_thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
let M be Matrix of n,K; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K ) )
assume ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; ::_thesis: for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
then consider i being Element of NAT such that
A1: i in Seg n and
A2: for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ;
let p be Element of Permutations n; ::_thesis: ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) . l = 0. K )
n in NAT by ORDINAL1:def_12;
then consider k being Element of NAT such that
A3: k in Seg n and
A4: i = p . k by A1, Th48;
A5: 1 <= k by A3, FINSEQ_1:1;
len M = n by MATRIX_1:def_2;
then k <= len M by A3, FINSEQ_1:1;
then A6: k in dom M by A5, FINSEQ_3:25;
take k ; ::_thesis: ( k in Seg n & (Path_matrix (p,M)) . k = 0. K )
len (Path_matrix (p,M)) = n by MATRIX_3:def_7;
then dom (Path_matrix (p,M)) = Seg n by FINSEQ_1:def_3;
then (Path_matrix (p,M)) . k = M * (k,i) by A3, A4, MATRIX_3:def_7;
then (Path_matrix (p,M)) . k = (Col (M,i)) . k by A6, MATRIX_1:def_8;
hence ( k in Seg n & (Path_matrix (p,M)) . k = 0. K ) by A2, A3; ::_thesis: verum
end;
theorem Th50: :: MATRIX_9:50
for n being Nat
for K being Field
for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(Path_product M) . p = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(Path_product M) . p = 0. K
let K be Field; ::_thesis: for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(Path_product M) . p = 0. K
let p be Element of Permutations n; ::_thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(Path_product M) . p = 0. K
let M be Matrix of n,K; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies (Path_product M) . p = 0. K )
A1: (Path_product M) . p = - (( the multF of K $$ (Path_matrix (p,M))),p) by MATRIX_3:def_8
.= - ((Product (Path_matrix (p,M))),p) by GROUP_4:def_2 ;
assume ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; ::_thesis: (Path_product M) . p = 0. K
then consider l being Element of NAT such that
A2: l in Seg n and
A3: (Path_matrix (p,M)) . l = 0. K by Th49;
set k = l;
len (Path_matrix (p,M)) = n by MATRIX_3:def_7;
then l in dom (Path_matrix (p,M)) by A2, FINSEQ_1:def_3;
then A4: Product (Path_matrix (p,M)) = 0. K by A3, FVSUM_1:82;
percases ( p is even or p is odd ) ;
suppose p is even ; ::_thesis: (Path_product M) . p = 0. K
hence (Path_product M) . p = 0. K by A4, A1, MATRIX_2:def_13; ::_thesis: verum
end;
suppose p is odd ; ::_thesis: (Path_product M) . p = 0. K
then - ((Product (Path_matrix (p,M))),p) = - (Product (Path_matrix (p,M))) by MATRIX_2:def_13
.= 0. K by A4, RLVECT_1:12 ;
hence (Path_product M) . p = 0. K by A1; ::_thesis: verum
end;
end;
end;
theorem Th51: :: MATRIX_9:51
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) = 0. K
let K be Field; ::_thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) = 0. K
let M be Matrix of n,K; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) = 0. K )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
reconsider M1 = M as Matrix of n1,K ;
given i being Element of NAT such that A1: ( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; ::_thesis: the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) = 0. K
set P1 = FinOmega (Permutations n);
set f = Path_product M1;
set F = the addF of K;
reconsider P1 = FinOmega (Permutations n) as non empty Element of Fin (Permutations n1) by MATRIX_2:26, MATRIX_2:def_14;
defpred S1[ non empty Element of Fin (Permutations n1)] means the addF of K $$ ($1,(Path_product M1)) = 0. K;
A2: for x being Element of Permutations n1
for B being non empty Element of Fin (Permutations n1) st x in P1 & B c= P1 & not x in B & S1[B] holds
S1[B \/ {.x.}]
proof
let x be Element of Permutations n1; ::_thesis: for B being non empty Element of Fin (Permutations n1) st x in P1 & B c= P1 & not x in B & S1[B] holds
S1[B \/ {.x.}]
let B be non empty Element of Fin (Permutations n1); ::_thesis: ( x in P1 & B c= P1 & not x in B & S1[B] implies S1[B \/ {.x.}] )
assume that
x in P1 and
B c= P1 and
A3: not x in B and
A4: S1[B] ; ::_thesis: S1[B \/ {.x.}]
the addF of K $$ ((B \/ {.x.}),(Path_product M1)) = the addF of K . (( the addF of K $$ (B,(Path_product M1))),((Path_product M1) . x)) by A3, SETWOP_2:2
.= ( the addF of K $$ (B,(Path_product M1))) + (0. K) by A1, Th50
.= 0. K by A4, RLVECT_1:4 ;
hence S1[B \/ {.x.}] ; ::_thesis: verum
end;
A5: for x being Element of Permutations n1 st x in P1 holds
S1[{.x.}]
proof
let x be Element of Permutations n1; ::_thesis: ( x in P1 implies S1[{.x.}] )
assume x in P1 ; ::_thesis: S1[{.x.}]
the addF of K $$ ({.x.},(Path_product M1)) = (Path_product M1) . x by SETWISEO:17
.= 0. K by A1, Th50 ;
hence S1[{.x.}] ; ::_thesis: verum
end;
S1[P1] from MATRIX_9:sch_1(A5, A2);
hence the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) = 0. K ; ::_thesis: verum
end;
theorem Th52: :: MATRIX_9:52
for n being Nat
for K being Field
for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(PPath_product M) . p = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(PPath_product M) . p = 0. K
let K be Field; ::_thesis: for p being Element of Permutations n
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(PPath_product M) . p = 0. K
let p be Element of Permutations n; ::_thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
(PPath_product M) . p = 0. K
let M be Matrix of n,K; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies (PPath_product M) . p = 0. K )
assume ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; ::_thesis: (PPath_product M) . p = 0. K
then consider l being Element of NAT such that
A1: l in Seg n and
A2: (Path_matrix (p,M)) . l = 0. K by Th49;
len (Path_matrix (p,M)) = n by MATRIX_3:def_7;
then l in dom (Path_matrix (p,M)) by A1, FINSEQ_1:def_3;
then A3: Product (Path_matrix (p,M)) = 0. K by A2, FVSUM_1:82;
(PPath_product M) . p = the multF of K $$ (Path_matrix (p,M)) by Def1
.= 0. K by A3, GROUP_4:def_2 ;
hence (PPath_product M) . p = 0. K ; ::_thesis: verum
end;
Lm18: for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) = 0. K
let K be Field; ::_thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) = 0. K
let M be Matrix of n,K; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) = 0. K )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
reconsider M1 = M as Matrix of n1,K ;
set F = the addF of K;
set f = PPath_product M1;
set P1 = FinOmega (Permutations n1);
reconsider P1 = FinOmega (Permutations n1) as non empty Element of Fin (Permutations n1) by MATRIX_2:26, MATRIX_2:def_14;
defpred S1[ non empty Element of Fin (Permutations n1)] means the addF of K $$ ($1,(PPath_product M1)) = 0. K;
assume A1: ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; ::_thesis: the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) = 0. K
A2: for x being Element of Permutations n1
for B being non empty Element of Fin (Permutations n1) st x in P1 & B c= P1 & not x in B & S1[B] holds
S1[B \/ {.x.}]
proof
let x be Element of Permutations n1; ::_thesis: for B being non empty Element of Fin (Permutations n1) st x in P1 & B c= P1 & not x in B & S1[B] holds
S1[B \/ {.x.}]
let B be non empty Element of Fin (Permutations n1); ::_thesis: ( x in P1 & B c= P1 & not x in B & S1[B] implies S1[B \/ {.x.}] )
assume that
x in P1 and
B c= P1 and
A3: not x in B and
A4: S1[B] ; ::_thesis: S1[B \/ {.x.}]
the addF of K $$ ((B \/ {.x.}),(PPath_product M1)) = the addF of K . (( the addF of K $$ (B,(PPath_product M1))),((PPath_product M1) . x)) by A3, SETWOP_2:2
.= ( the addF of K $$ (B,(PPath_product M1))) + (0. K) by A1, Th52
.= 0. K by A4, RLVECT_1:4 ;
hence S1[B \/ {.x.}] ; ::_thesis: verum
end;
A5: for x being Element of Permutations n1 st x in P1 holds
S1[{.x.}]
proof
let x be Element of Permutations n1; ::_thesis: ( x in P1 implies S1[{.x.}] )
assume x in P1 ; ::_thesis: S1[{.x.}]
the addF of K $$ ({.x.},(PPath_product M1)) = (PPath_product M1) . x by SETWISEO:17
.= 0. K by A1, Th52 ;
hence S1[{.x.}] ; ::_thesis: verum
end;
S1[P1] from MATRIX_9:sch_1(A5, A2);
hence the addF of K $$ ((FinOmega (Permutations n)),(PPath_product M)) = 0. K ; ::_thesis: verum
end;
theorem :: MATRIX_9:53
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Det M = 0. K
proof
let n be Nat; ::_thesis: for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Det M = 0. K
let K be Field; ::_thesis: for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Det M = 0. K
let M be Matrix of n,K; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) implies Det M = 0. K )
assume A1: ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) ; ::_thesis: Det M = 0. K
set f = Path_product M;
set F = the addF of K;
Det M = the addF of K $$ ((FinOmega (Permutations n)),(Path_product M)) by MATRIX_3:def_9
.= 0. K by A1, Th51 ;
hence Det M = 0. K ; ::_thesis: verum
end;
theorem :: MATRIX_9:54
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = 0. K ) ) holds
Per M = 0. K by Lm18;
begin
theorem :: MATRIX_9:55
for n, i being Nat
for K being Field
for M, N being Matrix of n,K st i in Seg n holds
for p being Element of Permutations n ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
proof
let n, i be Nat; ::_thesis: for K being Field
for M, N being Matrix of n,K st i in Seg n holds
for p being Element of Permutations n ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
let K be Field; ::_thesis: for M, N being Matrix of n,K st i in Seg n holds
for p being Element of Permutations n ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
let M, N be Matrix of n,K; ::_thesis: ( i in Seg n implies for p being Element of Permutations n ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k ) )
assume A1: i in Seg n ; ::_thesis: for p being Element of Permutations n ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
let p be Element of Permutations n; ::_thesis: ex k being Element of NAT st
( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
n in NAT by ORDINAL1:def_12;
then consider k being Element of NAT such that
A2: k in Seg n and
A3: i = p . k by A1, Th48;
len (Path_matrix (p,N)) = n by MATRIX_3:def_7;
then A4: k in dom (Path_matrix (p,N)) by A2, FINSEQ_1:def_3;
then (Path_matrix (p,N)) . k = N * (k,i) by A3, MATRIX_3:def_7;
then A5: (Path_matrix (p,N)) /. k = N * (k,i) by A4, PARTFUN1:def_6;
take k ; ::_thesis: ( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k )
A6: len N = n by MATRIX_1:def_2;
then k in dom N by A2, FINSEQ_1:def_3;
then A7: (Col (N,i)) . k = N * (k,i) by MATRIX_1:def_8;
len (Col (N,i)) = len N by MATRIX_1:def_8;
then k in dom (Col (N,i)) by A2, A6, FINSEQ_1:def_3;
hence ( k in Seg n & i = p . k & (Col (N,i)) /. k = (Path_matrix (p,N)) /. k ) by A2, A3, A5, A7, PARTFUN1:def_6; ::_thesis: verum
end;
theorem :: MATRIX_9:56
for n being Nat
for K being Field
for a being Element of K
for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col (M,l) = Col (N,l) ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
proof
let n be Nat; ::_thesis: for K being Field
for a being Element of K
for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col (M,l) = Col (N,l) ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
let K be Field; ::_thesis: for a being Element of K
for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col (M,l) = Col (N,l) ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
let a be Element of K; ::_thesis: for M, N being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col (M,l) = Col (N,l) ) ) holds
for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
let M, N be Matrix of n,K; ::_thesis: ( ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col (M,l) = Col (N,l) ) ) implies for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) ) )
assume ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) ) & ( for l being Element of NAT st l <> i & l in Seg n holds
Col (M,l) = Col (N,l) ) ) ; ::_thesis: for p being Element of Permutations n ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
then consider i being Element of NAT such that
A1: i in Seg n and
A2: for k being Element of NAT st k in Seg n holds
(Col (M,i)) . k = a * ((Col (N,i)) /. k) and
for l being Element of NAT st l <> i & l in Seg n holds
Col (M,l) = Col (N,l) ;
let p be Element of Permutations n; ::_thesis: ex l being Element of NAT st
( l in Seg n & (Path_matrix (p,M)) /. l = a * ((Path_matrix (p,N)) /. l) )
n in NAT by ORDINAL1:def_12;
then consider k being Element of NAT such that
A3: k in Seg n and
A4: i = p . k by A1, Th48;
A5: 1 <= k by A3, FINSEQ_1:1;
len (Path_matrix (p,N)) = n by MATRIX_3:def_7;
then A6: k in dom (Path_matrix (p,N)) by A3, FINSEQ_1:def_3;
then (Path_matrix (p,N)) . k = N * (k,i) by A4, MATRIX_3:def_7;
then A7: (Path_matrix (p,N)) /. k = N * (k,i) by A6, PARTFUN1:def_6;
len (Col (N,i)) = len N by MATRIX_1:def_8;
then A8: dom (Col (N,i)) = dom N by FINSEQ_3:29;
len N = n by MATRIX_1:def_2;
then k <= len N by A3, FINSEQ_1:1;
then A9: k in dom N by A5, FINSEQ_3:25;
then (Col (N,i)) . k = N * (k,i) by MATRIX_1:def_8;
then A10: (Col (N,i)) /. k = (Path_matrix (p,N)) /. k by A9, A7, A8, PARTFUN1:def_6;
len M = n by MATRIX_1:def_2;
then k <= len M by A3, FINSEQ_1:1;
then A11: k in dom M by A5, FINSEQ_3:25;
take k ; ::_thesis: ( k in Seg n & (Path_matrix (p,M)) /. k = a * ((Path_matrix (p,N)) /. k) )
len (Path_matrix (p,M)) = n by MATRIX_3:def_7;
then A12: dom (Path_matrix (p,M)) = Seg n by FINSEQ_1:def_3;
then (Path_matrix (p,M)) . k = M * (k,i) by A3, A4, MATRIX_3:def_7;
then (Path_matrix (p,M)) . k = (Col (M,i)) . k by A11, MATRIX_1:def_8
.= a * ((Path_matrix (p,N)) /. k) by A2, A3, A10 ;
hence ( k in Seg n & (Path_matrix (p,M)) /. k = a * ((Path_matrix (p,N)) /. k) ) by A12, A3, PARTFUN1:def_6; ::_thesis: verum
end;