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