:: MATRIX_6 semantic presentation begin definition let n be Nat; let K be Field; let M1, M2 be Matrix of n,K; predM1 commutes_with M2 means :Def1: :: MATRIX_6:def 1 M1 * M2 = M2 * M1; reflexivity for M1 being Matrix of n,K holds M1 * M1 = M1 * M1 ; symmetry for M1, M2 being Matrix of n,K st M1 * M2 = M2 * M1 holds M2 * M1 = M1 * M2 ; end; :: deftheorem Def1 defines commutes_with MATRIX_6:def_1_:_ for n being Nat for K being Field for M1, M2 being Matrix of n,K holds ( M1 commutes_with M2 iff M1 * M2 = M2 * M1 ); definition let n be Nat; let K be Field; let M1, M2 be Matrix of n,K; predM1 is_reverse_of M2 means :Def2: :: MATRIX_6:def 2 ( M1 * M2 = M2 * M1 & M1 * M2 = 1. (K,n) ); symmetry for M1, M2 being Matrix of n,K st M1 * M2 = M2 * M1 & M1 * M2 = 1. (K,n) holds ( M2 * M1 = M1 * M2 & M2 * M1 = 1. (K,n) ) ; end; :: deftheorem Def2 defines is_reverse_of MATRIX_6:def_2_:_ for n being Nat for K being Field for M1, M2 being Matrix of n,K holds ( M1 is_reverse_of M2 iff ( M1 * M2 = M2 * M1 & M1 * M2 = 1. (K,n) ) ); definition let n be Nat; let K be Field; let M1 be Matrix of n,K; attrM1 is invertible means :Def3: :: MATRIX_6:def 3 ex M2 being Matrix of n,K st M1 is_reverse_of M2; end; :: deftheorem Def3 defines invertible MATRIX_6:def_3_:_ for n being Nat for K being Field for M1 being Matrix of n,K holds ( M1 is invertible iff ex M2 being Matrix of n,K st M1 is_reverse_of M2 ); definition let n be Nat; let K be Field; let M1 be Matrix of n,K; :: original: - redefine func - M1 -> Matrix of n,K; coherence - M1 is Matrix of n,K proof len M1 = n by MATRIX_1:24; then A1: len (- M1) = n by MATRIX_3:def_2; width M1 = n by MATRIX_1:24; then width (- M1) = n by MATRIX_3:def_2; hence - M1 is Matrix of n,K by A1, MATRIX_2:7; ::_thesis: verum end; end; definition let n be Nat; let K be Field; let M1, M2 be Matrix of n,K; :: original: + redefine funcM1 + M2 -> Matrix of n,K; coherence M1 + M2 is Matrix of n,K proof A1: width M2 = n by MATRIX_1:24; width M1 = n by MATRIX_1:24; then ( len (M1 + M2) = len M1 & width (M1 + M2) = width M2 ) by A1, MATRIX_3:def_3; hence M1 + M2 is Matrix of n,K by A1, MATRIX_1:24, MATRIX_2:7; ::_thesis: verum end; end; definition let n be Nat; let K be Field; let M1, M2 be Matrix of n,K; :: original: - redefine funcM1 - M2 -> Matrix of n,K; coherence M1 - M2 is Matrix of n,K proof len (M1 + (- M2)) = n by MATRIX_1:24; hence M1 - M2 is Matrix of n,K ; ::_thesis: verum end; :: original: * redefine funcM1 * M2 -> Matrix of n,K; coherence M1 * M2 is Matrix of n,K proof ( width M1 = n & len M2 = n ) by MATRIX_1:24; then A1: ( len (M1 * M2) = len M1 & width (M1 * M2) = width M2 ) by MATRIX_3:def_4; width M2 = n by MATRIX_1:24; hence M1 * M2 is Matrix of n,K by A1, MATRIX_1:24, MATRIX_2:7; ::_thesis: verum end; end; theorem Th1: :: MATRIX_6:1 for K being Field for A being Matrix of K holds (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) proof let K be Field; ::_thesis: for A being Matrix of K holds (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) let A be Matrix of K; ::_thesis: (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) percases ( len A > 0 or len A = 0 ) by NAT_1:3; supposeA1: len A > 0 ; ::_thesis: (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) set B = (0. (K,(len A),(len A))) * A; A2: width (- ((0. (K,(len A),(len A))) * A)) = width ((0. (K,(len A),(len A))) * A) by MATRIX_3:def_2; A3: len (0. (K,(len A),(len A))) = len A by MATRIX_1:def_2; then A4: width (0. (K,(len A),(len A))) = len A by A1, MATRIX_1:20; then A5: len ((0. (K,(len A),(len A))) * A) = len A by A3, MATRIX_3:def_4; A6: width ((0. (K,(len A),(len A))) * A) = width A by A4, MATRIX_3:def_4; (0. (K,(len A),(len A))) * A = ((0. (K,(len A),(len A))) + (0. (K,(len A),(len A)))) * A by MATRIX_3:4 .= ((0. (K,(len A),(len A))) * A) + ((0. (K,(len A),(len A))) * A) by A1, A3, A4, MATRIX_4:63 ; then ( len (- ((0. (K,(len A),(len A))) * A)) = len ((0. (K,(len A),(len A))) * A) & 0. (K,(len A),(width A)) = (((0. (K,(len A),(len A))) * A) + ((0. (K,(len A),(len A))) * A)) + (- ((0. (K,(len A),(len A))) * A)) ) by A5, A6, MATRIX_3:def_2, MATRIX_4:2; then 0. (K,(len A),(width A)) = ((0. (K,(len A),(len A))) * A) + (((0. (K,(len A),(len A))) * A) - ((0. (K,(len A),(len A))) * A)) by A2, MATRIX_3:3 .= (0. (K,(len A),(len A))) * A by A5, A2, MATRIX_4:20 ; hence (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) ; ::_thesis: verum end; supposeA7: len A = 0 ; ::_thesis: (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) then len (0. (K,(len A),(len A))) = 0 by MATRIX_1:def_2; then width (0. (K,(len A),(len A))) = len A by A7, MATRIX_1:def_3; then A8: len ((0. (K,(len A),(len A))) * A) = len (0. (K,(len A),(len A))) by MATRIX_3:def_4; ( len (0. (K,(len A),(len A))) = len A & len (0. (K,(len A),(width A))) = len A ) by MATRIX_1:def_2; hence (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A)) by A7, A8, CARD_2:64; ::_thesis: verum end; end; end; theorem Th2: :: MATRIX_6:2 for K being Field for A being Matrix of K st width A > 0 holds A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) proof let K be Field; ::_thesis: for A being Matrix of K st width A > 0 holds A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) let A be Matrix of K; ::_thesis: ( width A > 0 implies A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) ) A1: width (- (A * (0. (K,(width A),(width A))))) = width (A * (0. (K,(width A),(width A)))) by MATRIX_3:def_2; set B = A * (0. (K,(width A),(width A))); assume A2: width A > 0 ; ::_thesis: A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) then A3: len A > 0 by MATRIX_1:def_3; A4: len (0. (K,(width A),(width A))) = width A by MATRIX_1:def_2; then A5: len (A * (0. (K,(width A),(width A)))) = len A by MATRIX_3:def_4; A6: width (0. (K,(width A),(width A))) = width A by A2, A4, MATRIX_1:20; then A7: width (A * (0. (K,(width A),(width A)))) = width A by A4, MATRIX_3:def_4; A * (0. (K,(width A),(width A))) = A * ((0. (K,(width A),(width A))) + (0. (K,(width A),(width A)))) by MATRIX_3:4 .= (A * (0. (K,(width A),(width A)))) + (A * (0. (K,(width A),(width A)))) by A2, A3, A4, A6, MATRIX_4:62 ; then ( len (- (A * (0. (K,(width A),(width A))))) = len (A * (0. (K,(width A),(width A)))) & 0. (K,(len A),(width A)) = ((A * (0. (K,(width A),(width A)))) + (A * (0. (K,(width A),(width A))))) + (- (A * (0. (K,(width A),(width A))))) ) by A5, A7, MATRIX_3:def_2, MATRIX_4:2; then 0. (K,(len A),(width A)) = (A * (0. (K,(width A),(width A)))) + ((A * (0. (K,(width A),(width A)))) - (A * (0. (K,(width A),(width A))))) by A1, MATRIX_3:3 .= A * (0. (K,(width A),(width A))) by A5, A1, MATRIX_4:20 ; hence A * (0. (K,(width A),(width A))) = 0. (K,(len A),(width A)) ; ::_thesis: verum end; theorem Th3: :: MATRIX_6:3 for n being Nat for K being Field for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n) proof let n be Nat; ::_thesis: for K being Field for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n) let K be Field; ::_thesis: for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n) let M1 be Matrix of n,K; ::_thesis: M1 commutes_with 0. (K,n,n) percases ( n > 0 or n = 0 ) by NAT_1:3; supposeA1: n > 0 ; ::_thesis: M1 commutes_with 0. (K,n,n) A2: ( len M1 = n & width M1 = n ) by MATRIX_1:24; then A3: (0. (K,n,n)) * M1 = 0. (K,n,n) by Th1; M1 * (0. (K,n,n)) = 0. (K,n,n) by A1, A2, Th2; hence M1 commutes_with 0. (K,n,n) by A3, Def1; ::_thesis: verum end; suppose n = 0 ; ::_thesis: M1 commutes_with 0. (K,n,n) then ( len M1 = 0 & len (0. (K,n,n)) = 0 ) by MATRIX_1:def_2; hence M1 commutes_with 0. (K,n,n) by CARD_2:64; ::_thesis: verum end; end; end; theorem :: MATRIX_6:4 for n being Nat for K being Field for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds M1 commutes_with M2 * M3 proof let n be Nat; ::_thesis: for K being Field for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds M1 commutes_with M2 * M3 let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 holds M1 commutes_with M2 * M3 let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 commutes_with M2 & M2 commutes_with M3 & M1 commutes_with M3 implies M1 commutes_with M2 * M3 ) A1: width M1 = n by MATRIX_1:24; A2: width M2 = n by MATRIX_1:24; A3: len M1 = n by MATRIX_1:24; A4: len M3 = n by MATRIX_1:24; A5: ( width M3 = n & len M2 = n ) by MATRIX_1:24; assume that A6: M1 commutes_with M2 and A7: M2 commutes_with M3 and A8: M1 commutes_with M3 ; ::_thesis: M1 commutes_with M2 * M3 (M2 * M3) * M1 = (M3 * M2) * M1 by A7, Def1 .= M3 * (M2 * M1) by A2, A3, A5, MATRIX_3:33 .= M3 * (M1 * M2) by A6, Def1 .= (M3 * M1) * M2 by A1, A3, A5, MATRIX_3:33 .= (M1 * M3) * M2 by A8, Def1 .= M1 * (M3 * M2) by A1, A5, A4, MATRIX_3:33 .= M1 * (M2 * M3) by A7, Def1 ; hence M1 commutes_with M2 * M3 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:5 for n being Nat for K being Field for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M1 commutes_with M3 & n > 0 holds M1 commutes_with M2 + M3 proof let n be Nat; ::_thesis: for K being Field for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M1 commutes_with M3 & n > 0 holds M1 commutes_with M2 + M3 let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 commutes_with M2 & M1 commutes_with M3 & n > 0 holds M1 commutes_with M2 + M3 let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 commutes_with M2 & M1 commutes_with M3 & n > 0 implies M1 commutes_with M2 + M3 ) A1: width M1 = n by MATRIX_1:24; A2: ( len M1 = n & len M2 = n ) by MATRIX_1:24; A3: len M3 = n by MATRIX_1:24; assume that A4: M1 commutes_with M2 and A5: M1 commutes_with M3 and A6: n > 0 ; ::_thesis: M1 commutes_with M2 + M3 A7: ( width M2 = n & width M3 = n ) by MATRIX_1:24; then (M2 + M3) * M1 = (M2 * M1) + (M3 * M1) by A2, A3, A6, MATRIX_4:63 .= (M1 * M2) + (M3 * M1) by A4, Def1 .= (M1 * M2) + (M1 * M3) by A5, Def1 .= M1 * (M2 + M3) by A1, A7, A2, A3, A6, MATRIX_4:62 ; hence M1 commutes_with M2 + M3 by Def1; ::_thesis: verum end; theorem Th6: :: MATRIX_6:6 for n being Nat for K being Field for M1 being Matrix of n,K holds M1 commutes_with 1. (K,n) proof let n be Nat; ::_thesis: for K being Field for M1 being Matrix of n,K holds M1 commutes_with 1. (K,n) let K be Field; ::_thesis: for M1 being Matrix of n,K holds M1 commutes_with 1. (K,n) let M1 be Matrix of n,K; ::_thesis: M1 commutes_with 1. (K,n) ( M1 = M1 * (1. (K,n)) & M1 = (1. (K,n)) * M1 ) by MATRIX_3:18, MATRIX_3:19; hence M1 commutes_with 1. (K,n) by Def1; ::_thesis: verum end; theorem Th7: :: MATRIX_6:7 for n being Nat for K being Field for M2, M3, M1 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds M1 = M2 proof let n be Nat; ::_thesis: for K being Field for M2, M3, M1 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds M1 = M2 let K be Field; ::_thesis: for M2, M3, M1 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds M1 = M2 let M2, M3, M1 be Matrix of n,K; ::_thesis: ( M2 is_reverse_of M3 & M1 is_reverse_of M3 implies M1 = M2 ) A1: ( width M1 = n & width M3 = n ) by MATRIX_1:24; A2: ( len M2 = n & len M3 = n ) by MATRIX_1:24; assume that A3: M2 is_reverse_of M3 and A4: M1 is_reverse_of M3 ; ::_thesis: M1 = M2 M1 = M1 * (1. (K,n)) by MATRIX_3:19 .= M1 * (M3 * M2) by A3, Def2 .= (M1 * M3) * M2 by A1, A2, MATRIX_3:33 .= (1. (K,n)) * M2 by A4, Def2 .= M2 by MATRIX_3:18 ; hence M1 = M2 ; ::_thesis: verum end; definition let n be Nat; let K be Field; let M1 be Matrix of n,K; assume A1: M1 is invertible ; funcM1 ~ -> Matrix of n,K means :Def4: :: MATRIX_6:def 4 it is_reverse_of M1; existence ex b1 being Matrix of n,K st b1 is_reverse_of M1 by A1, Def3; uniqueness for b1, b2 being Matrix of n,K st b1 is_reverse_of M1 & b2 is_reverse_of M1 holds b1 = b2 by Th7; end; :: deftheorem Def4 defines ~ MATRIX_6:def_4_:_ for n being Nat for K being Field for M1 being Matrix of n,K st M1 is invertible holds for b4 being Matrix of n,K holds ( b4 = M1 ~ iff b4 is_reverse_of M1 ); theorem Th8: :: MATRIX_6:8 for n being Nat for K being Field holds ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) proof let n be Nat; ::_thesis: for K being Field holds ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) let K be Field; ::_thesis: ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) (1. (K,n)) * (1. (K,n)) = 1. (K,n) by MATRIX_3:18; then A1: 1. (K,n) is_reverse_of 1. (K,n) by Def2; then 1. (K,n) is invertible by Def3; hence ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by A1, Def4; ::_thesis: verum end; theorem :: MATRIX_6:9 for n being Nat for K being Field holds ((1. (K,n)) ~) ~ = 1. (K,n) proof let n be Nat; ::_thesis: for K being Field holds ((1. (K,n)) ~) ~ = 1. (K,n) let K be Field; ::_thesis: ((1. (K,n)) ~) ~ = 1. (K,n) (1. (K,n)) ~ = 1. (K,n) by Th8; hence ((1. (K,n)) ~) ~ = 1. (K,n) ; ::_thesis: verum end; theorem Th10: :: MATRIX_6:10 for n being Nat for K being Field holds (1. (K,n)) @ = 1. (K,n) proof let n be Nat; ::_thesis: for K being Field holds (1. (K,n)) @ = 1. (K,n) let K be Field; ::_thesis: (1. (K,n)) @ = 1. (K,n) percases ( n > 0 or n = 0 ) by NAT_1:3; supposeA1: n > 0 ; ::_thesis: (1. (K,n)) @ = 1. (K,n) A2: len (1. (K,n)) = n by MATRIX_1:24; A3: Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_1:24; A4: for i, j being Nat st [i,j] in Indices (1. (K,n)) holds (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (1. (K,n)) implies (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) ) assume A5: [i,j] in Indices (1. (K,n)) ; ::_thesis: (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) then ( i in Seg n & j in Seg n ) by A3, ZFMISC_1:87; then A6: [j,i] in Indices (1. (K,n)) by A3, ZFMISC_1:87; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) hence (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) by A5, MATRIX_1:def_6; ::_thesis: verum end; suppose i <> j ; ::_thesis: (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) then ( (1. (K,n)) * (i,j) = 0. K & (1. (K,n)) * (j,i) = 0. K ) by A5, A6, MATRIX_1:def_11; hence (1. (K,n)) * (i,j) = ((1. (K,n)) @) * (i,j) by A6, MATRIX_1:def_6; ::_thesis: verum end; end; end; A7: width (1. (K,n)) = n by MATRIX_1:24; then ( len ((1. (K,n)) @) = width (1. (K,n)) & width ((1. (K,n)) @) = len (1. (K,n)) ) by A1, MATRIX_2:10; hence (1. (K,n)) @ = 1. (K,n) by A7, A2, A4, MATRIX_1:21; ::_thesis: verum end; suppose n = 0 ; ::_thesis: (1. (K,n)) @ = 1. (K,n) hence (1. (K,n)) @ = 1. (K,n) by MATRIX_1:35; ::_thesis: verum end; end; end; theorem :: MATRIX_6:11 for K being Field for n being Nat holds ((1. (K,n)) @) ~ = 1. (K,n) proof let K be Field; ::_thesis: for n being Nat holds ((1. (K,n)) @) ~ = 1. (K,n) let n be Nat; ::_thesis: ((1. (K,n)) @) ~ = 1. (K,n) (1. (K,n)) @ = 1. (K,n) by Th10; hence ((1. (K,n)) @) ~ = 1. (K,n) by Th8; ::_thesis: verum end; theorem :: MATRIX_6:12 for n being Nat for K being Field for M3, M1 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds M1 @ is_reverse_of M3 @ proof let n be Nat; ::_thesis: for K being Field for M3, M1 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds M1 @ is_reverse_of M3 @ let K be Field; ::_thesis: for M3, M1 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds M1 @ is_reverse_of M3 @ let M3, M1 be Matrix of n,K; ::_thesis: ( M3 is_reverse_of M1 & n > 0 implies M1 @ is_reverse_of M3 @ ) A1: ( width M1 = n & width M3 = n ) by MATRIX_1:24; assume that A2: M3 is_reverse_of M1 and A3: n > 0 ; ::_thesis: M1 @ is_reverse_of M3 @ ( len M1 = n & M3 * M1 = M1 * M3 ) by A2, Def2, MATRIX_1:24; then A4: (M1 * M3) @ = (M1 @) * (M3 @) by A1, A3, MATRIX_3:22; M1 * M3 = 1. (K,n) by A2, Def2; then A5: (M1 @) * (M3 @) = 1. (K,n) by A4, Th10; len M3 = n by MATRIX_1:24; then (M3 @) * (M1 @) = (M1 @) * (M3 @) by A1, A3, A4, MATRIX_3:22; hence M1 @ is_reverse_of M3 @ by A5, Def2; ::_thesis: verum end; theorem :: MATRIX_6:13 for n being Nat for K being Field for M being Matrix of n,K st M is invertible & n > 0 holds (M @) ~ = (M ~) @ proof let n be Nat; ::_thesis: for K being Field for M being Matrix of n,K st M is invertible & n > 0 holds (M @) ~ = (M ~) @ let K be Field; ::_thesis: for M being Matrix of n,K st M is invertible & n > 0 holds (M @) ~ = (M ~) @ let M be Matrix of n,K; ::_thesis: ( M is invertible & n > 0 implies (M @) ~ = (M ~) @ ) assume that A1: M is invertible and A2: n > 0 ; ::_thesis: (M @) ~ = (M ~) @ set M1 = M @ ; set M2 = (M ~) @ ; A3: ( width M = n & width (M ~) = n ) by MATRIX_1:24; len M = n by MATRIX_1:24; then A4: ((M ~) * M) @ = (M @) * ((M ~) @) by A2, A3, MATRIX_3:22; A5: M ~ is_reverse_of M by A1, Def4; then (M ~) * M = 1. (K,n) by Def2; then A6: (M @) * ((M ~) @) = 1. (K,n) by A4, Th10; len (M ~) = n by MATRIX_1:24; then (M * (M ~)) @ = ((M ~) @) * (M @) by A2, A3, MATRIX_3:22; then (M @) * ((M ~) @) = ((M ~) @) * (M @) by A5, A4, Def2; then A7: M @ is_reverse_of (M ~) @ by A6, Def2; then M @ is invertible by Def3; hence (M @) ~ = (M ~) @ by A7, Def4; ::_thesis: verum end; theorem :: MATRIX_6:14 for K being Field for n being Nat for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds M3 * M4 is_reverse_of M2 * M1 proof let K be Field; ::_thesis: for n being Nat for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds M3 * M4 is_reverse_of M2 * M1 let n be Nat; ::_thesis: for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds M3 * M4 is_reverse_of M2 * M1 let M1, M2, M3, M4 be Matrix of n,K; ::_thesis: ( M3 is_reverse_of M1 & M4 is_reverse_of M2 implies M3 * M4 is_reverse_of M2 * M1 ) A1: width M1 = n by MATRIX_1:24; A2: ( width M2 = n & len M1 = n ) by MATRIX_1:24; A3: len M3 = n by MATRIX_1:24; A4: ( width M3 = n & len M4 = n ) by MATRIX_1:24; assume that A5: M3 is_reverse_of M1 and A6: M4 is_reverse_of M2 ; ::_thesis: M3 * M4 is_reverse_of M2 * M1 width (M2 * M1) = n by MATRIX_1:24; then A7: (M2 * M1) * (M3 * M4) = ((M2 * M1) * M3) * M4 by A3, A4, MATRIX_3:33 .= (M2 * (M1 * M3)) * M4 by A1, A2, A3, MATRIX_3:33 .= (M2 * (1. (K,n))) * M4 by A5, Def2 .= M2 * M4 by MATRIX_3:19 .= 1. (K,n) by A6, Def2 ; A8: width M4 = n by MATRIX_1:24; A9: len M2 = n by MATRIX_1:24; width (M3 * M4) = n by MATRIX_1:24; then (M3 * M4) * (M2 * M1) = ((M3 * M4) * M2) * M1 by A2, A9, MATRIX_3:33 .= (M3 * (M4 * M2)) * M1 by A9, A8, A4, MATRIX_3:33 .= (M3 * (1. (K,n))) * M1 by A6, Def2 .= M3 * M1 by MATRIX_3:19 .= 1. (K,n) by A5, Def2 ; hence M3 * M4 is_reverse_of M2 * M1 by A7, Def2; ::_thesis: verum end; theorem :: MATRIX_6:15 for K being Field for n being Nat for M1, M2 being Matrix of n,K st M2 is_reverse_of M1 holds M1 commutes_with M2 proof let K be Field; ::_thesis: for n being Nat for M1, M2 being Matrix of n,K st M2 is_reverse_of M1 holds M1 commutes_with M2 let n be Nat; ::_thesis: for M1, M2 being Matrix of n,K st M2 is_reverse_of M1 holds M1 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M2 is_reverse_of M1 implies M1 commutes_with M2 ) assume M2 is_reverse_of M1 ; ::_thesis: M1 commutes_with M2 then M2 * M1 = M1 * M2 by Def2; hence M1 commutes_with M2 by Def1; ::_thesis: verum end; theorem Th16: :: MATRIX_6:16 for n being Nat for K being Field for M being Matrix of n,K st M is invertible holds ( M ~ is invertible & (M ~) ~ = M ) proof let n be Nat; ::_thesis: for K being Field for M being Matrix of n,K st M is invertible holds ( M ~ is invertible & (M ~) ~ = M ) let K be Field; ::_thesis: for M being Matrix of n,K st M is invertible holds ( M ~ is invertible & (M ~) ~ = M ) let M be Matrix of n,K; ::_thesis: ( M is invertible implies ( M ~ is invertible & (M ~) ~ = M ) ) assume M is invertible ; ::_thesis: ( M ~ is invertible & (M ~) ~ = M ) then A1: M ~ is_reverse_of M by Def4; then M ~ is invertible by Def3; hence ( M ~ is invertible & (M ~) ~ = M ) by A1, Def4; ::_thesis: verum end; theorem :: MATRIX_6:17 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible holds M1 commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible holds M1 commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible holds M1 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 * M2 = 0. (K,n,n) & M1 is invertible implies M1 commutes_with M2 ) assume that A1: n > 0 and A2: M1 * M2 = 0. (K,n,n) and A3: M1 is invertible ; ::_thesis: M1 commutes_with M2 A4: M1 ~ is_reverse_of M1 by A3, Def4; A5: len M2 = n by MATRIX_1:24; A6: ( len M1 = n & width M1 = n ) by MATRIX_1:24; A7: len (M1 ~) = n by MATRIX_1:24; A8: width (M1 ~) = n by MATRIX_1:24; M2 = (1. (K,n)) * M2 by MATRIX_3:18 .= ((M1 ~) * M1) * M2 by A4, Def2 .= (M1 ~) * (0. (K,n,n)) by A2, A6, A5, A8, MATRIX_3:33 .= 0. (K,n,n) by A1, A7, A8, Th2 ; hence M1 commutes_with M2 by Th3; ::_thesis: verum end; theorem :: MATRIX_6:18 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 = M1 * M2 & M1 is invertible holds M1 commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 = M1 * M2 & M1 is invertible holds M1 commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 = M1 * M2 & M1 is invertible holds M1 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 = M1 * M2 & M1 is invertible implies M1 commutes_with M2 ) assume that A1: M1 = M1 * M2 and A2: M1 is invertible ; ::_thesis: M1 commutes_with M2 A3: M1 ~ is_reverse_of M1 by A2, Def4; A4: ( len M2 = n & width (M1 ~) = n ) by MATRIX_1:24; A5: ( len M1 = n & width M1 = n ) by MATRIX_1:24; M2 = (1. (K,n)) * M2 by MATRIX_3:18 .= ((M1 ~) * M1) * M2 by A3, Def2 .= (M1 ~) * M1 by A1, A5, A4, MATRIX_3:33 .= 1. (K,n) by A3, Def2 ; hence M1 commutes_with M2 by Th6; ::_thesis: verum end; theorem :: MATRIX_6:19 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 = M2 * M1 & M1 is invertible holds M1 commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 = M2 * M1 & M1 is invertible holds M1 commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 = M2 * M1 & M1 is invertible holds M1 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 = M2 * M1 & M1 is invertible implies M1 commutes_with M2 ) assume that A1: M1 = M2 * M1 and A2: M1 is invertible ; ::_thesis: M1 commutes_with M2 A3: M1 ~ is_reverse_of M1 by A2, Def4; A4: ( width M2 = n & len (M1 ~) = n ) by MATRIX_1:24; A5: ( len M1 = n & width M1 = n ) by MATRIX_1:24; M2 = M2 * (1. (K,n)) by MATRIX_3:19 .= M2 * (M1 * (M1 ~)) by A3, Def2 .= M1 * (M1 ~) by A1, A5, A4, MATRIX_3:33 .= 1. (K,n) by A3, Def2 ; hence M1 commutes_with M2 by Th6; ::_thesis: verum end; definition let n be Nat; let K be Field; let M1 be Matrix of n,K; attrM1 is symmetric means :Def5: :: MATRIX_6:def 5 M1 @ = M1; end; :: deftheorem Def5 defines symmetric MATRIX_6:def_5_:_ for n being Nat for K being Field for M1 being Matrix of n,K holds ( M1 is symmetric iff M1 @ = M1 ); registration let n be Nat; let K be Field; cluster 1. (K,n) -> symmetric ; coherence 1. (K,n) is symmetric proof (1. (K,n)) @ = 1. (K,n) by Th10; hence 1. (K,n) is symmetric by Def5; ::_thesis: verum end; end; theorem Th20: :: MATRIX_6:20 for n being Nat for K being Field for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a proof let n be Nat; ::_thesis: for K being Field for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a let K be Field; ::_thesis: for a being Element of K holds ((n,n) --> a) @ = (n,n) --> a let a be Element of K; ::_thesis: ((n,n) --> a) @ = (n,n) --> a len ((n,n) --> a) = n by MATRIX_1:24; then A1: len (((n,n) --> a) @) = len ((n,n) --> a) by MATRIX_1:24; A2: Indices ((n,n) --> a) = [:(Seg n),(Seg n):] by MATRIX_1:24; A3: for i, j being Nat st [i,j] in Indices (((n,n) --> a) @) holds (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (((n,n) --> a) @) implies (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j) ) assume [i,j] in Indices (((n,n) --> a) @) ; ::_thesis: (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j) then A4: [i,j] in Indices ((n,n) --> a) by MATRIX_1:26; then ( i in Seg n & j in Seg n ) by A2, ZFMISC_1:87; then [j,i] in Indices ((n,n) --> a) by A2, ZFMISC_1:87; then ( (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (j,i) & ((n,n) --> a) * (j,i) = a ) by MATRIX_1:def_6, MATRIX_2:1; hence (((n,n) --> a) @) * (i,j) = ((n,n) --> a) * (i,j) by A4, MATRIX_2:1; ::_thesis: verum end; width ((n,n) --> a) = n by MATRIX_1:24; then width (((n,n) --> a) @) = width ((n,n) --> a) by MATRIX_1:24; hence ((n,n) --> a) @ = (n,n) --> a by A1, A3, MATRIX_1:21; ::_thesis: verum end; theorem :: MATRIX_6:21 for n being Nat for K being Field for a being Element of K holds (n,n) --> a is symmetric proof let n be Nat; ::_thesis: for K being Field for a being Element of K holds (n,n) --> a is symmetric let K be Field; ::_thesis: for a being Element of K holds (n,n) --> a is symmetric let a be Element of K; ::_thesis: (n,n) --> a is symmetric ((n,n) --> a) @ = (n,n) --> a by Th20; hence (n,n) --> a is symmetric by Def5; ::_thesis: verum end; theorem :: MATRIX_6:22 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds ( M1 commutes_with M2 iff M1 * M2 is symmetric ) proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds ( M1 commutes_with M2 iff M1 * M2 is symmetric ) let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is symmetric & M2 is symmetric holds ( M1 commutes_with M2 iff M1 * M2 is symmetric ) let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 is symmetric & M2 is symmetric implies ( M1 commutes_with M2 iff M1 * M2 is symmetric ) ) assume that A1: n > 0 and A2: ( M1 is symmetric & M2 is symmetric ) ; ::_thesis: ( M1 commutes_with M2 iff M1 * M2 is symmetric ) A3: ( width M1 = n & len M2 = n ) by MATRIX_1:24; A4: width M2 = n by MATRIX_1:24; A5: ( M1 @ = M1 & M2 @ = M2 ) by A2, Def5; thus ( M1 commutes_with M2 implies M1 * M2 is symmetric ) ::_thesis: ( M1 * M2 is symmetric implies M1 commutes_with M2 ) proof assume A6: M1 commutes_with M2 ; ::_thesis: M1 * M2 is symmetric (M1 * M2) @ = M2 * M1 by A1, A5, A3, A4, MATRIX_3:22 .= M1 * M2 by A6, Def1 ; hence M1 * M2 is symmetric by Def5; ::_thesis: verum end; assume A7: M1 * M2 is symmetric ; ::_thesis: M1 commutes_with M2 M2 * M1 = (M1 * M2) @ by A1, A5, A3, A4, MATRIX_3:22 .= M1 * M2 by A7, Def5 ; hence M1 commutes_with M2 by Def1; ::_thesis: verum end; theorem Th23: :: MATRIX_6:23 for n being Nat for K being Field for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @) proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @) let K be Field; ::_thesis: for M1, M2 being Matrix of n,K holds (M1 + M2) @ = (M1 @) + (M2 @) let M1, M2 be Matrix of n,K; ::_thesis: (M1 + M2) @ = (M1 @) + (M2 @) for i, j being Nat st [i,j] in Indices ((M1 + M2) @) holds ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((M1 + M2) @) implies ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j) ) assume [i,j] in Indices ((M1 + M2) @) ; ::_thesis: ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j) then A1: [i,j] in [:(Seg n),(Seg n):] by MATRIX_1:24; then A2: [i,j] in Indices (M1 @) by MATRIX_1:24; ( i in Seg n & j in Seg n ) by A1, ZFMISC_1:87; then A3: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87; then A4: [j,i] in Indices M1 by MATRIX_1:24; A5: [j,i] in Indices M2 by A3, MATRIX_1:24; [j,i] in Indices (M1 + M2) by A3, MATRIX_1:24; then ((M1 + M2) @) * (i,j) = (M1 + M2) * (j,i) by MATRIX_1:def_6 .= (M1 * (j,i)) + (M2 * (j,i)) by A4, MATRIX_3:def_3 .= ((M1 @) * (i,j)) + (M2 * (j,i)) by A4, MATRIX_1:def_6 .= ((M1 @) * (i,j)) + ((M2 @) * (i,j)) by A5, MATRIX_1:def_6 .= ((M1 @) + (M2 @)) * (i,j) by A2, MATRIX_3:def_3 ; hence ((M1 + M2) @) * (i,j) = ((M1 @) + (M2 @)) * (i,j) ; ::_thesis: verum end; hence (M1 + M2) @ = (M1 @) + (M2 @) by MATRIX_1:27; ::_thesis: verum end; theorem :: MATRIX_6:24 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds M1 + M2 is symmetric proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds M1 + M2 is symmetric let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds M1 + M2 is symmetric let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is symmetric & M2 is symmetric implies M1 + M2 is symmetric ) assume that A1: M1 is symmetric and A2: M2 is symmetric ; ::_thesis: M1 + M2 is symmetric (M1 + M2) @ = (M1 @) + (M2 @) by Th23 .= M1 + (M2 @) by A1, Def5 .= M1 + M2 by A2, Def5 ; hence M1 + M2 is symmetric by Def5; ::_thesis: verum end; theorem :: MATRIX_6:25 for n being Nat for K being Field for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K holds M1 is symmetric proof let n be Nat; ::_thesis: for K being Field for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K holds M1 is symmetric let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K holds M1 is symmetric let M1 be Matrix of n,K; ::_thesis: ( M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K implies M1 is symmetric ) assume A1: ( M1 is Upper_Triangular_Matrix of n,K & M1 is Lower_Triangular_Matrix of n,K ) ; ::_thesis: M1 is symmetric A2: Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; for i, j being Nat st [i,j] in Indices M1 holds (M1 @) * (i,j) = M1 * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies (M1 @) * (i,j) = M1 * (i,j) ) assume A3: [i,j] in Indices M1 ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j) then [i,j] in [:(Seg n),(Seg n):] by MATRIX_1:24; then ( i in Seg n & j in Seg n ) by ZFMISC_1:87; then A4: [j,i] in Indices M1 by A2, ZFMISC_1:87; percases ( i = j or i <> j ) ; suppose i = j ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j) hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_1:def_6; ::_thesis: verum end; supposeA5: i <> j ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j) percases ( i < j or i > j ) by A5, XXREAL_0:1; suppose i < j ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j) then ( M1 * (i,j) = 0. K & M1 * (j,i) = 0. K ) by A1, A3, A4, MATRIX_2:def_3, MATRIX_2:def_4; hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_1:def_6; ::_thesis: verum end; suppose i > j ; ::_thesis: (M1 @) * (i,j) = M1 * (i,j) then ( M1 * (i,j) = 0. K & M1 * (j,i) = 0. K ) by A1, A3, A4, MATRIX_2:def_3, MATRIX_2:def_4; hence (M1 @) * (i,j) = M1 * (i,j) by A4, MATRIX_1:def_6; ::_thesis: verum end; end; end; end; end; then M1 @ = M1 by MATRIX_1:27; hence M1 is symmetric by Def5; ::_thesis: verum end; theorem Th26: :: MATRIX_6:26 for K being Field for n being Nat for M1 being Matrix of n,K holds (- M1) @ = - (M1 @) proof let K be Field; ::_thesis: for n being Nat for M1 being Matrix of n,K holds (- M1) @ = - (M1 @) let n be Nat; ::_thesis: for M1 being Matrix of n,K holds (- M1) @ = - (M1 @) let M1 be Matrix of n,K; ::_thesis: (- M1) @ = - (M1 @) for i, j being Nat st [i,j] in Indices ((- M1) @) holds ((- M1) @) * (i,j) = (- (M1 @)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices ((- M1) @) implies ((- M1) @) * (i,j) = (- (M1 @)) * (i,j) ) assume A1: [i,j] in Indices ((- M1) @) ; ::_thesis: ((- M1) @) * (i,j) = (- (M1 @)) * (i,j) then A2: [i,j] in Indices (M1 @) by MATRIX_1:26; [i,j] in [:(Seg n),(Seg n):] by A1, MATRIX_1:24; then ( i in Seg n & j in Seg n ) by ZFMISC_1:87; then A3: [j,i] in [:(Seg n),(Seg n):] by ZFMISC_1:87; then A4: [j,i] in Indices M1 by MATRIX_1:24; [j,i] in Indices (- M1) by A3, MATRIX_1:24; then ((- M1) @) * (i,j) = (- M1) * (j,i) by MATRIX_1:def_6 .= - (M1 * (j,i)) by A4, MATRIX_3:def_2 .= - ((M1 @) * (i,j)) by A4, MATRIX_1:def_6 .= (- (M1 @)) * (i,j) by A2, MATRIX_3:def_2 ; hence ((- M1) @) * (i,j) = (- (M1 @)) * (i,j) ; ::_thesis: verum end; hence (- M1) @ = - (M1 @) by MATRIX_1:27; ::_thesis: verum end; theorem :: MATRIX_6:27 for K being Field for n being Nat for M1 being Matrix of n,K st M1 is symmetric holds - M1 is symmetric proof let K be Field; ::_thesis: for n being Nat for M1 being Matrix of n,K st M1 is symmetric holds - M1 is symmetric let n be Nat; ::_thesis: for M1 being Matrix of n,K st M1 is symmetric holds - M1 is symmetric let M1 be Matrix of n,K; ::_thesis: ( M1 is symmetric implies - M1 is symmetric ) assume A1: M1 is symmetric ; ::_thesis: - M1 is symmetric (- M1) @ = - (M1 @) by Th26 .= - M1 by A1, Def5 ; hence - M1 is symmetric by Def5; ::_thesis: verum end; theorem :: MATRIX_6:28 for K being Field for n being Nat for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds M1 - M2 is symmetric proof let K be Field; ::_thesis: for n being Nat for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds M1 - M2 is symmetric let n be Nat; ::_thesis: for M1, M2 being Matrix of n,K st M1 is symmetric & M2 is symmetric holds M1 - M2 is symmetric let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is symmetric & M2 is symmetric implies M1 - M2 is symmetric ) assume that A1: M1 is symmetric and A2: M2 is symmetric ; ::_thesis: M1 - M2 is symmetric (M1 - M2) @ = (M1 @) + ((- M2) @) by Th23 .= M1 + ((- M2) @) by A1, Def5 .= M1 + (- (M2 @)) by Th26 .= M1 - M2 by A2, Def5 ; hence M1 - M2 is symmetric by Def5; ::_thesis: verum end; definition let n be Nat; let K be Field; let M1 be Matrix of n,K; attrM1 is antisymmetric means :Def6: :: MATRIX_6:def 6 M1 @ = - M1; end; :: deftheorem Def6 defines antisymmetric MATRIX_6:def_6_:_ for n being Nat for K being Field for M1 being Matrix of n,K holds ( M1 is antisymmetric iff M1 @ = - M1 ); theorem :: MATRIX_6:29 for K being Fanoian Field for n being Nat for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds M1 = 0. (K,n,n) proof let K be Fanoian Field; ::_thesis: for n being Nat for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds M1 = 0. (K,n,n) let n be Nat; ::_thesis: for M1 being Matrix of n,K st M1 is symmetric & M1 is antisymmetric holds M1 = 0. (K,n,n) let M1 be Matrix of n,K; ::_thesis: ( M1 is symmetric & M1 is antisymmetric implies M1 = 0. (K,n,n) ) assume ( M1 is symmetric & M1 is antisymmetric ) ; ::_thesis: M1 = 0. (K,n,n) then A1: ( M1 @ = M1 & M1 @ = - M1 ) by Def5, Def6; for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = (0. (K,n,n)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = (0. (K,n,n)) * (i,j) ) assume A2: [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = (0. (K,n,n)) * (i,j) then M1 * (i,j) = - (M1 * (i,j)) by A1, MATRIX_3:def_2; then (M1 * (i,j)) + (M1 * (i,j)) = 0. K by RLVECT_1:5; then ((1_ K) * (M1 * (i,j))) + (M1 * (i,j)) = 0. K by VECTSP_1:def_8; then ((1_ K) * (M1 * (i,j))) + ((1_ K) * (M1 * (i,j))) = 0. K by VECTSP_1:def_8; then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,j)) = 0. K ) by VECTSP_1:def_7, VECTSP_1:def_19; then A3: M1 * (i,j) = 0. K by VECTSP_1:12; [i,j] in Indices (0. (K,n,n)) by A2, MATRIX_1:26; hence M1 * (i,j) = (0. (K,n,n)) * (i,j) by A3, MATRIX_3:1; ::_thesis: verum end; hence M1 = 0. (K,n,n) by MATRIX_1:27; ::_thesis: verum end; theorem :: MATRIX_6:30 for K being Fanoian Field for n, i being Nat for M1 being Matrix of n,K st M1 is antisymmetric & i in Seg n holds M1 * (i,i) = 0. K proof let K be Fanoian Field; ::_thesis: for n, i being Nat for M1 being Matrix of n,K st M1 is antisymmetric & i in Seg n holds M1 * (i,i) = 0. K let n, i be Nat; ::_thesis: for M1 being Matrix of n,K st M1 is antisymmetric & i in Seg n holds M1 * (i,i) = 0. K let M1 be Matrix of n,K; ::_thesis: ( M1 is antisymmetric & i in Seg n implies M1 * (i,i) = 0. K ) assume that A1: M1 is antisymmetric and A2: i in Seg n ; ::_thesis: M1 * (i,i) = 0. K A3: M1 @ = - M1 by A1, Def6; Indices M1 = [:(Seg n),(Seg n):] by MATRIX_1:24; then A4: [i,i] in Indices M1 by A2, ZFMISC_1:87; then (M1 @) * (i,i) = M1 * (i,i) by MATRIX_1:def_6; then M1 * (i,i) = - (M1 * (i,i)) by A4, A3, MATRIX_3:def_2; then (M1 * (i,i)) + (M1 * (i,i)) = 0. K by RLVECT_1:5; then ((1_ K) * (M1 * (i,i))) + (M1 * (i,i)) = 0. K by VECTSP_1:def_8; then ((1_ K) * (M1 * (i,i))) + ((1_ K) * (M1 * (i,i))) = 0. K by VECTSP_1:def_8; then ( (1_ K) + (1_ K) <> 0. K & ((1_ K) + (1_ K)) * (M1 * (i,i)) = 0. K ) by VECTSP_1:def_7, VECTSP_1:def_19; hence M1 * (i,i) = 0. K by VECTSP_1:12; ::_thesis: verum end; theorem :: MATRIX_6:31 for K being Field for n being Nat for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds M1 + M2 is antisymmetric proof let K be Field; ::_thesis: for n being Nat for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds M1 + M2 is antisymmetric let n be Nat; ::_thesis: for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds M1 + M2 is antisymmetric let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is antisymmetric & M2 is antisymmetric implies M1 + M2 is antisymmetric ) assume that A1: M1 is antisymmetric and A2: M2 is antisymmetric ; ::_thesis: M1 + M2 is antisymmetric A3: ( len M1 = n & width M1 = n ) by MATRIX_1:24; A4: ( len M2 = n & width M2 = n ) by MATRIX_1:24; (M1 + M2) @ = (M1 @) + (M2 @) by Th23 .= (- M1) + (M2 @) by A1, Def6 .= (- M1) + (- M2) by A2, Def6 .= - (M1 + M2) by A3, A4, MATRIX_4:12 ; hence M1 + M2 is antisymmetric by Def6; ::_thesis: verum end; theorem :: MATRIX_6:32 for K being Field for n being Nat for M1 being Matrix of n,K st M1 is antisymmetric holds - M1 is antisymmetric proof let K be Field; ::_thesis: for n being Nat for M1 being Matrix of n,K st M1 is antisymmetric holds - M1 is antisymmetric let n be Nat; ::_thesis: for M1 being Matrix of n,K st M1 is antisymmetric holds - M1 is antisymmetric let M1 be Matrix of n,K; ::_thesis: ( M1 is antisymmetric implies - M1 is antisymmetric ) assume A1: M1 is antisymmetric ; ::_thesis: - M1 is antisymmetric (- M1) @ = - (M1 @) by Th26 .= - (- M1) by A1, Def6 ; hence - M1 is antisymmetric by Def6; ::_thesis: verum end; theorem :: MATRIX_6:33 for K being Field for n being Nat for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds M1 - M2 is antisymmetric proof let K be Field; ::_thesis: for n being Nat for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds M1 - M2 is antisymmetric let n be Nat; ::_thesis: for M1, M2 being Matrix of n,K st M1 is antisymmetric & M2 is antisymmetric holds M1 - M2 is antisymmetric let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is antisymmetric & M2 is antisymmetric implies M1 - M2 is antisymmetric ) assume that A1: M1 is antisymmetric and A2: M2 is antisymmetric ; ::_thesis: M1 - M2 is antisymmetric A3: ( len (- M2) = n & width (- M2) = n ) by MATRIX_1:24; A4: ( len M1 = n & width M1 = n ) by MATRIX_1:24; (M1 - M2) @ = (M1 @) + ((- M2) @) by Th23 .= (- M1) + ((- M2) @) by A1, Def6 .= (- M1) + (- (M2 @)) by Th26 .= (- M1) + (- (- M2)) by A2, Def6 .= - (M1 - M2) by A3, A4, MATRIX_4:12 ; hence M1 - M2 is antisymmetric by Def6; ::_thesis: verum end; theorem :: MATRIX_6:34 for n being Nat for K being Field for M1 being Matrix of n,K st n > 0 holds M1 - (M1 @) is antisymmetric proof let n be Nat; ::_thesis: for K being Field for M1 being Matrix of n,K st n > 0 holds M1 - (M1 @) is antisymmetric let K be Field; ::_thesis: for M1 being Matrix of n,K st n > 0 holds M1 - (M1 @) is antisymmetric let M1 be Matrix of n,K; ::_thesis: ( n > 0 implies M1 - (M1 @) is antisymmetric ) assume A1: n > 0 ; ::_thesis: M1 - (M1 @) is antisymmetric set M2 = M1 - (M1 @); A2: ( len M1 = n & width M1 = n ) by MATRIX_1:24; A3: ( len (M1 @) = n & width (M1 @) = n ) by MATRIX_1:24; (M1 - (M1 @)) @ = (M1 @) + ((- (M1 @)) @) by Th23 .= (M1 @) + (- ((M1 @) @)) by Th26 .= (M1 @) - M1 by A1, A2, MATRIX_2:13 .= - (M1 - (M1 @)) by A2, A3, MATRIX_4:43 ; hence M1 - (M1 @) is antisymmetric by Def6; ::_thesis: verum end; theorem :: MATRIX_6:35 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 holds ( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) ) proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 holds ( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) ) let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 holds ( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) ) let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 implies ( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) ) ) assume A1: n > 0 ; ::_thesis: ( M1 commutes_with M2 iff (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) ) A2: ( len (M1 * M2) = n & width (M1 * M2) = n ) by MATRIX_1:24; A3: ( len ((M1 * M1) + (M1 * M2)) = n & width ((M1 * M1) + (M1 * M2)) = n ) by MATRIX_1:24; A4: ( len ((M1 * M2) + (M2 * M2)) = n & width ((M1 * M2) + (M2 * M2)) = n ) by MATRIX_1:24; A5: ( len (M1 * M1) = n & width (M1 * M1) = n ) by MATRIX_1:24; A6: ( len M1 = n & width M1 = n ) by MATRIX_1:24; A7: ( len ((M1 * M1) + (M2 * M1)) = n & width ((M1 * M1) + (M2 * M1)) = n ) by MATRIX_1:24; A8: ( len M2 = n & width M2 = n ) by MATRIX_1:24; A9: ( len (M1 + M2) = n & width (M1 + M2) = n ) by MATRIX_1:24; thus ( M1 commutes_with M2 implies (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) ) ::_thesis: ( (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) implies M1 commutes_with M2 ) proof assume A10: M1 commutes_with M2 ; ::_thesis: (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) (M1 + M2) * (M1 + M2) = ((M1 + M2) * M1) + ((M1 + M2) * M2) by A1, A6, A8, A9, MATRIX_4:62 .= ((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) by A1, A6, A8, MATRIX_4:63 .= ((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) by A1, A6, A8, MATRIX_4:63 .= (((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) by A2, A7, MATRIX_3:3 ; hence (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) by A10, Def1; ::_thesis: verum end; assume A11: (M1 + M2) * (M1 + M2) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) ; ::_thesis: M1 commutes_with M2 A12: ( len (M2 * M1) = n & width (M2 * M1) = n ) by MATRIX_1:24; (M1 + M2) * (M1 + M2) = ((M1 + M2) * M1) + ((M1 + M2) * M2) by A1, A6, A8, A9, MATRIX_4:62 .= ((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) by A1, A6, A8, MATRIX_4:63 .= ((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) by A1, A6, A8, MATRIX_4:63 .= (((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) by A2, A7, MATRIX_3:3 ; then ((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) = (((M1 * M1) + (M1 * M2)) + (M1 * M2)) + (M2 * M2) by A2, A7, A11, MATRIX_3:3; then ((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) = ((M1 * M1) + (M1 * M2)) + ((M1 * M2) + (M2 * M2)) by A2, A3, MATRIX_3:3; then (M1 * M1) + (M2 * M1) = (M1 * M1) + (M1 * M2) by A7, A4, A3, MATRIX_4:4; then (M2 * M1) + (M1 * M1) = (M1 * M1) + (M1 * M2) by A5, A12, MATRIX_3:2; then (M2 * M1) + (M1 * M1) = (M1 * M2) + (M1 * M1) by A5, A2, MATRIX_3:2; then M2 * M1 = M1 * M2 by A5, A2, A12, MATRIX_4:4; hence M1 commutes_with M2 by Def1; ::_thesis: verum end; theorem Th36: :: MATRIX_6:36 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible & M2 is invertible implies ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) ) assume that A1: M1 is invertible and A2: M2 is invertible ; ::_thesis: ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) A3: M2 ~ is_reverse_of M2 by A2, Def4; A4: M1 ~ is_reverse_of M1 by A1, Def4; A5: len (M2 ~) = n by MATRIX_1:24; A6: width (M1 ~) = n by MATRIX_1:24; A7: len M1 = n by MATRIX_1:24; A8: width M2 = n by MATRIX_1:24; A9: ( width M1 = n & len M2 = n ) by MATRIX_1:24; A10: ( width (M2 ~) = n & len (M1 ~) = n ) by MATRIX_1:24; width (M1 * M2) = n by MATRIX_1:24; then A11: (M1 * M2) * ((M2 ~) * (M1 ~)) = ((M1 * M2) * (M2 ~)) * (M1 ~) by A5, A10, MATRIX_3:33 .= (M1 * (M2 * (M2 ~))) * (M1 ~) by A9, A8, A5, MATRIX_3:33 .= (M1 * (1. (K,n))) * (M1 ~) by A3, Def2 .= M1 * (M1 ~) by MATRIX_3:19 .= 1. (K,n) by A4, Def2 ; width ((M2 ~) * (M1 ~)) = n by MATRIX_1:24; then ((M2 ~) * (M1 ~)) * (M1 * M2) = (((M2 ~) * (M1 ~)) * M1) * M2 by A9, A7, MATRIX_3:33 .= ((M2 ~) * ((M1 ~) * M1)) * M2 by A7, A6, A10, MATRIX_3:33 .= ((M2 ~) * (1. (K,n))) * M2 by A4, Def2 .= (M2 ~) * M2 by MATRIX_3:19 .= 1. (K,n) by A3, Def2 ; then A12: (M2 ~) * (M1 ~) is_reverse_of M1 * M2 by A11, Def2; then M1 * M2 is invertible by Def3; hence ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) by A12, Def4; ::_thesis: verum end; theorem :: MATRIX_6:37 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible & M1 commutes_with M2 holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) ) proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible & M1 commutes_with M2 holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) ) let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible & M1 commutes_with M2 holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) ) let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible & M2 is invertible & M1 commutes_with M2 implies ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) ) ) assume that A1: M1 is invertible and A2: M2 is invertible and A3: M1 commutes_with M2 ; ::_thesis: ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) ) A4: M2 ~ is_reverse_of M2 by A2, Def4; A5: width ((M1 ~) * (M2 ~)) = n by MATRIX_1:24; A6: width (M2 ~) = n by MATRIX_1:24; A7: len M2 = n by MATRIX_1:24; A8: width M1 = n by MATRIX_1:24; A9: ( width M2 = n & len M1 = n ) by MATRIX_1:24; A10: M1 ~ is_reverse_of M1 by A1, Def4; A11: ( width (M1 ~) = n & len (M2 ~) = n ) by MATRIX_1:24; A12: len (M1 ~) = n by MATRIX_1:24; width (M1 * M2) = n by MATRIX_1:24; then A13: (M1 * M2) * ((M1 ~) * (M2 ~)) = ((M1 * M2) * (M1 ~)) * (M2 ~) by A11, A12, MATRIX_3:33 .= ((M2 * M1) * (M1 ~)) * (M2 ~) by A3, Def1 .= (M2 * (M1 * (M1 ~))) * (M2 ~) by A8, A9, A12, MATRIX_3:33 .= (M2 * (1. (K,n))) * (M2 ~) by A10, Def2 .= M2 * (M2 ~) by MATRIX_3:19 .= 1. (K,n) by A4, Def2 ; ((M1 ~) * (M2 ~)) * (M1 * M2) = ((M1 ~) * (M2 ~)) * (M2 * M1) by A3, Def1 .= (((M1 ~) * (M2 ~)) * M2) * M1 by A7, A9, A5, MATRIX_3:33 .= ((M1 ~) * ((M2 ~) * M2)) * M1 by A7, A11, A6, MATRIX_3:33 .= ((M1 ~) * (1. (K,n))) * M1 by A4, Def2 .= (M1 ~) * M1 by MATRIX_3:19 .= 1. (K,n) by A10, Def2 ; then A14: (M1 ~) * (M2 ~) is_reverse_of M1 * M2 by A13, Def2; then M1 * M2 is invertible by Def3; hence ( M1 * M2 is invertible & (M1 * M2) ~ = (M1 ~) * (M2 ~) ) by A14, Def4; ::_thesis: verum end; theorem :: MATRIX_6:38 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M1 * M2 = 1. (K,n) holds M1 is_reverse_of M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M1 * M2 = 1. (K,n) holds M1 is_reverse_of M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M1 * M2 = 1. (K,n) holds M1 is_reverse_of M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible & M1 * M2 = 1. (K,n) implies M1 is_reverse_of M2 ) A1: ( width M1 = n & len M1 = n ) by MATRIX_1:24; A2: ( len M2 = n & width (M1 ~) = n ) by MATRIX_1:24; assume that A3: M1 is invertible and A4: M1 * M2 = 1. (K,n) ; ::_thesis: M1 is_reverse_of M2 A5: M1 ~ is_reverse_of M1 by A3, Def4; (M1 ~) * (M1 * M2) = M1 ~ by A4, MATRIX_3:19; then ((M1 ~) * M1) * M2 = M1 ~ by A1, A2, MATRIX_3:33; then (1. (K,n)) * M2 = M1 ~ by A5, Def2; then M2 = M1 ~ by MATRIX_3:18; hence M1 is_reverse_of M2 by A3, Def4; ::_thesis: verum end; theorem :: MATRIX_6:39 for n being Nat for K being Field for M2, M1 being Matrix of n,K st M2 is invertible & M2 * M1 = 1. (K,n) holds M1 is_reverse_of M2 proof let n be Nat; ::_thesis: for K being Field for M2, M1 being Matrix of n,K st M2 is invertible & M2 * M1 = 1. (K,n) holds M1 is_reverse_of M2 let K be Field; ::_thesis: for M2, M1 being Matrix of n,K st M2 is invertible & M2 * M1 = 1. (K,n) holds M1 is_reverse_of M2 let M2, M1 be Matrix of n,K; ::_thesis: ( M2 is invertible & M2 * M1 = 1. (K,n) implies M1 is_reverse_of M2 ) A1: ( len M1 = n & width M2 = n ) by MATRIX_1:24; A2: ( len M2 = n & width (M2 ~) = n ) by MATRIX_1:24; assume that A3: M2 is invertible and A4: M2 * M1 = 1. (K,n) ; ::_thesis: M1 is_reverse_of M2 A5: M2 ~ is_reverse_of M2 by A3, Def4; (M2 ~) * (M2 * M1) = M2 ~ by A4, MATRIX_3:19; then ((M2 ~) * M2) * M1 = M2 ~ by A1, A2, MATRIX_3:33; then (1. (K,n)) * M1 = M2 ~ by A5, Def2; then M1 = M2 ~ by MATRIX_3:18; hence M1 is_reverse_of M2 by A3, Def4; ::_thesis: verum end; theorem Th40: :: MATRIX_6:40 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M1 commutes_with M2 holds M1 ~ commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M1 commutes_with M2 holds M1 ~ commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M1 commutes_with M2 holds M1 ~ commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible & M1 commutes_with M2 implies M1 ~ commutes_with M2 ) assume that A1: M1 is invertible and A2: M1 commutes_with M2 ; ::_thesis: M1 ~ commutes_with M2 A3: M1 ~ is_reverse_of M1 by A1, Def4; A4: width M2 = n by MATRIX_1:24; A5: ( width M1 = n & len M1 = n ) by MATRIX_1:24; A6: ( len (M2 * M1) = n & width (M2 * M1) = n ) by MATRIX_1:24; A7: len (M1 ~) = n by MATRIX_1:24; A8: len M2 = n by MATRIX_1:24; A9: width (M1 ~) = n by MATRIX_1:24; M2 = (1. (K,n)) * M2 by MATRIX_3:18 .= ((M1 ~) * M1) * M2 by A3, Def2 .= (M1 ~) * (M1 * M2) by A5, A8, A9, MATRIX_3:33 .= (M1 ~) * (M2 * M1) by A2, Def1 ; then M2 * (M1 ~) = (M1 ~) * ((M2 * M1) * (M1 ~)) by A9, A7, A6, MATRIX_3:33 .= (M1 ~) * (M2 * (M1 * (M1 ~))) by A5, A4, A7, MATRIX_3:33 .= (M1 ~) * (M2 * (1. (K,n))) by A3, Def2 .= (M1 ~) * M2 by MATRIX_3:19 ; hence M1 ~ commutes_with M2 by Def1; ::_thesis: verum end; definition let n be Nat; let K be Field; let M1 be Matrix of n,K; attrM1 is Orthogonal means :Def7: :: MATRIX_6:def 7 ( M1 is invertible & M1 @ = M1 ~ ); end; :: deftheorem Def7 defines Orthogonal MATRIX_6:def_7_:_ for n being Nat for K being Field for M1 being Matrix of n,K holds ( M1 is Orthogonal iff ( M1 is invertible & M1 @ = M1 ~ ) ); theorem Th41: :: MATRIX_6:41 for n being Nat for K being Field for M1 being Matrix of n,K holds ( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal ) proof let n be Nat; ::_thesis: for K being Field for M1 being Matrix of n,K holds ( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal ) let K be Field; ::_thesis: for M1 being Matrix of n,K holds ( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal ) let M1 be Matrix of n,K; ::_thesis: ( ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) iff M1 is Orthogonal ) A1: ( width M1 = n & len M1 = n ) by MATRIX_1:24; A2: len (M1 @) = n by MATRIX_1:24; A3: width (M1 ~) = n by MATRIX_1:24; A4: len (M1 ~) = n by MATRIX_1:24; thus ( M1 * (M1 @) = 1. (K,n) & M1 is invertible implies M1 is Orthogonal ) ::_thesis: ( M1 is Orthogonal implies ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) ) proof assume that A5: M1 * (M1 @) = 1. (K,n) and A6: M1 is invertible ; ::_thesis: M1 is Orthogonal A7: M1 ~ is_reverse_of M1 by A6, Def4; then (M1 ~) * (M1 * (M1 ~)) = (M1 ~) * (M1 * (M1 @)) by A5, Def2; then ((M1 ~) * M1) * (M1 ~) = (M1 ~) * (M1 * (M1 @)) by A1, A3, A4, MATRIX_3:33; then ((M1 ~) * M1) * (M1 ~) = ((M1 ~) * M1) * (M1 @) by A1, A3, A2, MATRIX_3:33; then (1. (K,n)) * (M1 ~) = ((M1 ~) * M1) * (M1 @) by A7, Def2; then (1. (K,n)) * (M1 ~) = (1. (K,n)) * (M1 @) by A7, Def2; then M1 ~ = (1. (K,n)) * (M1 @) by MATRIX_3:18; then M1 ~ = M1 @ by MATRIX_3:18; hence M1 is Orthogonal by A6, Def7; ::_thesis: verum end; assume A8: M1 is Orthogonal ; ::_thesis: ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) then M1 is invertible by Def7; then A9: M1 ~ is_reverse_of M1 by Def4; M1 * (M1 @) = M1 * (M1 ~) by A8, Def7; hence ( M1 * (M1 @) = 1. (K,n) & M1 is invertible ) by A8, A9, Def2, Def7; ::_thesis: verum end; theorem Th42: :: MATRIX_6:42 for n being Nat for K being Field for M1 being Matrix of n,K holds ( ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) iff M1 is Orthogonal ) proof let n be Nat; ::_thesis: for K being Field for M1 being Matrix of n,K holds ( ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) iff M1 is Orthogonal ) let K be Field; ::_thesis: for M1 being Matrix of n,K holds ( ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) iff M1 is Orthogonal ) let M1 be Matrix of n,K; ::_thesis: ( ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) iff M1 is Orthogonal ) A1: ( width M1 = n & len M1 = n ) by MATRIX_1:24; A2: width (M1 @) = n by MATRIX_1:24; A3: len (M1 ~) = n by MATRIX_1:24; A4: width (M1 ~) = n by MATRIX_1:24; thus ( M1 is invertible & (M1 @) * M1 = 1. (K,n) implies M1 is Orthogonal ) ::_thesis: ( M1 is Orthogonal implies ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) ) proof assume that A5: M1 is invertible and A6: (M1 @) * M1 = 1. (K,n) ; ::_thesis: M1 is Orthogonal A7: M1 ~ is_reverse_of M1 by A5, Def4; then ((M1 ~) * M1) * (M1 ~) = ((M1 @) * M1) * (M1 ~) by A6, Def2; then (M1 ~) * (M1 * (M1 ~)) = ((M1 @) * M1) * (M1 ~) by A1, A4, A3, MATRIX_3:33; then (M1 ~) * (M1 * (M1 ~)) = (M1 @) * (M1 * (M1 ~)) by A1, A3, A2, MATRIX_3:33; then (M1 ~) * (1. (K,n)) = (M1 @) * (M1 * (M1 ~)) by A7, Def2; then (M1 ~) * (1. (K,n)) = (M1 @) * (1. (K,n)) by A7, Def2; then M1 ~ = (M1 @) * (1. (K,n)) by MATRIX_3:19; then M1 ~ = M1 @ by MATRIX_3:19; hence M1 is Orthogonal by A5, Def7; ::_thesis: verum end; assume A8: M1 is Orthogonal ; ::_thesis: ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) then M1 is invertible by Def7; then A9: M1 ~ is_reverse_of M1 by Def4; (M1 @) * M1 = (M1 ~) * M1 by A8, Def7; hence ( M1 is invertible & (M1 @) * M1 = 1. (K,n) ) by A8, A9, Def2, Def7; ::_thesis: verum end; theorem :: MATRIX_6:43 for n being Nat for K being Field for M1 being Matrix of n,K st M1 is Orthogonal holds (M1 @) * M1 = M1 * (M1 @) proof let n be Nat; ::_thesis: for K being Field for M1 being Matrix of n,K st M1 is Orthogonal holds (M1 @) * M1 = M1 * (M1 @) let K be Field; ::_thesis: for M1 being Matrix of n,K st M1 is Orthogonal holds (M1 @) * M1 = M1 * (M1 @) let M1 be Matrix of n,K; ::_thesis: ( M1 is Orthogonal implies (M1 @) * M1 = M1 * (M1 @) ) assume A1: M1 is Orthogonal ; ::_thesis: (M1 @) * M1 = M1 * (M1 @) then (M1 @) * M1 = 1. (K,n) by Th42; hence (M1 @) * M1 = M1 * (M1 @) by A1, Th41; ::_thesis: verum end; theorem :: MATRIX_6:44 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds M1 @ commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds M1 @ commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds M1 @ commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Orthogonal & M1 commutes_with M2 implies M1 @ commutes_with M2 ) assume that A1: M1 is Orthogonal and A2: M1 commutes_with M2 ; ::_thesis: M1 @ commutes_with M2 ( M1 @ = M1 ~ & M1 is invertible ) by A1, Def7; hence M1 @ commutes_with M2 by A2, Th40; ::_thesis: verum end; theorem Th45: :: MATRIX_6:45 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is invertible & M2 is invertible holds ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is invertible & M2 is invertible implies ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) ) assume that A1: M1 is invertible and A2: M2 is invertible ; ::_thesis: ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) A3: M1 ~ is_reverse_of M1 by A1, Def4; A4: M2 ~ is_reverse_of M2 by A2, Def4; A5: len M1 = n by MATRIX_1:24; A6: width (M1 ~) = n by MATRIX_1:24; A7: ( width M1 = n & len M2 = n ) by MATRIX_1:24; A8: width M2 = n by MATRIX_1:24; A9: len (M2 ~) = n by MATRIX_1:24; A10: ( width (M2 ~) = n & len (M1 ~) = n ) by MATRIX_1:24; width ((M2 ~) * (M1 ~)) = n by MATRIX_1:24; then A11: ((M2 ~) * (M1 ~)) * (M1 * M2) = (((M2 ~) * (M1 ~)) * M1) * M2 by A7, A5, MATRIX_3:33 .= ((M2 ~) * ((M1 ~) * M1)) * M2 by A5, A6, A10, MATRIX_3:33 .= ((M2 ~) * (1. (K,n))) * M2 by A3, Def2 .= (M2 ~) * M2 by MATRIX_3:19 .= 1. (K,n) by A4, Def2 ; width (M1 * M2) = n by MATRIX_1:24; then (M1 * M2) * ((M2 ~) * (M1 ~)) = ((M1 * M2) * (M2 ~)) * (M1 ~) by A9, A10, MATRIX_3:33 .= (M1 * (M2 * (M2 ~))) * (M1 ~) by A7, A8, A9, MATRIX_3:33 .= (M1 * (1. (K,n))) * (M1 ~) by A4, Def2 .= M1 * (M1 ~) by MATRIX_3:19 .= 1. (K,n) by A3, Def2 ; then A12: (M2 ~) * (M1 ~) is_reverse_of M1 * M2 by A11, Def2; then M1 * M2 is invertible by Def3; hence ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) by A12, Def4; ::_thesis: verum end; theorem :: MATRIX_6:46 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds M1 * M2 is Orthogonal proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds M1 * M2 is Orthogonal let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds M1 * M2 is Orthogonal let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 is Orthogonal & M2 is Orthogonal implies M1 * M2 is Orthogonal ) assume that A1: n > 0 and A2: ( M1 is Orthogonal & M2 is Orthogonal ) ; ::_thesis: M1 * M2 is Orthogonal ( M1 is invertible & M2 is invertible ) by A2, Def7; then A3: ( M1 * M2 is invertible & (M1 * M2) ~ = (M2 ~) * (M1 ~) ) by Th45; A4: width M2 = n by MATRIX_1:24; A5: ( width M1 = n & len M2 = n ) by MATRIX_1:24; ( M1 @ = M1 ~ & M2 @ = M2 ~ ) by A2, Def7; then (M1 * M2) @ = (M2 ~) * (M1 ~) by A1, A5, A4, MATRIX_3:22; hence M1 * M2 is Orthogonal by A3, Def7; ::_thesis: verum end; theorem :: MATRIX_6:47 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds M1 @ commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds M1 @ commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 is Orthogonal & M1 commutes_with M2 holds M1 @ commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 is Orthogonal & M1 commutes_with M2 implies M1 @ commutes_with M2 ) set M3 = M1 @ ; assume that A1: M1 is Orthogonal and A2: M1 commutes_with M2 ; ::_thesis: M1 @ commutes_with M2 M1 is invertible by A1, Def7; then A3: M1 ~ is_reverse_of M1 by Def4; A4: width M2 = n by MATRIX_1:24; A5: width M1 = n by MATRIX_1:24; A6: ( len M2 = n & width (M1 ~) = n ) by MATRIX_1:24; A7: ( len (M1 ~) = n & width ((M1 ~) * M2) = n ) by MATRIX_1:24; A8: len M1 = n by MATRIX_1:24; M2 * (M1 @) = ((1. (K,n)) * M2) * (M1 @) by MATRIX_3:18 .= (((M1 ~) * M1) * M2) * (M1 @) by A3, Def2 .= ((M1 ~) * (M1 * M2)) * (M1 @) by A5, A8, A6, MATRIX_3:33 .= ((M1 ~) * (M2 * M1)) * (M1 @) by A2, Def1 .= ((M1 ~) * (M2 * M1)) * (M1 ~) by A1, Def7 .= (((M1 ~) * M2) * M1) * (M1 ~) by A4, A8, A6, MATRIX_3:33 .= ((M1 ~) * M2) * (M1 * (M1 ~)) by A5, A8, A7, MATRIX_3:33 .= ((M1 ~) * M2) * (1. (K,n)) by A3, Def2 .= (M1 ~) * M2 by MATRIX_3:19 .= (M1 @) * M2 by A1, Def7 ; hence M1 @ commutes_with M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:48 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M1 commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M1 commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M1 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 commutes_with M2 implies M1 + M1 commutes_with M2 ) assume that A1: n > 0 and A2: M1 commutes_with M2 ; ::_thesis: M1 + M1 commutes_with M2 A3: width M2 = n by MATRIX_1:24; A4: len M1 = n by MATRIX_1:24; A5: ( width M1 = n & len M2 = n ) by MATRIX_1:24; then (M1 + M1) * M2 = (M1 * M2) + (M1 * M2) by A1, A4, MATRIX_4:63 .= (M2 * M1) + (M1 * M2) by A2, Def1 .= (M2 * M1) + (M2 * M1) by A2, Def1 .= M2 * (M1 + M1) by A1, A5, A3, A4, MATRIX_4:62 ; hence M1 + M1 commutes_with M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:49 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M2 commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M2 commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M2 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 commutes_with M2 implies M1 + M2 commutes_with M2 ) assume that A1: n > 0 and A2: M1 commutes_with M2 ; ::_thesis: M1 + M2 commutes_with M2 A3: ( width M2 = n & len M1 = n ) by MATRIX_1:24; A4: ( width M1 = n & len M2 = n ) by MATRIX_1:24; then (M1 + M2) * M2 = (M1 * M2) + (M2 * M2) by A1, A3, MATRIX_4:63 .= (M2 * M1) + (M2 * M2) by A2, Def1 .= M2 * (M1 + M2) by A1, A4, A3, MATRIX_4:62 ; hence M1 + M2 commutes_with M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:50 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M1 commutes_with M2 + M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M1 commutes_with M2 + M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M1 commutes_with M2 + M2 let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 commutes_with M2 implies M1 + M1 commutes_with M2 + M2 ) assume that A1: n > 0 and A2: M1 commutes_with M2 ; ::_thesis: M1 + M1 commutes_with M2 + M2 A3: len M2 = n by MATRIX_1:24; A4: len (M1 + M1) = n by MATRIX_1:24; A5: width M2 = n by MATRIX_1:24; A6: ( width M1 = n & len M1 = n ) by MATRIX_1:24; width (M1 + M1) = n by MATRIX_1:24; then (M1 + M1) * (M2 + M2) = ((M1 + M1) * M2) + ((M1 + M1) * M2) by A1, A3, A5, A4, MATRIX_4:62 .= ((M1 * M2) + (M1 * M2)) + ((M1 + M1) * M2) by A1, A3, A6, MATRIX_4:63 .= ((M1 * M2) + (M1 * M2)) + ((M1 * M2) + (M1 * M2)) by A1, A3, A6, MATRIX_4:63 .= ((M2 * M1) + (M1 * M2)) + ((M1 * M2) + (M1 * M2)) by A2, Def1 .= ((M2 * M1) + (M2 * M1)) + ((M1 * M2) + (M1 * M2)) by A2, Def1 .= ((M2 * M1) + (M2 * M1)) + ((M2 * M1) + (M1 * M2)) by A2, Def1 .= ((M2 * M1) + (M2 * M1)) + ((M2 * M1) + (M2 * M1)) by A2, Def1 .= (M2 * (M1 + M1)) + ((M2 * M1) + (M2 * M1)) by A1, A3, A5, A6, MATRIX_4:62 .= (M2 * (M1 + M1)) + (M2 * (M1 + M1)) by A1, A3, A5, A6, MATRIX_4:62 .= (M2 + M2) * (M1 + M1) by A1, A3, A5, A4, MATRIX_4:63 ; hence M1 + M1 commutes_with M2 + M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:51 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M2 commutes_with M2 + M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M2 commutes_with M2 + M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 + M2 commutes_with M2 + M2 let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 commutes_with M2 implies M1 + M2 commutes_with M2 + M2 ) assume that A1: n > 0 and A2: M1 commutes_with M2 ; ::_thesis: M1 + M2 commutes_with M2 + M2 A3: ( len M2 = n & width M2 = n ) by MATRIX_1:24; A4: len (M1 + M2) = n by MATRIX_1:24; A5: ( width M1 = n & len M1 = n ) by MATRIX_1:24; width (M1 + M2) = n by MATRIX_1:24; then (M1 + M2) * (M2 + M2) = ((M1 + M2) * M2) + ((M1 + M2) * M2) by A1, A3, A4, MATRIX_4:62 .= ((M1 * M2) + (M2 * M2)) + ((M1 + M2) * M2) by A1, A3, A5, MATRIX_4:63 .= ((M1 * M2) + (M2 * M2)) + ((M1 * M2) + (M2 * M2)) by A1, A3, A5, MATRIX_4:63 .= ((M2 * M1) + (M2 * M2)) + ((M1 * M2) + (M2 * M2)) by A2, Def1 .= ((M2 * M1) + (M2 * M2)) + ((M2 * M1) + (M2 * M2)) by A2, Def1 .= (M2 * (M1 + M2)) + ((M2 * M1) + (M2 * M2)) by A1, A3, A5, MATRIX_4:62 .= (M2 * (M1 + M2)) + (M2 * (M1 + M2)) by A1, A3, A5, MATRIX_4:62 .= (M2 + M2) * (M1 + M2) by A1, A3, A4, MATRIX_4:63 ; hence M1 + M2 commutes_with M2 + M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:52 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M2 commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M2 commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M2 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 commutes_with M2 implies M1 * M2 commutes_with M2 ) A1: ( width M1 = n & width M2 = n ) by MATRIX_1:24; A2: ( len M1 = n & len M2 = n ) by MATRIX_1:24; assume M1 commutes_with M2 ; ::_thesis: M1 * M2 commutes_with M2 then (M1 * M2) * M2 = (M2 * M1) * M2 by Def1 .= M2 * (M1 * M2) by A1, A2, MATRIX_3:33 ; hence M1 * M2 commutes_with M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:53 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M1 commutes_with M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M1 commutes_with M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M1 commutes_with M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 commutes_with M2 implies M1 * M1 commutes_with M2 ) A1: width M2 = n by MATRIX_1:24; A2: ( width M1 = n & len M1 = n ) by MATRIX_1:24; assume A3: M1 commutes_with M2 ; ::_thesis: M1 * M1 commutes_with M2 A4: len M2 = n by MATRIX_1:24; then (M1 * M1) * M2 = M1 * (M1 * M2) by A2, MATRIX_3:33 .= M1 * (M2 * M1) by A3, Def1 .= (M1 * M2) * M1 by A1, A2, A4, MATRIX_3:33 .= (M2 * M1) * M1 by A3, Def1 .= M2 * (M1 * M1) by A1, A2, MATRIX_3:33 ; hence M1 * M1 commutes_with M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:54 for n being Nat for K being Field for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M1 commutes_with M2 * M2 proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M1 commutes_with M2 * M2 let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st M1 commutes_with M2 holds M1 * M1 commutes_with M2 * M2 let M1, M2 be Matrix of n,K; ::_thesis: ( M1 commutes_with M2 implies M1 * M1 commutes_with M2 * M2 ) A1: width M2 = n by MATRIX_1:24; A2: len (M1 * M1) = n by MATRIX_1:24; A3: ( width M1 = n & len M1 = n ) by MATRIX_1:24; assume A4: M1 commutes_with M2 ; ::_thesis: M1 * M1 commutes_with M2 * M2 A5: len M2 = n by MATRIX_1:24; A6: width (M1 * M1) = n by MATRIX_1:24; then (M1 * M1) * (M2 * M2) = ((M1 * M1) * M2) * M2 by A1, A5, MATRIX_3:33 .= (M1 * (M1 * M2)) * M2 by A3, A5, MATRIX_3:33 .= (M1 * (M2 * M1)) * M2 by A4, Def1 .= ((M1 * M2) * M1) * M2 by A1, A3, A5, MATRIX_3:33 .= ((M2 * M1) * M1) * M2 by A4, Def1 .= (M2 * (M1 * M1)) * M2 by A1, A3, MATRIX_3:33 .= M2 * ((M1 * M1) * M2) by A1, A5, A6, A2, MATRIX_3:33 .= M2 * (M1 * (M1 * M2)) by A3, A5, MATRIX_3:33 .= M2 * (M1 * (M2 * M1)) by A4, Def1 .= M2 * ((M1 * M2) * M1) by A1, A3, A5, MATRIX_3:33 .= M2 * ((M2 * M1) * M1) by A4, Def1 .= M2 * (M2 * (M1 * M1)) by A1, A3, MATRIX_3:33 .= (M2 * M2) * (M1 * M1) by A1, A5, A2, MATRIX_3:33 ; hence M1 * M1 commutes_with M2 * M2 by Def1; ::_thesis: verum end; theorem :: MATRIX_6:55 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 @ commutes_with M2 @ proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 @ commutes_with M2 @ let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 commutes_with M2 holds M1 @ commutes_with M2 @ let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 commutes_with M2 implies M1 @ commutes_with M2 @ ) A1: ( width M1 = n & width M2 = n ) by MATRIX_1:24; set M3 = M1 @ ; set M4 = M2 @ ; A2: len M2 = n by MATRIX_1:24; assume that A3: n > 0 and A4: M1 commutes_with M2 ; ::_thesis: M1 @ commutes_with M2 @ len M1 = n by MATRIX_1:24; then (M1 @) * (M2 @) = (M2 * M1) @ by A1, A3, MATRIX_3:22 .= (M1 * M2) @ by A4, Def1 .= (M2 @) * (M1 @) by A1, A2, A3, MATRIX_3:22 ; hence M1 @ commutes_with M2 @ by Def1; ::_thesis: verum end; theorem Th56: :: MATRIX_6:56 for n being Nat for K being Field for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 is invertible & M3 is invertible holds ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) ) proof let n be Nat; ::_thesis: for K being Field for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 is invertible & M3 is invertible holds ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) ) let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st M1 is invertible & M2 is invertible & M3 is invertible holds ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) ) let M1, M2, M3 be Matrix of n,K; ::_thesis: ( M1 is invertible & M2 is invertible & M3 is invertible implies ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) ) ) assume that A1: M1 is invertible and A2: M2 is invertible and A3: M3 is invertible ; ::_thesis: ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) ) A4: M1 ~ is_reverse_of M1 by A1, Def4; A5: M2 ~ is_reverse_of M2 by A2, Def4; A6: len M3 = n by MATRIX_1:24; A7: M3 ~ is_reverse_of M3 by A3, Def4; A8: width (M2 ~) = n by MATRIX_1:24; A9: width M3 = n by MATRIX_1:24; A10: width (M1 * M2) = n by MATRIX_1:24; A11: len (M1 ~) = n by MATRIX_1:24; set M5 = ((M3 ~) * (M2 ~)) * (M1 ~); set M4 = (M1 * M2) * M3; A12: width M2 = n by MATRIX_1:24; A13: ( len (M2 * M3) = n & width (((M3 ~) * (M2 ~)) * (M1 ~)) = n ) by MATRIX_1:24; A14: len M2 = n by MATRIX_1:24; A15: ( width ((M1 * M2) * M3) = n & len ((M2 ~) * (M1 ~)) = n ) by MATRIX_1:24; A16: len (M3 ~) = n by MATRIX_1:24; A17: width ((M3 ~) * (M2 ~)) = n by MATRIX_1:24; A18: width (M3 ~) = n by MATRIX_1:24; A19: width (M1 ~) = n by MATRIX_1:24; A20: len M1 = n by MATRIX_1:24; A21: len (M2 ~) = n by MATRIX_1:24; A22: width M1 = n by MATRIX_1:24; then A23: (((M3 ~) * (M2 ~)) * (M1 ~)) * ((M1 * M2) * M3) = (((M3 ~) * (M2 ~)) * (M1 ~)) * (M1 * (M2 * M3)) by A12, A14, A6, MATRIX_3:33 .= ((((M3 ~) * (M2 ~)) * (M1 ~)) * M1) * (M2 * M3) by A22, A20, A13, MATRIX_3:33 .= (((M3 ~) * (M2 ~)) * ((M1 ~) * M1)) * (M2 * M3) by A20, A19, A11, A17, MATRIX_3:33 .= (((M3 ~) * (M2 ~)) * (1. (K,n))) * (M2 * M3) by A4, Def2 .= ((M3 ~) * (M2 ~)) * (M2 * M3) by MATRIX_3:19 .= (((M3 ~) * (M2 ~)) * M2) * M3 by A12, A14, A6, A17, MATRIX_3:33 .= ((M3 ~) * ((M2 ~) * M2)) * M3 by A14, A8, A18, A21, MATRIX_3:33 .= ((M3 ~) * (1. (K,n))) * M3 by A5, Def2 .= (M3 ~) * M3 by MATRIX_3:19 .= 1. (K,n) by A7, Def2 ; ((M1 * M2) * M3) * (((M3 ~) * (M2 ~)) * (M1 ~)) = ((M1 * M2) * M3) * ((M3 ~) * ((M2 ~) * (M1 ~))) by A8, A18, A11, A21, MATRIX_3:33 .= (((M1 * M2) * M3) * (M3 ~)) * ((M2 ~) * (M1 ~)) by A18, A16, A15, MATRIX_3:33 .= ((M1 * M2) * (M3 * (M3 ~))) * ((M2 ~) * (M1 ~)) by A9, A6, A10, A16, MATRIX_3:33 .= ((M1 * M2) * (1. (K,n))) * ((M2 ~) * (M1 ~)) by A7, Def2 .= (M1 * M2) * ((M2 ~) * (M1 ~)) by MATRIX_3:19 .= ((M1 * M2) * (M2 ~)) * (M1 ~) by A10, A8, A11, A21, MATRIX_3:33 .= (M1 * (M2 * (M2 ~))) * (M1 ~) by A22, A12, A14, A21, MATRIX_3:33 .= (M1 * (1. (K,n))) * (M1 ~) by A5, Def2 .= M1 * (M1 ~) by MATRIX_3:19 .= 1. (K,n) by A4, Def2 ; then A24: ((M3 ~) * (M2 ~)) * (M1 ~) is_reverse_of (M1 * M2) * M3 by A23, Def2; then (M1 * M2) * M3 is invertible by Def3; hence ( (M1 * M2) * M3 is invertible & ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) ) by A24, Def4; ::_thesis: verum end; theorem :: MATRIX_6:57 for n being Nat for K being Field for M1, M2, M3 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal holds (M1 * M2) * M3 is Orthogonal proof let n be Nat; ::_thesis: for K being Field for M1, M2, M3 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal holds (M1 * M2) * M3 is Orthogonal let K be Field; ::_thesis: for M1, M2, M3 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal holds (M1 * M2) * M3 is Orthogonal let M1, M2, M3 be Matrix of n,K; ::_thesis: ( n > 0 & M1 is Orthogonal & M2 is Orthogonal & M3 is Orthogonal implies (M1 * M2) * M3 is Orthogonal ) assume that A1: n > 0 and A2: ( M1 is Orthogonal & M2 is Orthogonal ) and A3: M3 is Orthogonal ; ::_thesis: (M1 * M2) * M3 is Orthogonal A4: M3 is invertible by A3, Def7; set M5 = ((M3 ~) * (M2 ~)) * (M1 ~); set M4 = (M1 * M2) * M3; A5: ( width M1 = n & len M2 = n ) by MATRIX_1:24; ( M1 is invertible & M2 is invertible ) by A2, Def7; then A6: ( ((M1 * M2) * M3) ~ = ((M3 ~) * (M2 ~)) * (M1 ~) & (M1 * M2) * M3 is invertible ) by A4, Th56; A7: ( width M2 = n & M3 @ = M3 ~ ) by A3, Def7, MATRIX_1:24; A8: ( width (M2 ~) = n & width (M3 ~) = n ) by MATRIX_1:24; A9: ( M1 @ = M1 ~ & M2 @ = M2 ~ ) by A2, Def7; A10: width (M1 * M2) = n by MATRIX_1:24; A11: ( len (M1 ~) = n & len (M2 ~) = n ) by MATRIX_1:24; ( len M3 = n & width M3 = n ) by MATRIX_1:24; then ((M1 * M2) * M3) @ = (M3 @) * ((M1 * M2) @) by A1, A10, MATRIX_3:22 .= (M3 ~) * ((M2 ~) * (M1 ~)) by A1, A5, A9, A7, MATRIX_3:22 .= ((M3 ~) * (M2 ~)) * (M1 ~) by A8, A11, MATRIX_3:33 ; hence (M1 * M2) * M3 is Orthogonal by A6, Def7; ::_thesis: verum end; theorem :: MATRIX_6:58 for n being Nat for K being Field holds 1. (K,n) is Orthogonal proof let n be Nat; ::_thesis: for K being Field holds 1. (K,n) is Orthogonal let K be Field; ::_thesis: 1. (K,n) is Orthogonal A1: (1. (K,n)) @ = 1. (K,n) by Th10; ( (1. (K,n)) ~ = 1. (K,n) & 1. (K,n) is invertible ) by Th8; hence 1. (K,n) is Orthogonal by A1, Def7; ::_thesis: verum end; theorem :: MATRIX_6:59 for n being Nat for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds (M1 ~) * M2 is Orthogonal proof let n be Nat; ::_thesis: for K being Field for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds (M1 ~) * M2 is Orthogonal let K be Field; ::_thesis: for M1, M2 being Matrix of n,K st n > 0 & M1 is Orthogonal & M2 is Orthogonal holds (M1 ~) * M2 is Orthogonal let M1, M2 be Matrix of n,K; ::_thesis: ( n > 0 & M1 is Orthogonal & M2 is Orthogonal implies (M1 ~) * M2 is Orthogonal ) assume that A1: n > 0 and A2: M1 is Orthogonal and A3: M2 is Orthogonal ; ::_thesis: (M1 ~) * M2 is Orthogonal A4: M1 is invertible by A2, Def7; then A5: M1 ~ is invertible by Th16; A6: M2 is invertible by A3, Def7; then A7: (M1 ~) * M2 is invertible by A5, Th36; ((M1 ~) * M2) ~ = (M2 ~) * ((M1 ~) ~) by A6, A5, Th36; then A8: ((M1 ~) * M2) ~ = (M2 ~) * M1 by A4, Th16; A9: len M2 = n by MATRIX_1:24; A10: ( width (M1 ~) = n & width M2 = n ) by MATRIX_1:24; A11: ( width M1 = n & len M1 = n ) by MATRIX_1:24; ( M1 @ = M1 ~ & M2 @ = M2 ~ ) by A2, A3, Def7; then ((M1 ~) * M2) @ = (M2 ~) * ((M1 @) @) by A1, A10, A9, MATRIX_3:22 .= (M2 ~) * M1 by A1, A11, MATRIX_2:13 ; hence (M1 ~) * M2 is Orthogonal by A7, A8, Def7; ::_thesis: verum end;