:: 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;