:: MATRIXR2 semantic presentation
begin
Lm1: for F1, F2 being FinSequence of REAL
for j being Element of NAT st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: for j being Element of NAT st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)
let j be Element of NAT ; ::_thesis: ( len F1 = len F2 implies (F1 - F2) . j = (F1 . j) - (F2 . j) )
reconsider n = len F1 as Element of NAT ;
reconsider G1 = F1 as Element of n -tuples_on REAL by FINSEQ_2:92;
assume len F1 = len F2 ; ::_thesis: (F1 - F2) . j = (F1 . j) - (F2 . j)
then reconsider G2 = F2 as Element of n -tuples_on REAL by FINSEQ_2:92;
(G1 - G2) . j = (G1 . j) - (G2 . j) by RVSUM_1:27;
hence (F1 - F2) . j = (F1 . j) - (F2 . j) ; ::_thesis: verum
end;
theorem Th1: :: MATRIXR2:1
for x, y being FinSequence of REAL st len x = len y & x + y = 0* (len x) holds
( x = - y & y = - x )
proof
let x, y be FinSequence of REAL ; ::_thesis: ( len x = len y & x + y = 0* (len x) implies ( x = - y & y = - x ) )
assume that
A1: len x = len y and
A2: x + y = 0* (len x) ; ::_thesis: ( x = - y & y = - x )
A3: x = (0* (len x)) - y by A1, A2, MATRIXR1:14;
hence x = - y by A1, MATRIXR1:6; ::_thesis: y = - x
thus - x = - (- y) by A1, A3, MATRIXR1:6
.= y ; ::_thesis: verum
end;
Lm2: for D being non empty set
for i being Element of NAT
for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i
proof
let D be non empty set ; ::_thesis: for i being Element of NAT
for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i
let i be Element of NAT ; ::_thesis: for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i
let A be Matrix of D; ::_thesis: ( 1 <= i & i <= len A implies Line (A,i) = A . i )
assume ( 1 <= i & i <= len A ) ; ::_thesis: Line (A,i) = A . i
then i in dom A by FINSEQ_3:25;
hence Line (A,i) = A . i by MATRIX_2:16; ::_thesis: verum
end;
theorem Th2: :: MATRIXR2:2
for D being non empty set
for i, j being Element of NAT
for A being Matrix of D
for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * (i,j) = p . j
proof
let D be non empty set ; ::_thesis: for i, j being Element of NAT
for A being Matrix of D
for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * (i,j) = p . j
let i, j be Element of NAT ; ::_thesis: for A being Matrix of D
for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * (i,j) = p . j
let A be Matrix of D; ::_thesis: for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * (i,j) = p . j
let p be FinSequence of D; ::_thesis: ( p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A implies A * (i,j) = p . j )
assume that
A1: p = A . i and
A2: ( 1 <= i & i <= len A ) and
A3: ( 1 <= j & j <= width A ) and
A4: len p = width A ; ::_thesis: A * (i,j) = p . j
A5: j in Seg (width A) by A3;
then j in dom p by A4, FINSEQ_1:def_3;
then ( rng p c= D & p . j in rng p ) by FINSEQ_1:def_4, FUNCT_1:def_3;
then reconsider xp = p . j as Element of D ;
A6: xp = p . j ;
i in dom A by A2, FINSEQ_3:25;
then [i,j] in Indices A by A5, ZFMISC_1:87;
hence A * (i,j) = p . j by A1, A6, MATRIX_1:def_5; ::_thesis: verum
end;
theorem Th3: :: MATRIXR2:3
for i, j being Element of NAT
for a being real number
for A being Matrix of REAL st [i,j] in Indices A holds
(a * A) * (i,j) = a * (A * (i,j))
proof
let i, j be Element of NAT ; ::_thesis: for a being real number
for A being Matrix of REAL st [i,j] in Indices A holds
(a * A) * (i,j) = a * (A * (i,j))
let a be real number ; ::_thesis: for A being Matrix of REAL st [i,j] in Indices A holds
(a * A) * (i,j) = a * (A * (i,j))
let A be Matrix of REAL; ::_thesis: ( [i,j] in Indices A implies (a * A) * (i,j) = a * (A * (i,j)) )
assume A1: [i,j] in Indices A ; ::_thesis: (a * A) * (i,j) = a * (A * (i,j))
reconsider aa = a as Element of F_Real by XREAL_0:def_1;
(a * A) * (i,j) = (MXF2MXR (aa * (MXR2MXF A))) * (i,j) by MATRIXR1:def_7
.= aa * ((MXR2MXF A) * (i,j)) by A1, MATRIX_3:def_5
.= a * (A * (i,j)) ;
hence (a * A) * (i,j) = a * (A * (i,j)) ; ::_thesis: verum
end;
theorem Th4: :: MATRIXR2:4
for n being Element of NAT
for A, B being Matrix of n, REAL holds
( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
proof
let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL holds
( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
let A, B be Matrix of n, REAL ; ::_thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
A1: len B = n by MATRIX_1:25;
A2: len A = n by MATRIX_1:25;
percases ( n > 0 or n <= 0 ) ;
supposeA3: n > 0 ; ::_thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
then width (MXR2MXF A) = n by MATRIX_1:23
.= len (MXR2MXF B) by MATRIX_1:25 ;
then ( len (A * B) = len A & width (A * B) = width B ) by MATRIX_3:def_4;
hence ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) by A1, A3, MATRIX_1:20, MATRIX_1:25; ::_thesis: verum
end;
supposeA4: n <= 0 ; ::_thesis: ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )
then A5: width (MXR2MXF A) = 0 by A2, MATRIX_1:def_3
.= len (MXR2MXF B) by A4, MATRIX_1:25 ;
then len (A * B) = len A by MATRIX_3:def_4;
hence ( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n ) by A2, A4, A5, MATRIX_1:def_3, MATRIX_3:def_4; ::_thesis: verum
end;
end;
end;
theorem Th5: :: MATRIXR2:5
for a being real number
for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )
proof
let a be real number ; ::_thesis: for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )
let A be Matrix of REAL; ::_thesis: ( len (a * A) = len A & width (a * A) = width A )
reconsider ea = a as Element of F_Real by XREAL_0:def_1;
A1: width (a * A) = width (MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) by MATRIXR1:def_7
.= width A by MATRIX_3:def_5 ;
len (a * A) = len (MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) by MATRIXR1:def_7
.= len A by MATRIX_3:def_5 ;
hence ( len (a * A) = len A & width (a * A) = width A ) by A1; ::_thesis: verum
end;
begin
theorem Th6: :: MATRIXR2:6
for A, B being Matrix of REAL st len A = len B & width A = width B holds
( len (A - B) = len A & width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B implies ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) ) )
assume A1: ( len A = len B & width A = width B ) ; ::_thesis: ( len (A - B) = len A & width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )
thus len (A - B) = len (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF B)))) by MATRIX_4:def_1
.= len A by MATRIX_3:def_3 ; ::_thesis: ( width (A - B) = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )
thus width (A - B) = width (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF B)))) by MATRIX_4:def_1
.= width A by MATRIX_3:def_3 ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j))
thus for i, j being Element of NAT st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) by A1, MATRIX10:3; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let A, B be Matrix of n, REAL ;
:: original: *
redefine funcA * B -> Matrix of n, REAL ;
coherence
A * B is Matrix of n, REAL
proof
A1: ( len A = n & width B = n ) by MATRIX_1:24;
( len (A * B) = len A & width (A * B) = width B ) by Th4;
hence A * B is Matrix of n, REAL by A1, MATRIX_2:7; ::_thesis: verum
end;
end;
theorem Th7: :: MATRIXR2:7
for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds
A + (B - B) = A
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len A > 0 implies A + (B - B) = A )
assume ( len A = len B & width A = width B & len A > 0 ) ; ::_thesis: A + (B - B) = A
hence A = A + (0_Rmatrix ((len B),(width B))) by MATRIXR1:36
.= (MXF2MXR (MXR2MXF A)) + (MXF2MXR ((MXR2MXF B) + (- (MXR2MXF B)))) by MATRIX_4:2
.= A + (B - B) by MATRIX_4:def_1 ;
::_thesis: verum
end;
theorem :: MATRIXR2:8
for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds
(A + B) - B = A
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len A > 0 implies (A + B) - B = A )
assume that
A1: ( len A = len B & width A = width B ) and
A2: len A > 0 ; ::_thesis: (A + B) - B = A
thus (A + B) - B = (A + B) + (- B) by MATRIX_4:def_1
.= A + (B + (- B)) by A1, MATRIX_3:3
.= A + (B - B) by MATRIX_4:def_1
.= A by A1, A2, Th7 ; ::_thesis: verum
end;
Lm3: for i, j being Element of NAT
for A being Matrix of REAL st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
proof
let i, j be Element of NAT ; ::_thesis: for A being Matrix of REAL st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
let A be Matrix of REAL; ::_thesis: ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) )
assume [i,j] in Indices A ; ::_thesis: (- A) * (i,j) = - (A * (i,j))
then (- A) * (i,j) = - ((MXR2MXF A) * (i,j)) by MATRIX_3:def_2;
hence (- A) * (i,j) = - (A * (i,j)) ; ::_thesis: verum
end;
theorem Th9: :: MATRIXR2:9
for A being Matrix of REAL holds (- 1) * A = - A
proof
let A be Matrix of REAL; ::_thesis: (- 1) * A = - A
A1: width ((- 1) * A) = width A by Th5;
A2: len ((- 1) * A) = len A by Th5;
A3: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((-_1)_*_A)_holds_
((-_1)_*_A)_*_(i,j)_=_(-_A)_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((- 1) * A) implies ((- 1) * A) * (i,j) = (- A) * (i,j) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12;
assume A4: [i,j] in Indices ((- 1) * A) ; ::_thesis: ((- 1) * A) * (i,j) = (- A) * (i,j)
then A5: ( 1 <= j0 & j0 <= width A ) by A1, MATRIXC1:1;
( 1 <= i0 & i0 <= len A ) by A2, A4, MATRIXC1:1;
then A6: [i0,j0] in Indices A by A5, MATRIXC1:1;
hence ((- 1) * A) * (i,j) = (- 1) * (A * (i0,j0)) by Th3
.= - (A * (i,j))
.= (- A) * (i,j) by A6, Lm3 ;
::_thesis: verum
end;
( len (- A) = len A & width (- A) = width A ) by MATRIX_3:def_2;
hence (- 1) * A = - A by A2, A1, A3, MATRIX_1:21; ::_thesis: verum
end;
theorem Th10: :: MATRIXR2:10
for A being Matrix of REAL
for i, j being Element of NAT st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
proof
let A be Matrix of REAL; ::_thesis: for i, j being Element of NAT st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices A implies (- A) * (i,j) = - (A * (i,j)) )
assume A1: [i,j] in Indices A ; ::_thesis: (- A) * (i,j) = - (A * (i,j))
- A = (- 1) * A by Th9;
then (- A) * (i,j) = (- 1) * (A * (i,j)) by A1, MATRIXR1:29;
hence (- A) * (i,j) = - (A * (i,j)) ; ::_thesis: verum
end;
theorem :: MATRIXR2:11
for a, b being Real
for A being Matrix of REAL holds (a * b) * A = a * (b * A)
proof
let a, b be Real; ::_thesis: for A being Matrix of REAL holds (a * b) * A = a * (b * A)
let A be Matrix of REAL; ::_thesis: (a * b) * A = a * (b * A)
A1: ( len ((a * b) * A) = len A & width ((a * b) * A) = width A ) by Th5;
A2: len (a * (b * A)) = len (b * A) by Th5;
A3: width (a * (b * A)) = width (b * A) by Th5;
then A4: width (a * (b * A)) = width A by Th5;
A5: ( len (b * A) = len A & width (b * A) = width A ) by Th5;
A6: for i, j being Nat st [i,j] in Indices (a * (b * A)) holds
(a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (b * A)) implies (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) )
assume A7: [i,j] in Indices (a * (b * A)) ; ::_thesis: (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)
A8: Indices (b * A) = Indices A by A5, MATRIX_4:55;
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12;
A9: Indices (a * (b * A)) = Indices (b * A) by A2, A3, MATRIX_4:55;
then (a * (b * A)) * (i,j) = a * ((b * A) * (i0,j0)) by A7, Th3
.= a * (b * (A * (i0,j0))) by A7, A9, A8, Th3
.= (a * b) * (A * (i0,j0))
.= ((a * b) * A) * (i,j) by A7, A9, A8, Th3 ;
hence (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) ; ::_thesis: verum
end;
len (a * (b * A)) = len A by A2, Th5;
hence (a * b) * A = a * (b * A) by A1, A4, A6, MATRIX_1:21; ::_thesis: verum
end;
theorem Th12: :: MATRIXR2:12
for a, b being Real
for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)
proof
let a, b be Real; ::_thesis: for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)
let A be Matrix of REAL; ::_thesis: (a + b) * A = (a * A) + (b * A)
A1: ( len (a * A) = len A & width (a * A) = width A ) by MATRIXR1:27;
A2: ( len ((a + b) * A) = len A & width ((a + b) * A) = width A ) by MATRIXR1:27;
A3: for i, j being Nat st [i,j] in Indices ((a + b) * A) holds
((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((a + b) * A) implies ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) )
assume A4: [i,j] in Indices ((a + b) * A) ; ::_thesis: ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j)
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12;
A5: Indices ((a + b) * A) = Indices A by A2, MATRIX_4:55;
Indices (a * A) = Indices A by A1, MATRIX_4:55;
then ((a * A) + (b * A)) * (i,j) = ((a * A) * (i0,j0)) + ((b * A) * (i0,j0)) by A4, A5, MATRIXR1:25
.= (a * (A * (i0,j0))) + ((b * A) * (i0,j0)) by A4, A5, MATRIXR1:29
.= (a * (A * (i0,j0))) + (b * (A * (i0,j0))) by A4, A5, MATRIXR1:29
.= (a + b) * (A * (i,j)) ;
hence ((a + b) * A) * (i,j) = ((a * A) + (b * A)) * (i,j) by A4, A5, MATRIXR1:29; ::_thesis: verum
end;
( len ((a * A) + (b * A)) = len (a * A) & width ((a * A) + (b * A)) = width (a * A) ) by MATRIX_3:def_3;
hence (a + b) * A = (a * A) + (b * A) by A2, A1, A3, MATRIX_1:21; ::_thesis: verum
end;
theorem :: MATRIXR2:13
for a, b being Real
for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A)
proof
let a, b be Real; ::_thesis: for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A)
let A be Matrix of REAL; ::_thesis: (a - b) * A = (a * A) - (b * A)
A1: ( len ((a - b) * A) = len A & width ((a - b) * A) = width A ) by MATRIXR1:27;
A2: ( len (a * A) = len A & width (a * A) = width A ) by MATRIXR1:27;
A3: ( len (b * A) = len A & width (b * A) = width A ) by MATRIXR1:27;
A4: for i, j being Nat st [i,j] in Indices ((a - b) * A) holds
((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((a - b) * A) implies ((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j) )
assume A5: [i,j] in Indices ((a - b) * A) ; ::_thesis: ((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j)
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12;
A6: Indices ((a - b) * A) = Indices A by A1, MATRIX_4:55;
Indices (a * A) = Indices A by A2, MATRIX_4:55;
then ((a * A) - (b * A)) * (i,j) = ((a * A) * (i0,j0)) - ((b * A) * (i0,j0)) by A2, A3, A5, A6, Th6
.= (a * (A * (i0,j0))) - ((b * A) * (i0,j0)) by A5, A6, MATRIXR1:29
.= (a * (A * (i0,j0))) - (b * (A * (i0,j0))) by A5, A6, MATRIXR1:29
.= (a - b) * (A * (i,j)) ;
hence ((a - b) * A) * (i,j) = ((a * A) - (b * A)) * (i,j) by A5, A6, MATRIXR1:29; ::_thesis: verum
end;
A7: width ((a * A) - (b * A)) = width (MXF2MXR ((MXR2MXF (a * A)) + (- (MXR2MXF (b * A))))) by MATRIX_4:def_1
.= width (a * A) by MATRIX_3:def_3 ;
len ((a * A) - (b * A)) = len (MXF2MXR ((MXR2MXF (a * A)) + (- (MXR2MXF (b * A))))) by MATRIX_4:def_1
.= len (a * A) by MATRIX_3:def_3 ;
hence (a - b) * A = (a * A) - (b * A) by A1, A7, A2, A4, MATRIX_1:21; ::_thesis: verum
end;
theorem Th14: :: MATRIXR2:14
for n being Element of NAT
for K being Field
for A being Matrix of K st n > 0 & len A > 0 holds
(0. (K,n,(len A))) * A = 0. (K,n,(width A))
proof
let n be Element of NAT ; ::_thesis: for K being Field
for A being Matrix of K st n > 0 & len A > 0 holds
(0. (K,n,(len A))) * A = 0. (K,n,(width A))
let K be Field; ::_thesis: for A being Matrix of K st n > 0 & len A > 0 holds
(0. (K,n,(len A))) * A = 0. (K,n,(width A))
let A be Matrix of K; ::_thesis: ( n > 0 & len A > 0 implies (0. (K,n,(len A))) * A = 0. (K,n,(width A)) )
assume that
A1: n > 0 and
A2: len A > 0 ; ::_thesis: (0. (K,n,(len A))) * A = 0. (K,n,(width A))
A3: len (0. (K,n,(len A))) = n by MATRIX_1:def_2;
then A4: width (0. (K,n,(len A))) = len A by A1, MATRIX_1:20;
then A5: len ((0. (K,n,(len A))) * A) = n by A3, MATRIX_3:def_4;
A6: width ((0. (K,n,(len A))) * A) = width A by A4, MATRIX_3:def_4;
((0. (K,n,(len A))) * A) + ((0. (K,n,(len A))) * A) = ((0. (K,n,(len A))) + (0. (K,n,(len A)))) * A by A1, A2, A3, A4, MATRIX_4:63
.= (0. (K,n,(len A))) * A by MATRIX_3:4 ;
hence (0. (K,n,(len A))) * A = 0. (K,n,(width A)) by A5, A6, MATRIX_4:6; ::_thesis: verum
end;
theorem Th15: :: MATRIXR2:15
for K being Field
for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds
(- C) * A = - (C * A)
proof
let K be Field; ::_thesis: for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds
(- C) * A = - (C * A)
let A, C be Matrix of K; ::_thesis: ( len A = width C & len C > 0 & len A > 0 implies (- C) * A = - (C * A) )
assume that
A1: len A = width C and
A2: len C > 0 and
A3: len A > 0 ; ::_thesis: (- C) * A = - (C * A)
A4: len C = len (- C) by MATRIX_3:def_2;
A5: width (- C) = width C by MATRIX_3:def_2;
then width ((- C) * A) = width A by A1, MATRIX_3:def_4;
then A6: width (C * A) = width ((- C) * A) by A1, MATRIX_3:def_4;
reconsider D = C as Matrix of len C, width C,K by A2, MATRIX_1:20;
A7: width (- C) = width C by MATRIX_3:def_2;
then A8: ( len ((- C) * A) = len (- C) & width ((- C) * A) = width A ) by A1, MATRIX_3:def_4;
len (- C) = len ((- C) * A) by A1, A5, MATRIX_3:def_4;
then A9: len (C * A) = len ((- C) * A) by A1, A4, MATRIX_3:def_4;
len C = len (- C) by MATRIX_3:def_2;
then (C * A) + ((- C) * A) = (D + (- D)) * A by A1, A2, A3, A7, MATRIX_4:63
.= (0. (K,(len C),(width C))) * A by MATRIX_3:5
.= 0. (K,(len C),(width A)) by A1, A2, A3, Th14 ;
hence (- C) * A = - (C * A) by A4, A8, A9, A6, MATRIX_4:8; ::_thesis: verum
end;
theorem Th16: :: MATRIXR2:16
for K being Field
for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds
(B - C) * A = (B * A) - (C * A)
proof
let K be Field; ::_thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds
(B - C) * A = (B * A) - (C * A)
let A, B, C be Matrix of K; ::_thesis: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 implies (B - C) * A = (B * A) - (C * A) )
assume A1: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 ) ; ::_thesis: (B - C) * A = (B * A) - (C * A)
A2: ( width (- C) = width C & len C = len (- C) ) by MATRIX_3:def_2;
thus (B - C) * A = (B + (- C)) * A by MATRIX_4:def_1
.= (B * A) + ((- C) * A) by A1, A2, MATRIX_4:63
.= (B * A) + (- (C * A)) by A1, Th15
.= (B * A) - (C * A) by MATRIX_4:def_1 ; ::_thesis: verum
end;
theorem :: MATRIXR2:17
for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = width A & len A > 0 & len C > 0 holds
(A - B) * C = (A * C) - (B * C) by Th16;
theorem Th18: :: MATRIXR2:18
for K being Field
for m being Element of NAT
for A, C being Matrix of K st width A > 0 & len A > 0 holds
A * (0. (K,(width A),m)) = 0. (K,(len A),m)
proof
let K be Field; ::_thesis: for m being Element of NAT
for A, C being Matrix of K st width A > 0 & len A > 0 holds
A * (0. (K,(width A),m)) = 0. (K,(len A),m)
let m be Element of NAT ; ::_thesis: for A, C being Matrix of K st width A > 0 & len A > 0 holds
A * (0. (K,(width A),m)) = 0. (K,(len A),m)
let A, C be Matrix of K; ::_thesis: ( width A > 0 & len A > 0 implies A * (0. (K,(width A),m)) = 0. (K,(len A),m) )
assume that
A1: width A > 0 and
A2: len A > 0 ; ::_thesis: A * (0. (K,(width A),m)) = 0. (K,(len A),m)
A3: len (0. (K,(width A),m)) = width A by MATRIX_1:def_2;
then m = width (0. (K,(width A),m)) by A1, MATRIX_1:20;
then A4: width (A * (0. (K,(width A),m))) = m by A3, MATRIX_3:def_4;
width (0. (K,(width A),m)) = m by A1, A3, MATRIX_1:20;
then A5: (A * (0. (K,(width A),m))) + (A * (0. (K,(width A),m))) = A * ((0. (K,(width A),m)) + (0. (K,(width A),m))) by A1, A2, A3, MATRIX_4:62
.= A * (0. (K,(width A),m)) by MATRIX_3:4 ;
len (A * (0. (K,(width A),m))) = len A by A3, MATRIX_3:def_4;
hence A * (0. (K,(width A),m)) = 0. (K,(len A),m) by A4, A5, MATRIX_4:6; ::_thesis: verum
end;
theorem Th19: :: MATRIXR2:19
for K being Field
for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds
A * (- C) = - (A * C)
proof
let K be Field; ::_thesis: for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds
A * (- C) = - (A * C)
let A, C be Matrix of K; ::_thesis: ( width A = len C & len A > 0 & len C > 0 implies A * (- C) = - (A * C) )
assume that
A1: width A = len C and
A2: len A > 0 and
A3: len C > 0 ; ::_thesis: A * (- C) = - (A * C)
A4: len C = len (- C) by MATRIX_3:def_2;
then A5: len A = len (A * (- C)) by A1, MATRIX_3:def_4;
width (- C) = width C by MATRIX_3:def_2;
then A6: width (A * (- C)) = width C by A1, A4, MATRIX_3:def_4;
reconsider D = C as Matrix of len C, width C,K by A3, MATRIX_1:20;
A7: ( len (A * C) = len A & width (A * C) = width C ) by A1, MATRIX_3:def_4;
( len C = len (- C) & width (- C) = width C ) by MATRIX_3:def_2;
then (A * C) + (A * (- C)) = A * (D + (- D)) by A1, A2, A3, MATRIX_4:62
.= A * (0. (K,(len C),(width C))) by MATRIX_3:5
.= 0. (K,(len A),(width C)) by A1, A2, A3, Th18 ;
hence A * (- C) = - (A * C) by A7, A5, A6, MATRIX_4:8; ::_thesis: verum
end;
theorem Th20: :: MATRIXR2:20
for K being Field
for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds
A * (B - C) = (A * B) - (A * C)
proof
let K be Field; ::_thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds
A * (B - C) = (A * B) - (A * C)
let A, B, C be Matrix of K; ::_thesis: ( len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 implies A * (B - C) = (A * B) - (A * C) )
assume that
A1: len B = len C and
A2: width B = width C and
A3: ( len B = width A & len B > 0 & len A > 0 ) ; ::_thesis: A * (B - C) = (A * B) - (A * C)
A4: ( width (- C) = width C & len C = len (- C) ) by MATRIX_3:def_2;
thus A * (B - C) = A * (B + (- C)) by MATRIX_4:def_1
.= (A * B) + (A * (- C)) by A1, A2, A3, A4, MATRIX_4:62
.= (A * B) + (- (A * C)) by A1, A3, Th19
.= (A * B) - (A * C) by MATRIX_4:def_1 ; ::_thesis: verum
end;
theorem :: MATRIXR2:21
for A, B, C being Matrix of REAL st len A = len B & width A = width B & width C = len A & len C > 0 & len A > 0 holds
C * (A - B) = (C * A) - (C * B) by Th20;
theorem Th22: :: MATRIXR2:22
for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = len A & width C = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) - (B * (i,j)) ) holds
C = A - B
proof
let A, B, C be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len C = len A & width C = width A & ( for i, j being Element of NAT st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) - (B * (i,j)) ) implies C = A - B )
assume that
A1: ( len A = len B & width A = width B ) and
A2: ( len C = len A & width C = width A ) and
A3: for i, j being Element of NAT st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) - (B * (i,j)) ; ::_thesis: C = A - B
A4: Indices B = Indices A by A1, MATRIX_4:55;
for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) + ((- B) * (i,j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies C * (i,j) = (A * (i,j)) + ((- B) * (i,j)) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12;
assume A5: [i,j] in Indices A ; ::_thesis: C * (i,j) = (A * (i,j)) + ((- B) * (i,j))
hence C * (i,j) = (A * (i0,j0)) - (B * (i0,j0)) by A3
.= (A * (i0,j0)) + (- (B * (i0,j0)))
.= (A * (i,j)) + ((- B) * (i,j)) by A4, A5, Th10 ;
::_thesis: verum
end;
then C = A + (- B) by A2, MATRIXR1:26;
hence C = A - B by MATRIX_4:def_1; ::_thesis: verum
end;
theorem Th23: :: MATRIXR2:23
for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 implies LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) )
A1: ( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 ) by MATRIXR1:def_10;
A2: Seg (width (LineVec2Mx x1)) = Seg (len x1) by MATRIXR1:def_10
.= dom x1 by FINSEQ_1:def_3 ;
A3: dom (LineVec2Mx x1) = Seg (len (LineVec2Mx x1)) by FINSEQ_1:def_3
.= Seg 1 by MATRIXR1:def_10 ;
assume A4: len x1 = len x2 ; ::_thesis: LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)
then A5: dom x1 = dom x2 by FINSEQ_3:29;
A6: ( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 ) by MATRIXR1:def_10;
then A7: Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1) by A4, A1, MATRIX_4:55;
A8: len (x1 - x2) = len x1 by A4, RVSUM_1:116;
then A9: dom (x1 - x2) = dom x1 by FINSEQ_3:29;
A10: ( width (LineVec2Mx (x1 - x2)) = len (x1 - x2) & len (LineVec2Mx (x1 - x2)) = 1 ) by MATRIXR1:def_10;
then A11: Indices (LineVec2Mx (x1 - x2)) = Indices (LineVec2Mx x1) by A4, A1, MATRIX_4:55, RVSUM_1:116;
for i, j being Element of NAT st [i,j] in Indices (LineVec2Mx x1) holds
(LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j))
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j)) )
assume A12: [i,j] in Indices (LineVec2Mx x1) ; ::_thesis: (LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j))
then consider q1 being FinSequence of REAL such that
q1 = (LineVec2Mx x1) . i and
A13: (LineVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5;
i in Seg 1 by A3, A12, ZFMISC_1:87;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A14: i = 1 by XXREAL_0:1;
A15: j in dom x1 by A2, A12, ZFMISC_1:87;
then A16: q1 . j = x1 . j by A14, A13, MATRIXR1:def_10;
consider p being FinSequence of REAL such that
p = (LineVec2Mx (x1 - x2)) . i and
A17: (LineVec2Mx (x1 - x2)) * (i,j) = p . j by A11, A12, MATRIX_1:def_5;
consider q2 being FinSequence of REAL such that
q2 = (LineVec2Mx x2) . i and
A18: (LineVec2Mx x2) * (i,j) = q2 . j by A7, A12, MATRIX_1:def_5;
A19: q2 . j = x2 . j by A5, A15, A14, A18, MATRIXR1:def_10;
p . j = (x1 - x2) . j by A9, A15, A14, A17, MATRIXR1:def_10;
hence (LineVec2Mx (x1 - x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) - ((LineVec2Mx x2) * (i,j)) by A4, A17, A13, A16, A18, A19, Lm1; ::_thesis: verum
end;
hence LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2) by A4, A8, A10, A1, A6, Th22; ::_thesis: verum
end;
theorem Th24: :: MATRIXR2:24
for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds
ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2)
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: ( len x1 = len x2 & len x1 > 0 implies ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2) )
assume that
A1: len x1 = len x2 and
A2: len x1 > 0 ; ::_thesis: ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2)
A3: width (ColVec2Mx x1) = 1 by A2, MATRIXR1:def_9;
A4: Seg (width (ColVec2Mx x1)) = Seg 1 by A2, MATRIXR1:def_9;
A5: dom x1 = dom x2 by A1, FINSEQ_3:29;
A6: len (x1 - x2) = len x1 by A1, RVSUM_1:116;
then A7: dom (x1 - x2) = dom x1 by FINSEQ_3:29;
A8: len (ColVec2Mx x1) = len x1 by A2, MATRIXR1:def_9;
then A9: dom (ColVec2Mx x1) = dom x1 by FINSEQ_3:29;
A10: ( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 ) by A1, A2, MATRIXR1:def_9;
then A11: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A8, A3, MATRIX_4:55;
A12: ( len (ColVec2Mx (x1 - x2)) = len (x1 - x2) & width (ColVec2Mx (x1 - x2)) = 1 ) by A2, A6, MATRIXR1:def_9;
then A13: Indices (ColVec2Mx (x1 - x2)) = Indices (ColVec2Mx x1) by A1, A8, A3, MATRIX_4:55, RVSUM_1:116;
for i, j being Element of NAT st [i,j] in Indices (ColVec2Mx x1) holds
(ColVec2Mx (x1 - x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) - ((ColVec2Mx x2) * (i,j))
proof
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 - x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) - ((ColVec2Mx x2) * (i,j)) )
assume A14: [i,j] in Indices (ColVec2Mx x1) ; ::_thesis: (ColVec2Mx (x1 - x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) - ((ColVec2Mx x2) * (i,j))
then consider q1 being FinSequence of REAL such that
A15: q1 = (ColVec2Mx x1) . i and
A16: (ColVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5;
j in Seg 1 by A4, A14, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A17: j = 1 by XXREAL_0:1;
A18: i in dom x1 by A9, A14, ZFMISC_1:87;
then (ColVec2Mx x1) . i = <*(x1 . i)*> by A2, MATRIXR1:def_9;
then A19: q1 . j = x1 . i by A17, A15, FINSEQ_1:40;
consider p being FinSequence of REAL such that
A20: p = (ColVec2Mx (x1 - x2)) . i and
A21: (ColVec2Mx (x1 - x2)) * (i,j) = p . j by A13, A14, MATRIX_1:def_5;
consider q2 being FinSequence of REAL such that
A22: q2 = (ColVec2Mx x2) . i and
A23: (ColVec2Mx x2) * (i,j) = q2 . j by A11, A14, MATRIX_1:def_5;
(ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A2, A5, A18, MATRIXR1:def_9;
then A24: q2 . j = x2 . i by A17, A22, FINSEQ_1:40;
(ColVec2Mx (x1 - x2)) . i = <*((x1 - x2) . i)*> by A2, A6, A7, A18, MATRIXR1:def_9;
then p . j = (x1 - x2) . i by A17, A20, FINSEQ_1:40;
hence (ColVec2Mx (x1 - x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) - ((ColVec2Mx x2) * (i,j)) by A1, A21, A16, A19, A23, A24, Lm1; ::_thesis: verum
end;
hence ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2) by A1, A6, A8, A12, A3, A10, Th22; ::_thesis: verum
end;
theorem Th25: :: MATRIXR2:25
for A, B being Matrix of REAL st len A = len B & width A = width B holds
for i being Nat st 1 <= i & i <= len A holds
Line ((A - B),i) = (Line (A,i)) - (Line (B,i))
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B implies for i being Nat st 1 <= i & i <= len A holds
Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) )
assume that
A1: len A = len B and
A2: width A = width B ; ::_thesis: for i being Nat st 1 <= i & i <= len A holds
Line ((A - B),i) = (Line (A,i)) - (Line (B,i))
A3: width (A - B) = width A by A1, A2, Th6;
let i be Nat; ::_thesis: ( 1 <= i & i <= len A implies Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) )
A4: len (Line (A,i)) = width A by MATRIX_1:def_7;
A5: len (Line (B,i)) = width B by MATRIX_1:def_7;
assume ( 1 <= i & i <= len A ) ; ::_thesis: Line ((A - B),i) = (Line (A,i)) - (Line (B,i))
then A6: i in dom A by FINSEQ_3:25;
A7: for j being Nat st j in Seg (width (A - B)) holds
((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j)
proof
reconsider i2 = i as Element of NAT by ORDINAL1:def_12;
let j be Nat; ::_thesis: ( j in Seg (width (A - B)) implies ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) )
reconsider j2 = j as Element of NAT by ORDINAL1:def_12;
A8: ((Line (A,i2)) - (Line (B,i2))) . j = ((Line (A,i2)) . j2) - ((Line (B,i2)) . j2) by A2, A4, A5, Lm1;
assume A9: j in Seg (width (A - B)) ; ::_thesis: ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j)
then [i,j] in Indices A by A6, A3, ZFMISC_1:87;
then A10: (A - B) * (i2,j2) = (A * (i2,j2)) - (B * (i2,j2)) by A1, A2, Th6;
A11: j in Seg (width A) by A1, A2, A9, Th6;
then (Line (A,i)) . j = A * (i,j) by MATRIX_1:def_7;
hence ((Line (A,i)) - (Line (B,i))) . j = (A - B) * (i,j) by A2, A11, A10, A8, MATRIX_1:def_7; ::_thesis: verum
end;
len ((Line (A,i)) - (Line (B,i))) = len (Line (A,i)) by A2, A4, A5, RVSUM_1:116;
hence Line ((A - B),i) = (Line (A,i)) - (Line (B,i)) by A4, A3, A7, MATRIX_1:def_7; ::_thesis: verum
end;
theorem Th26: :: MATRIXR2:26
for A, B being Matrix of REAL st len A = len B & width A = width B holds
for i being Nat st 1 <= i & i <= width A holds
Col ((A - B),i) = (Col (A,i)) - (Col (B,i))
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B implies for i being Nat st 1 <= i & i <= width A holds
Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) )
assume that
A1: len A = len B and
A2: width A = width B ; ::_thesis: for i being Nat st 1 <= i & i <= width A holds
Col ((A - B),i) = (Col (A,i)) - (Col (B,i))
A3: len (A - B) = len A by A1, A2, Th6;
let i be Nat; ::_thesis: ( 1 <= i & i <= width A implies Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) )
A4: len (Col (A,i)) = len A by MATRIX_1:def_8;
assume ( 1 <= i & i <= width A ) ; ::_thesis: Col ((A - B),i) = (Col (A,i)) - (Col (B,i))
then A5: i in Seg (width A) by FINSEQ_1:1;
A6: len (Col (B,i)) = len B by MATRIX_1:def_8;
A7: dom A = dom B by A1, FINSEQ_3:29;
A8: for j being Nat st j in dom (A - B) holds
((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i)
proof
let j be Nat; ::_thesis: ( j in dom (A - B) implies ((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i) )
assume j in dom (A - B) ; ::_thesis: ((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i)
then j in Seg (len (A - B)) by FINSEQ_1:def_3;
then A9: j in dom A by A3, FINSEQ_1:def_3;
then A10: [j,i] in Indices A by A5, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
( (Col (A,i)) . j = A * (j,i) & (Col (B,i)) . j = B * (j,i) ) by A7, A9, MATRIX_1:def_8;
then ((Col (A,i)) . j) - ((Col (B,i)) . j) = (A - B) * (j,i) by A1, A2, A5, A10, Th6;
hence ((Col (A,i)) - (Col (B,i))) . j = (A - B) * (j,i) by A1, A4, A6, Lm1; ::_thesis: verum
end;
len ((Col (A,i)) - (Col (B,i))) = len (Col (A,i)) by A1, A4, A6, RVSUM_1:116;
hence Col ((A - B),i) = (Col (A,i)) - (Col (B,i)) by A4, A3, A8, MATRIX_1:def_8; ::_thesis: verum
end;
theorem :: MATRIXR2:27
for n, k, m, l being Element of NAT
for A being Matrix of n,k, REAL
for B being Matrix of k,m, REAL
for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
proof
let n, k, m, l be Element of NAT ; ::_thesis: for A being Matrix of n,k, REAL
for B being Matrix of k,m, REAL
for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
let A be Matrix of n,k, REAL ; ::_thesis: for B being Matrix of k,m, REAL
for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
let B be Matrix of k,m, REAL ; ::_thesis: for C being Matrix of m,l, REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)
let C be Matrix of m,l, REAL ; ::_thesis: ( n > 0 & k > 0 & m > 0 implies (A * B) * C = A * (B * C) )
assume that
A1: n > 0 and
A2: k > 0 and
A3: m > 0 ; ::_thesis: (A * B) * C = A * (B * C)
A4: ( width B = m & len C = m ) by A2, A3, MATRIX_1:23;
( width A = k & len B = k ) by A1, A2, MATRIX_1:23;
hence (A * B) * C = A * (B * C) by A4, MATRIX_3:33; ::_thesis: verum
end;
theorem Th28: :: MATRIXR2:28
for n being Element of NAT
for A, B, C being Matrix of n, REAL holds (A * B) * C = A * (B * C)
proof
let n be Element of NAT ; ::_thesis: for A, B, C being Matrix of n, REAL holds (A * B) * C = A * (B * C)
let A, B, C be Matrix of n, REAL ; ::_thesis: (A * B) * C = A * (B * C)
A1: ( width B = n & len C = n ) by MATRIX_1:24;
( width A = n & len B = n ) by MATRIX_1:24;
hence (A * B) * C = A * (B * C) by A1, MATRIX_3:33; ::_thesis: verum
end;
theorem Th29: :: MATRIXR2:29
for D being non empty set
for n being Element of NAT
for A being Matrix of n,D holds (A @) @ = A
proof
let D be non empty set ; ::_thesis: for n being Element of NAT
for A being Matrix of n,D holds (A @) @ = A
let n be Element of NAT ; ::_thesis: for A being Matrix of n,D holds (A @) @ = A
let A be Matrix of n,D; ::_thesis: (A @) @ = A
reconsider N = A @ as Matrix of n,D ;
A1: ( len A = n & width A = n ) by MATRIX_1:24;
A2: Indices (N @) = [:(Seg n),(Seg n):] by MATRIX_1:24
.= Indices A by MATRIX_1:24 ;
A3: for i, j being Nat st [i,j] in Indices (N @) holds
(N @) * (i,j) = A * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (N @) implies (N @) * (i,j) = A * (i,j) )
assume A4: [i,j] in Indices (N @) ; ::_thesis: (N @) * (i,j) = A * (i,j)
then [j,i] in Indices N by MATRIX_1:def_6;
then (N @) * (i,j) = N * (j,i) by MATRIX_1:def_6;
hence (N @) * (i,j) = A * (i,j) by A2, A4, MATRIX_1:def_6; ::_thesis: verum
end;
( len (N @) = n & width (N @) = n ) by MATRIX_1:24;
hence (A @) @ = A by A1, A3, MATRIX_1:21; ::_thesis: verum
end;
theorem Th30: :: MATRIXR2:30
for n being Element of NAT
for A, B being Matrix of n, REAL holds (A * B) @ = (B @) * (A @)
proof
let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL holds (A * B) @ = (B @) * (A @)
let A, B be Matrix of n, REAL ; ::_thesis: (A * B) @ = (B @) * (A @)
A1: len A = n by MATRIX_1:24;
A2: ( width A = n & len B = n ) by MATRIX_1:24;
A3: len (A * B) = n by MATRIX_1:24;
A4: width B = n by MATRIX_1:24;
A5: len (B @) = n by MATRIX_1:24;
then A6: len ((B @) * (A @)) = len (B @) by MATRIX_1:24;
A7: width (B @) = n by MATRIX_1:24
.= len (A @) by MATRIX_1:24 ;
A8: width (A * B) = n by MATRIX_1:24;
A9: width (A @) = n by MATRIX_1:24;
then A10: width ((B @) * (A @)) = width (A @) by MATRIX_1:24;
A11: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((A_*_B)_@)_holds_
((B_@)_*_(A_@))_*_(i,j)_=_((A_*_B)_@)_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((A * B) @) implies ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j) )
A12: Indices ((A * B) @) = [:(Seg n),(Seg n):] by MATRIX_1:24;
assume A13: [i,j] in Indices ((A * B) @) ; ::_thesis: ((B @) * (A @)) * (i,j) = ((A * B) @) * (i,j)
then j in Seg (len (A * B)) by A3, A12, ZFMISC_1:87;
then A14: j in dom (A * B) by FINSEQ_1:def_3;
i in Seg (width (A * B)) by A8, A13, A12, ZFMISC_1:87;
then A15: [j,i] in Indices (A * B) by A14, ZFMISC_1:87;
Seg (width (A @)) = dom A by A1, A9, FINSEQ_1:def_3;
then j in dom A by A9, A13, A12, ZFMISC_1:87;
then A16: Col ((A @),j) = Line (A,j) by MATRIX_2:14;
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12;
A17: Seg (width B) = dom (B @) by A4, A5, FINSEQ_1:def_3;
A18: Indices ((B @) * (A @)) = [:(Seg n),(Seg n):] by MATRIX_1:24;
then [i,j] in [:(dom (B @)),(Seg (width (A @))):] by A6, A10, A13, A12, FINSEQ_3:29;
then i in Seg (width B) by A17, ZFMISC_1:87;
then Line ((B @),i) = Col (B,i) by MATRIX_2:15;
hence ((B @) * (A @)) * (i,j) = (Col (B,i0)) "*" (Line (A,j0)) by A7, A13, A12, A18, A16, MATRPROB:39
.= (A * B) * (j0,i0) by A2, A15, MATRPROB:39
.= ((A * B) @) * (i,j) by A15, MATRIX_1:def_6 ;
::_thesis: verum
end;
A19: ( len ((B @) * (A @)) = n & width ((B @) * (A @)) = n ) by MATRIX_1:24;
( len ((A * B) @) = n & width ((A * B) @) = n ) by MATRIX_1:24;
hence (A * B) @ = (B @) * (A @) by A19, A11, MATRIX_1:21; ::_thesis: verum
end;
theorem Th31: :: MATRIXR2:31
for n, m being Element of NAT
for A being Matrix of REAL st len A = n & width A = m holds
(- A) + A = 0_Rmatrix (n,m)
proof
let n, m be Element of NAT ; ::_thesis: for A being Matrix of REAL st len A = n & width A = m holds
(- A) + A = 0_Rmatrix (n,m)
let A be Matrix of REAL; ::_thesis: ( len A = n & width A = m implies (- A) + A = 0_Rmatrix (n,m) )
assume A1: ( len A = n & width A = m ) ; ::_thesis: (- A) + A = 0_Rmatrix (n,m)
( len (- (MXR2MXF A)) = len A & width (- (MXR2MXF A)) = width A ) by MATRIX_3:def_2;
hence (- A) + A = MXF2MXR ((MXR2MXF A) + (- (MXR2MXF A))) by MATRIX_3:2
.= 0_Rmatrix (n,m) by A1, MATRIX_4:2 ;
::_thesis: verum
end;
begin
definition
let n be Element of NAT ;
let A be Matrix of n, REAL ;
:: original: MXR2MXF
redefine func MXR2MXF A -> Matrix of n,F_Real;
coherence
MXR2MXF A is Matrix of n,F_Real ;
end;
definition
let n be Element of NAT ;
let A be Matrix of n, REAL ;
func Det A -> Real equals :: MATRIXR2:def 1
Det (MXR2MXF A);
coherence
Det (MXR2MXF A) is Real ;
end;
:: deftheorem defines Det MATRIXR2:def_1_:_
for n being Element of NAT
for A being Matrix of n, REAL holds Det A = Det (MXR2MXF A);
theorem :: MATRIXR2:32
for A being Matrix of 2, REAL holds Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1)))
proof
let A be Matrix of 2, REAL ; ::_thesis: Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1)))
reconsider N = MXR2MXF A as Matrix of 2,F_Real ;
Det A = ((N * (1,1)) * (N * (2,2))) - ((N * (1,2)) * (N * (2,1))) by MATRIX_7:12;
hence Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1))) ; ::_thesis: verum
end;
theorem Th33: :: MATRIXR2:33
for n being Element of NAT
for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds
<*s1,s2,s3*> is tabular
proof
let n be Element of NAT ; ::_thesis: for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds
<*s1,s2,s3*> is tabular
let s1, s2, s3 be FinSequence; ::_thesis: ( len s1 = n & len s2 = n & len s3 = n implies <*s1,s2,s3*> is tabular )
assume A1: ( len s1 = n & len s2 = n & len s3 = n ) ; ::_thesis: <*s1,s2,s3*> is tabular
now__::_thesis:_ex_n_being_Element_of_NAT_st_
for_x_being_set_st_x_in_rng_<*s1,s2,s3*>_holds_
ex_r_being_FinSequence_st_
(_x_=_r_&_len_r_=_n_)
take n = n; ::_thesis: for x being set st x in rng <*s1,s2,s3*> holds
ex r being FinSequence st
( x = r & len r = n )
let x be set ; ::_thesis: ( x in rng <*s1,s2,s3*> implies ex r being FinSequence st
( x = r & len r = n ) )
assume x in rng <*s1,s2,s3*> ; ::_thesis: ex r being FinSequence st
( x = r & len r = n )
then A2: x in {s1,s2,s3} by FINSEQ_2:128;
then reconsider r = x as FinSequence by ENUMSET1:def_1;
take r = r; ::_thesis: ( x = r & len r = n )
thus ( x = r & len r = n ) by A1, A2, ENUMSET1:def_1; ::_thesis: verum
end;
hence <*s1,s2,s3*> is tabular by MATRIX_1:def_1; ::_thesis: verum
end;
theorem Th34: :: MATRIXR2:34
for D being non empty set
for n being Element of NAT
for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds
<*p1,p2,p3*> is Matrix of 3,n,D
proof
let D be non empty set ; ::_thesis: for n being Element of NAT
for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds
<*p1,p2,p3*> is Matrix of 3,n,D
let n be Element of NAT ; ::_thesis: for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds
<*p1,p2,p3*> is Matrix of 3,n,D
let p1, p2, p3 be FinSequence of D; ::_thesis: ( len p1 = n & len p2 = n & len p3 = n implies <*p1,p2,p3*> is Matrix of 3,n,D )
reconsider q1 = p1, q2 = p2, q3 = p3 as Element of D * by FINSEQ_1:def_11;
reconsider M = <*q1,q2,q3*> as FinSequence of D * ;
assume A1: ( len p1 = n & len p2 = n & len p3 = n ) ; ::_thesis: <*p1,p2,p3*> is Matrix of 3,n,D
then reconsider M = M as Matrix of D by Th33;
M is Matrix of 3,n,D
proof
thus len M = 3 by FINSEQ_1:45; :: according to MATRIX_1:def_2 ::_thesis: for b1 being FinSequence of D holds
( not b1 in rng M or len b1 = n )
let r be FinSequence of D; ::_thesis: ( not r in rng M or len r = n )
assume r in rng M ; ::_thesis: len r = n
then r in {p1,p2,p3} by FINSEQ_2:128;
hence len r = n by A1, ENUMSET1:def_1; ::_thesis: verum
end;
hence <*p1,p2,p3*> is Matrix of 3,n,D ; ::_thesis: verum
end;
theorem Th35: :: MATRIXR2:35
for D being non empty set
for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D
proof
let D be non empty set ; ::_thesis: for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D
let a1, a2, a3, b1, b2, b3, c1, c2, c3 be Element of D; ::_thesis: <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D
A1: len <*c1,c2,c3*> = 3 by FINSEQ_1:45;
( len <*a1,a2,a3*> = 3 & len <*b1,b2,b3*> = 3 ) by FINSEQ_1:45;
hence <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D by A1, Th34; ::_thesis: verum
end;
theorem Th36: :: MATRIXR2:36
for D being non empty set
for n being Element of NAT
for A being Matrix of n,D
for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n
proof
let D be non empty set ; ::_thesis: for n being Element of NAT
for A being Matrix of n,D
for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n
let n be Element of NAT ; ::_thesis: for A being Matrix of n,D
for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n
let A be Matrix of n,D; ::_thesis: for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n
let p be FinSequence of D; ::_thesis: for i being Nat st p = A . i & i in Seg n holds
len p = n
let i be Nat; ::_thesis: ( p = A . i & i in Seg n implies len p = n )
assume that
A1: p = A . i and
A2: i in Seg n ; ::_thesis: len p = n
consider n2 being Nat such that
A3: for x being set st x in rng A holds
ex s being FinSequence of D st
( s = x & len s = n2 ) by MATRIX_1:9;
len A = n by MATRIX_1:24;
then A4: i in dom A by A2, FINSEQ_1:def_3;
then A . i in rng A by FUNCT_1:def_3;
then consider s being FinSequence of D such that
A5: s = A . i and
len s = n2 by A3;
s in rng A by A4, A5, FUNCT_1:def_3;
hence len p = n by A1, A5, MATRIX_1:def_2; ::_thesis: verum
end;
theorem Th37: :: MATRIXR2:37
for D being non empty set
for A being Matrix of 3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*>
proof
let D be non empty set ; ::_thesis: for A being Matrix of 3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*>
let A be Matrix of 3,D; ::_thesis: A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*>
reconsider B = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> as Matrix of 3,D by Th35;
A1: ( len A = 3 & width A = 3 ) by MATRIX_1:24;
A2: for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
A3: Indices B = [:(Seg 3),(Seg 3):] by MATRIX_1:24;
A4: Indices A = [:(Seg 3),(Seg 3):] by MATRIX_1:24;
assume A5: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j)
then A6: i in Seg 3 by A4, ZFMISC_1:87;
2 in Seg 3 ;
then A7: [i,2] in Indices A by A4, A6, ZFMISC_1:87;
1 in Seg 3 ;
then A8: [i,1] in Indices A by A4, A6, ZFMISC_1:87;
3 in Seg 3 ;
then A9: [i,3] in Indices A by A4, A6, ZFMISC_1:87;
A10: i in {1,2,3} by A5, A4, FINSEQ_3:1, ZFMISC_1:87;
now__::_thesis:_(_(_i_=_1_&_ex_p_being_FinSequence_of_D_st_
(_p_=_A_._i_&_B_*_(i,j)_=_p_._j_)_)_or_(_i_=_2_&_ex_p_being_FinSequence_of_D_st_
(_p_=_A_._i_&_B_*_(i,j)_=_p_._j_)_)_or_(_i_=_3_&_ex_p_being_FinSequence_of_D_st_
(_p_=_A_._i_&_B_*_(i,j)_=_p_._j_)_)_)
percases ( i = 1 or i = 2 or i = 3 ) by A10, ENUMSET1:def_1;
caseA11: i = 1 ; ::_thesis: ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j )
reconsider p0 = <*(A * (1,1)),(A * (1,2)),(A * (1,3))*> as FinSequence of D ;
A12: len p0 = 3 by FINSEQ_1:45;
A13: ex p23 being FinSequence of D st
( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_1:def_5;
consider p2 being FinSequence of D such that
A14: p2 = A . i and
A15: A * (i,1) = p2 . 1 by A8, MATRIX_1:def_5;
A16: ex p22 being FinSequence of D st
( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_1:def_5;
A17: for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k )
assume A18: ( 1 <= k & k <= len p0 ) ; ::_thesis: p0 . k = p2 . k
k in NAT by ORDINAL1:def_12;
then A19: k in Seg 3 by A12, A18;
percases ( k = 1 or k = 2 or k = 3 ) by A19, ENUMSET1:def_1, FINSEQ_3:1;
suppose k = 1 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A15, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A14, A16, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 3 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A11, A14, A13, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
ex p being FinSequence of D st
( p = B . i & B * (i,j) = p . j ) by A5, A3, A4, MATRIX_1:def_5;
then A20: B * (i,j) = p0 . j by A11, FINSEQ_1:45;
len p2 = 3 by A6, A14, Th36;
hence ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j ) by A12, A14, A17, A20, FINSEQ_1:14; ::_thesis: verum
end;
caseA21: i = 2 ; ::_thesis: ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j )
reconsider p0 = <*(A * (2,1)),(A * (2,2)),(A * (2,3))*> as FinSequence of D ;
A22: len p0 = 3 by FINSEQ_1:45;
A23: ex p23 being FinSequence of D st
( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_1:def_5;
consider p2 being FinSequence of D such that
A24: p2 = A . i and
A25: A * (i,1) = p2 . 1 by A8, MATRIX_1:def_5;
A26: ex p22 being FinSequence of D st
( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_1:def_5;
A27: for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k )
assume A28: ( 1 <= k & k <= len p0 ) ; ::_thesis: p0 . k = p2 . k
k in NAT by ORDINAL1:def_12;
then A29: k in {1,2,3} by A22, A28, FINSEQ_3:1;
percases ( k = 1 or k = 2 or k = 3 ) by A29, ENUMSET1:def_1;
suppose k = 1 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A25, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A24, A26, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 3 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A21, A24, A23, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
ex p being FinSequence of D st
( p = B . i & B * (i,j) = p . j ) by A5, A3, A4, MATRIX_1:def_5;
then A30: B * (i,j) = p0 . j by A21, FINSEQ_1:45;
len p2 = 3 by A6, A24, Th36;
hence ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j ) by A22, A24, A27, A30, FINSEQ_1:14; ::_thesis: verum
end;
caseA31: i = 3 ; ::_thesis: ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j )
reconsider p0 = <*(A * (3,1)),(A * (3,2)),(A * (3,3))*> as FinSequence of D ;
A32: len p0 = 3 by FINSEQ_1:45;
A33: ex p23 being FinSequence of D st
( p23 = A . i & A * (i,3) = p23 . 3 ) by A9, MATRIX_1:def_5;
consider p2 being FinSequence of D such that
A34: p2 = A . i and
A35: A * (i,1) = p2 . 1 by A8, MATRIX_1:def_5;
A36: ex p22 being FinSequence of D st
( p22 = A . i & A * (i,2) = p22 . 2 ) by A7, MATRIX_1:def_5;
A37: for k being Nat st 1 <= k & k <= len p0 holds
p0 . k = p2 . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len p0 implies p0 . k = p2 . k )
assume A38: ( 1 <= k & k <= len p0 ) ; ::_thesis: p0 . k = p2 . k
k in NAT by ORDINAL1:def_12;
then A39: k in {1,2,3} by A32, A38, FINSEQ_3:1;
percases ( k = 1 or k = 2 or k = 3 ) by A39, ENUMSET1:def_1;
suppose k = 1 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A35, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A34, A36, FINSEQ_1:45; ::_thesis: verum
end;
suppose k = 3 ; ::_thesis: p0 . k = p2 . k
hence p0 . k = p2 . k by A31, A34, A33, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
ex p being FinSequence of D st
( p = B . i & B * (i,j) = p . j ) by A5, A3, A4, MATRIX_1:def_5;
then A40: B * (i,j) = p0 . j by A31, FINSEQ_1:45;
len p2 = 3 by A6, A34, Th36;
hence ex p being FinSequence of D st
( p = A . i & B * (i,j) = p . j ) by A32, A34, A37, A40, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
hence A * (i,j) = B * (i,j) by A5, MATRIX_1:def_5; ::_thesis: verum
end;
( len B = 3 & width B = 3 ) by MATRIX_1:24;
hence A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*> by A1, A2, MATRIX_1:21; ::_thesis: verum
end;
theorem :: MATRIXR2:38
for A being Matrix of 3, REAL holds Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2)))
proof
let A be Matrix of 3, REAL ; ::_thesis: Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2)))
reconsider N = MXR2MXF A as Matrix of 3,F_Real ;
reconsider N2 = <*<*(N * (1,1)),(N * (1,2)),(N * (1,3))*>,<*(N * (2,1)),(N * (2,2)),(N * (2,3))*>,<*(N * (3,1)),(N * (3,2)),(N * (3,3))*>*> as Matrix of 3,F_Real by Th35;
Det A = Det N2 by Th37
.= (((((((N * (1,1)) * (N * (2,2))) * (N * (3,3))) - (((N * (1,3)) * (N * (2,2))) * (N * (3,1)))) - (((N * (1,1)) * (N * (2,3))) * (N * (3,2)))) + (((N * (1,2)) * (N * (2,3))) * (N * (3,1)))) - (((N * (1,2)) * (N * (2,1))) * (N * (3,3)))) + (((N * (1,3)) * (N * (2,1))) * (N * (3,2))) by MATRIX_9:46 ;
hence Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2))) ; ::_thesis: verum
end;
theorem :: MATRIXR2:39
for f being Permutation of (Seg 0) holds f = <*> NAT ;
Lm4: idseq 0 is Permutation of (Seg 0)
by FINSEQ_2:55;
theorem Th40: :: MATRIXR2:40
Permutations 0 = {(<*> NAT)}
proof
now__::_thesis:_for_p_being_set_st_p_in_Permutations_0_holds_
p_in_{(<*>_NAT)}
let p be set ; ::_thesis: ( p in Permutations 0 implies p in {(<*> NAT)} )
assume p in Permutations 0 ; ::_thesis: p in {(<*> NAT)}
then reconsider q = p as Permutation of (Seg 0) by MATRIX_2:def_9;
q = <*> NAT ;
hence p in {(<*> NAT)} by TARSKI:def_1; ::_thesis: verum
end;
then A1: Permutations 0 c= {(<*> NAT)} by TARSKI:def_3;
{(<*> NAT)} c= Permutations 0
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(<*> NAT)} or x in Permutations 0 )
assume x in {(<*> NAT)} ; ::_thesis: x in Permutations 0
then x is Permutation of (Seg 0) by Lm4, TARSKI:def_1;
hence x in Permutations 0 by MATRIX_2:def_9; ::_thesis: verum
end;
hence Permutations 0 = {(<*> NAT)} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th41: :: MATRIXR2:41
for K being Field
for A being Matrix of 0 ,K holds Det A = 1. K
proof
let K be Field; ::_thesis: for A being Matrix of 0 ,K holds Det A = 1. K
reconsider kk = idseq 0 as Element of Permutations 0 by Th40, TARSKI:def_1;
let A be Matrix of 0 ,K; ::_thesis: Det A = 1. K
A1: (Path_product A) . (idseq 0) = 1. K
proof
reconsider p = idseq 0 as Element of Permutations 0 by Lm4, MATRIX_2:def_9;
A2: - ((1_ K),p) = 1_ K
proof
reconsider q = id (Seg 0) as Element of Permutations 0 by Lm4, MATRIX_2:def_9;
len (Permutations 0) = 0 by MATRIX_2:18;
then q is even by MATRIX_2:25;
hence - ((1_ K),p) = 1_ K by MATRIX_2:def_13; ::_thesis: verum
end;
1_ K is_a_unity_wrt the multF of K by GROUP_1:21;
then ( len (Path_matrix (p,A)) = 0 & the multF of K is having_a_unity ) by MATRIX_3:def_7, SETWISEO:def_2;
then the multF of K $$ (Path_matrix (p,A)) = the_unity_wrt the multF of K by FINSOP_1:def_1
.= 1_ K by GROUP_1:22 ;
hence (Path_product A) . (idseq 0) = 1. K by A2, MATRIX_3:def_8; ::_thesis: verum
end;
A3: FinOmega (Permutations 0) = Permutations 0 by Th40, MATRIX_2:def_14
.= {.kk.} by Th40 ;
Det A = the addF of K $$ ((FinOmega (Permutations 0)),(Path_product A)) by MATRIX_3:def_9
.= 1. K by A1, A3, SETWISEO:17 ;
hence Det A = 1. K ; ::_thesis: verum
end;
theorem :: MATRIXR2:42
for A being Matrix of 0 , REAL holds Det A = 1
proof
let A be Matrix of 0 , REAL ; ::_thesis: Det A = 1
thus Det A = 1. F_Real by Th41
.= 1 ; ::_thesis: verum
end;
theorem Th43: :: MATRIXR2:43
for K being Field
for n being Nat
for A being Matrix of n,K holds Det A = Det (A @)
proof
let K be Field; ::_thesis: for n being Nat
for A being Matrix of n,K holds Det A = Det (A @)
let n be Nat; ::_thesis: for A being Matrix of n,K holds Det A = Det (A @)
let A be Matrix of n,K; ::_thesis: Det A = Det (A @)
( n = 0 or ( n >= 1 & n is Element of NAT ) ) by NAT_1:14, ORDINAL1:def_12;
then ( ( Det A = 1_ K & Det (A @) = 1_ K ) or Det A = Det (A @) ) by Th41, MATRIX_7:37;
hence Det A = Det (A @) ; ::_thesis: verum
end;
theorem :: MATRIXR2:44
for n being Element of NAT
for A being Matrix of n, REAL holds Det A = Det (A @)
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL holds Det A = Det (A @)
let A be Matrix of n, REAL ; ::_thesis: Det A = Det (A @)
reconsider N1 = MXR2MXF A, N2 = MXR2MXF (A @) as Matrix of n,F_Real ;
reconsider N3 = MXF2MXR (N1 @) as Matrix of n, REAL ;
reconsider N4 = MXR2MXF N3 as Matrix of n,F_Real ;
thus Det A = Det (A @) by Th43; ::_thesis: verum
end;
theorem Th45: :: MATRIXR2:45
for n being Element of NAT
for K being Field
for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)
proof
let n be Element of NAT ; ::_thesis: for K being Field
for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)
let K be Field; ::_thesis: for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)
let A, B be Matrix of n,K; ::_thesis: Det (A * B) = (Det A) * (Det B)
percases ( n > 0 or n <= 0 ) ;
suppose n > 0 ; ::_thesis: Det (A * B) = (Det A) * (Det B)
hence Det (A * B) = (Det A) * (Det B) by MATRIX11:62; ::_thesis: verum
end;
suppose n <= 0 ; ::_thesis: Det (A * B) = (Det A) * (Det B)
then A1: n = 0 ;
hence Det (A * B) = 1. K by Th41
.= (1. K) * (1. K) by VECTSP_1:def_6
.= (Det A) * (1. K) by A1, Th41
.= (Det A) * (Det B) by A1, Th41 ;
::_thesis: verum
end;
end;
end;
theorem Th46: :: MATRIXR2:46
for n being Element of NAT
for A, B being Matrix of n, REAL holds Det (A * B) = (Det A) * (Det B)
proof
let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL holds Det (A * B) = (Det A) * (Det B)
set K = F_Real ;
let A, B be Matrix of n, REAL ; ::_thesis: Det (A * B) = (Det A) * (Det B)
reconsider Na = MXR2MXF A, Nb = MXR2MXF B as Matrix of n,F_Real ;
Det (A * B) = (Det Na) * (Det Nb) by Th45
.= (Det A) * (Det B) ;
hence Det (A * B) = (Det A) * (Det B) ; ::_thesis: verum
end;
begin
theorem :: MATRIXR2:47
for x, y being FinSequence of REAL
for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds
(x - y) * A = (x * A) - (y * A)
proof
let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds
(x - y) * A = (x * A) - (y * A)
let A be Matrix of REAL; ::_thesis: ( len x = len A & len y = len x & len x > 0 implies (x - y) * A = (x * A) - (y * A) )
assume that
A1: len x = len A and
A2: len y = len x and
A3: len x > 0 ; ::_thesis: (x - y) * A = (x * A) - (y * A)
A4: width (LineVec2Mx y) = len y by MATRIXR1:def_10;
A5: width (LineVec2Mx x) = len x by MATRIXR1:def_10;
then A6: width ((LineVec2Mx x) * A) = width A by A1, MATRIX_3:def_4
.= width ((LineVec2Mx y) * A) by A1, A2, A4, MATRIX_3:def_4 ;
A7: len (LineVec2Mx y) = 1 by MATRIXR1:def_10;
A8: len (LineVec2Mx x) = 1 by MATRIXR1:def_10;
then A9: 1 <= len ((LineVec2Mx x) * A) by A1, A5, MATRIX_3:def_4;
A10: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A5, MATRIX_3:def_4
.= len (LineVec2Mx y) by A7, MATRIXR1:def_10
.= len ((LineVec2Mx y) * A) by A1, A2, A4, MATRIX_3:def_4 ;
thus (x - y) * A = Line ((((LineVec2Mx x) - (LineVec2Mx y)) * A),1) by A2, Th23
.= Line ((((LineVec2Mx x) * A) - ((LineVec2Mx y) * A)),1) by A1, A2, A3, A5, A4, A8, A7, Th16
.= (x * A) - (y * A) by A6, A10, A9, Th25 ; ::_thesis: verum
end;
theorem :: MATRIXR2:48
for x, y being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds
A * (x - y) = (A * x) - (A * y)
proof
let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds
A * (x - y) = (A * x) - (A * y)
let A be Matrix of REAL; ::_thesis: ( len x = width A & len y = len x & len x > 0 & len A > 0 implies A * (x - y) = (A * x) - (A * y) )
assume that
A1: len x = width A and
A2: len y = len x and
A3: len x > 0 and
A4: len A > 0 ; ::_thesis: A * (x - y) = (A * x) - (A * y)
A5: len (ColVec2Mx y) = len y by A2, A3, MATRIXR1:def_9;
A6: width (ColVec2Mx y) = 1 by A2, A3, MATRIXR1:def_9;
A7: len (ColVec2Mx x) = len x by A3, MATRIXR1:def_9;
then A8: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def_4
.= len (A * (ColVec2Mx y)) by A1, A2, A5, MATRIX_3:def_4 ;
A9: width (ColVec2Mx x) = 1 by A3, MATRIXR1:def_9;
then A10: 1 <= width (A * (ColVec2Mx x)) by A1, A7, MATRIX_3:def_4;
A11: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A7, MATRIX_3:def_4
.= width (ColVec2Mx y) by A3, A6, MATRIXR1:def_9
.= width (A * (ColVec2Mx y)) by A1, A2, A5, MATRIX_3:def_4 ;
thus A * (x - y) = Col ((A * ((ColVec2Mx x) - (ColVec2Mx y))),1) by A2, A3, Th24
.= Col (((A * (ColVec2Mx x)) - (A * (ColVec2Mx y))),1) by A1, A2, A3, A4, A7, A5, A9, A6, Th20
.= (A * x) - (A * y) by A8, A11, A10, Th26 ; ::_thesis: verum
end;
theorem :: MATRIXR2:49
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(- x) * A = - (x * A)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(- x) * A = - (x * A)
let A be Matrix of REAL; ::_thesis: ( len A = len x & len x > 0 & width A > 0 implies (- x) * A = - (x * A) )
assume that
A1: len A = len x and
A2: len x > 0 and
A3: width A > 0 ; ::_thesis: (- x) * A = - (x * A)
A4: (A @) * x = x * A by A1, A2, A3, MATRIXR1:52;
A5: width (A @) = len x by A1, A3, MATRIX_2:10;
then A6: (A @) * (- x) = (- 1) * ((A @) * x) by A2, MATRIXR1:59;
A7: len (- x) = len x by RVSUM_1:114;
len (A @) > 0 by A3, MATRIX_2:10;
then (- x) * ((A @) @) = (A @) * (- x) by A2, A5, A7, MATRIXR1:53;
hence (- x) * A = - (x * A) by A1, A2, A3, A6, A4, MATRIX_2:13; ::_thesis: verum
end;
theorem :: MATRIXR2:50
for x being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len x > 0 holds
A * (- x) = - (A * x)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = width A & len x > 0 holds
A * (- x) = - (A * x)
let A be Matrix of REAL; ::_thesis: ( len x = width A & len x > 0 implies A * (- x) = - (A * x) )
assume that
A1: len x = width A and
A2: len x > 0 ; ::_thesis: A * (- x) = - (A * x)
A3: len (ColVec2Mx x) = len x by A2, MATRIXR1:def_9;
width (ColVec2Mx x) = 1 by A2, MATRIXR1:def_9;
then A4: 1 <= width (A * (ColVec2Mx x)) by A1, A3, MATRIX_3:def_4;
thus A * (- x) = Col ((A * ((- 1) * (ColVec2Mx x))),1) by A2, MATRIXR1:47
.= Col (((- 1) * (A * (ColVec2Mx x))),1) by A1, A3, MATRIXR1:40
.= - (A * x) by A4, MATRIXR1:56 ; ::_thesis: verum
end;
theorem :: MATRIXR2:51
for x being FinSequence of REAL
for A being Matrix of REAL st len x = len A & len x > 0 holds
x * (- A) = - (x * A)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = len A & len x > 0 holds
x * (- A) = - (x * A)
let A be Matrix of REAL; ::_thesis: ( len x = len A & len x > 0 implies x * (- A) = - (x * A) )
assume that
A1: len x = len A and
A2: len x > 0 ; ::_thesis: x * (- A) = - (x * A)
A3: width A = len (x * A) by A1, MATRIXR1:62;
A4: ( len A = len (- A) & width A = width (- A) ) by MATRIX_3:def_2;
then A5: len (x * (- A)) = width A by A1, MATRIXR1:62;
(x * (- A)) + (x * A) = x * ((- A) + A) by A1, A2, A4, MATRIXR1:64
.= x * (0_Rmatrix ((len A),(width A))) by Th31
.= 0* (width A) by A1, A2, MATRIXR1:66 ;
hence x * (- A) = - (x * A) by A5, A3, Th1; ::_thesis: verum
end;
theorem :: MATRIXR2:52
for x being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds
(- A) * x = - (A * x)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds
(- A) * x = - (A * x)
let A be Matrix of REAL; ::_thesis: ( len x = width A & len A > 0 & len x > 0 implies (- A) * x = - (A * x) )
assume that
A1: len x = width A and
A2: len A > 0 and
A3: len x > 0 ; ::_thesis: (- A) * x = - (A * x)
A4: ( len (ColVec2Mx x) = len x & width (ColVec2Mx x) = 1 ) by A3, MATRIXR1:def_9;
then A5: 1 <= width (A * (ColVec2Mx x)) by A1, MATRIX_3:def_4;
thus (- A) * x = Col ((((- 1) * A) * (ColVec2Mx x)),1) by Th9
.= Col (((- 1) * (A * (ColVec2Mx x))),1) by A1, A2, A3, A4, MATRIXR1:41
.= - (A * x) by A5, MATRIXR1:56 ; ::_thesis: verum
end;
theorem :: MATRIXR2:53
for a being Real
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)
let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 implies A * (a * x) = a * (A * x) )
assume that
A1: width A = len x and
A2: len x > 0 ; ::_thesis: A * (a * x) = a * (A * x)
A3: len (ColVec2Mx x) = len x by A2, MATRIXR1:def_9;
width (ColVec2Mx x) = 1 by A2, MATRIXR1:def_9;
then A4: 1 <= width (A * (ColVec2Mx x)) by A1, A3, MATRIX_3:def_4;
thus A * (a * x) = Col ((A * (a * (ColVec2Mx x))),1) by A2, MATRIXR1:47
.= Col ((a * (A * (ColVec2Mx x))),1) by A1, A3, MATRIXR1:40
.= a * (A * x) by A4, MATRIXR1:56 ; ::_thesis: verum
end;
theorem :: MATRIXR2:54
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds
x * (A - B) = (x * A) - (x * B)
proof
let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds
x * (A - B) = (x * A) - (x * B)
let A, B be Matrix of REAL; ::_thesis: ( len x = len A & len A = len B & width A = width B & len A > 0 implies x * (A - B) = (x * A) - (x * B) )
assume that
A1: len x = len A and
A2: len A = len B and
A3: width A = width B and
A4: len A > 0 ; ::_thesis: x * (A - B) = (x * A) - (x * B)
A5: width (LineVec2Mx x) = len x by MATRIXR1:def_10;
then A6: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, MATRIX_3:def_4
.= 1 by MATRIXR1:def_10 ;
A7: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A1, A5, MATRIX_3:def_4
.= len ((LineVec2Mx x) * B) by A1, A2, A5, MATRIX_3:def_4 ;
A8: width ((LineVec2Mx x) * A) = width A by A1, A5, MATRIX_3:def_4
.= width ((LineVec2Mx x) * B) by A1, A2, A3, A5, MATRIX_3:def_4 ;
len (LineVec2Mx x) = 1 by MATRIXR1:def_10;
hence x * (A - B) = Line ((((LineVec2Mx x) * A) - ((LineVec2Mx x) * B)),1) by A1, A2, A3, A4, A5, Th20
.= (x * A) - (x * B) by A8, A7, A6, Th25 ;
::_thesis: verum
end;
theorem :: MATRIXR2:55
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds
(A - B) * x = (A * x) - (B * x)
proof
let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds
(A - B) * x = (A * x) - (B * x)
let A, B be Matrix of REAL; ::_thesis: ( len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 implies (A - B) * x = (A * x) - (B * x) )
assume that
A1: len x = width A and
A2: len A = len B and
A3: width A = width B and
A4: len x > 0 and
A5: len A > 0 ; ::_thesis: (A - B) * x = (A * x) - (B * x)
A6: len (ColVec2Mx x) = len x by A4, MATRIXR1:def_9;
then A7: len (A * (ColVec2Mx x)) = len A by A1, MATRIX_3:def_4
.= len (B * (ColVec2Mx x)) by A1, A2, A3, A6, MATRIX_3:def_4 ;
A8: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A6, MATRIX_3:def_4
.= 1 by A4, MATRIXR1:45 ;
A9: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A6, MATRIX_3:def_4
.= width (B * (ColVec2Mx x)) by A1, A3, A6, MATRIX_3:def_4 ;
thus (A - B) * x = Col (((A * (ColVec2Mx x)) - (B * (ColVec2Mx x))),1) by A1, A2, A3, A4, A5, A6, Th16
.= (A * x) - (B * x) by A7, A9, A8, Th26 ; ::_thesis: verum
end;
theorem Th56: :: MATRIXR2:56
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x holds
(LineVec2Mx x) * A = LineVec2Mx (x * A)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x holds
(LineVec2Mx x) * A = LineVec2Mx (x * A)
let A be Matrix of REAL; ::_thesis: ( len A = len x implies (LineVec2Mx x) * A = LineVec2Mx (x * A) )
A1: len (LineVec2Mx (x * A)) = 1 by MATRIXR1:def_10;
assume A2: len A = len x ; ::_thesis: (LineVec2Mx x) * A = LineVec2Mx (x * A)
then A3: width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A) by MATRIXR1:def_10;
width (LineVec2Mx (x * A)) = len (x * A) by MATRIXR1:def_10;
then A4: width (LineVec2Mx (x * A)) = width A by A2, MATRIXR1:62;
A5: len (x * A) = width A by A2, MATRIXR1:62;
then A6: width (MXR2MXF (LineVec2Mx (x * A))) = width (MXR2MXF A) by MATRIXR1:def_10;
A7: width (LineVec2Mx x) = len x by MATRIXR1:def_10;
A8: for i, j being Nat st [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) holds
(MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))
proof
len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = len (MXR2MXF (LineVec2Mx x)) by A3, MATRIX_3:def_4;
then len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = 1 by MATRIXR1:def_10;
then A9: 1 in Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))) ;
let i, j be Nat; ::_thesis: ( [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) implies (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) )
A10: width ((LineVec2Mx x) * A) = width A by A2, A7, MATRIX_3:def_4;
assume A11: [i,j] in Indices (MXR2MXF (LineVec2Mx (x * A))) ; ::_thesis: (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j))
then A12: j in Seg (width A) by A4, ZFMISC_1:87;
then j in dom (x * A) by A5, FINSEQ_1:def_3;
then A13: (Line (((LineVec2Mx x) * A),1)) . j = (LineVec2Mx (x * A)) * (1,j) by MATRIXR1:def_10;
Indices (LineVec2Mx (x * A)) = [:(Seg 1),(Seg (width A)):] by A1, A4, FINSEQ_1:def_3;
then i in Seg 1 by A11, ZFMISC_1:87;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A14: i = 1 by XXREAL_0:1;
width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) = width A by A3, MATRIX_3:def_4;
then [1,j] in [:(Seg (len ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))),(Seg (width ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)))):] by A12, A9, ZFMISC_1:87;
then A15: [1,j] in Indices ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A)) by FINSEQ_1:def_3;
width (MXR2MXF (LineVec2Mx x)) = len (MXR2MXF A) by A2, MATRIXR1:def_10;
then ((LineVec2Mx x) * A) * (1,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) by A14, A15, MATRIX_3:def_4;
hence (MXR2MXF (LineVec2Mx (x * A))) * (i,j) = (Line ((MXR2MXF (LineVec2Mx x)),i)) "*" (Col ((MXR2MXF A),j)) by A12, A14, A13, A10, MATRIX_1:def_7; ::_thesis: verum
end;
len (MXR2MXF (LineVec2Mx (x * A))) = len (MXR2MXF (LineVec2Mx x)) by A1, MATRIXR1:def_10;
hence (LineVec2Mx x) * A = LineVec2Mx (x * A) by A6, A3, A8, MATRIX_3:def_4; ::_thesis: verum
end;
theorem Th57: :: MATRIXR2:57
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = len A & width A = len B holds
x * (A * B) = (x * A) * B
proof
let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len x = len A & width A = len B holds
x * (A * B) = (x * A) * B
let A, B be Matrix of REAL; ::_thesis: ( len x = len A & width A = len B implies x * (A * B) = (x * A) * B )
assume that
A1: len x = len A and
A2: width A = len B ; ::_thesis: x * (A * B) = (x * A) * B
width (LineVec2Mx x) = len x by MATRIXR1:def_10;
hence x * (A * B) = Line ((((LineVec2Mx x) * A) * B),1) by A1, A2, MATRIX_3:33
.= (x * A) * B by A1, Th56 ;
::_thesis: verum
end;
theorem Th58: :: MATRIXR2:58
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * (ColVec2Mx x) = ColVec2Mx (A * x)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * (ColVec2Mx x) = ColVec2Mx (A * x)
let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 & len A > 0 implies A * (ColVec2Mx x) = ColVec2Mx (A * x) )
assume that
A1: width A = len x and
A2: len x > 0 and
A3: len A > 0 ; ::_thesis: A * (ColVec2Mx x) = ColVec2Mx (A * x)
A4: len (ColVec2Mx x) = len x by A2, MATRIXR1:def_9;
A5: len (MXR2MXF (ColVec2Mx x)) = width (MXR2MXF A) by A1, A2, MATRIXR1:def_9;
then A6: width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = width (ColVec2Mx x) by MATRIX_3:def_4
.= 1 by A2, MATRIXR1:def_9 ;
A7: len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) = len A by A5, MATRIX_3:def_4;
A8: len (A * x) = len A by A1, A2, MATRIXR1:61;
then A9: width (ColVec2Mx (A * x)) = 1 by A3, MATRIXR1:def_9;
A10: len (ColVec2Mx (A * x)) = len A by A3, A8, MATRIXR1:def_9;
A11: len (ColVec2Mx (A * x)) = len (A * x) by A3, A8, MATRIXR1:def_9;
A12: for i, j being Nat st [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) holds
(MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) implies (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j)) )
A13: ( 1 in Seg 1 & Indices (ColVec2Mx (A * x)) = [:(Seg (len (ColVec2Mx (A * x)))),(Seg 1):] ) by A9, FINSEQ_1:def_3;
assume A14: [i,j] in Indices (MXR2MXF (ColVec2Mx (A * x))) ; ::_thesis: (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j))
then A15: j in Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A9, A6, ZFMISC_1:87;
A16: Indices (ColVec2Mx (A * x)) = [:(Seg (len A)),(Seg 1):] by A8, A11, A9, FINSEQ_1:def_3;
then A17: i in Seg (len A) by A14, ZFMISC_1:87;
then A18: i in dom (A * x) by A8, FINSEQ_1:def_3;
i in Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x)))) by A7, A14, A16, ZFMISC_1:87;
then [i,j] in [:(Seg (len ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))),(Seg (width ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))))):] by A15, ZFMISC_1:87;
then A19: [i,j] in Indices ((MXR2MXF A) * (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:def_3;
j in Seg 1 by A9, A14, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A20: j = 1 by XXREAL_0:1;
i in Seg (len (ColVec2Mx (A * x))) by A10, A14, A16, ZFMISC_1:87;
then [i,1] in Indices (ColVec2Mx (A * x)) by A13, ZFMISC_1:87;
then A21: ex p2 being FinSequence of REAL st
( p2 = (ColVec2Mx (A * x)) . i & (ColVec2Mx (A * x)) * (i,1) = p2 . 1 ) by MATRIX_1:def_5;
A22: (Col ((A * (ColVec2Mx x)),1)) . i = <*((A * x) . i)*> . 1 by FINSEQ_1:40
.= (ColVec2Mx (A * x)) * (i,1) by A3, A8, A18, A21, MATRIXR1:def_9 ;
len (A * (ColVec2Mx x)) = len A by A1, A4, MATRIX_3:def_4;
then i in dom (A * (ColVec2Mx x)) by A17, FINSEQ_1:def_3;
then (Col ((A * (ColVec2Mx x)),1)) . i = (A * (ColVec2Mx x)) * (i,j) by A20, MATRIX_1:def_8;
hence (MXR2MXF (ColVec2Mx (A * x))) * (i,j) = (Line ((MXR2MXF A),i)) "*" (Col ((MXR2MXF (ColVec2Mx x)),j)) by A5, A20, A22, A19, MATRIX_3:def_4; ::_thesis: verum
end;
A23: len (MXR2MXF (ColVec2Mx (A * x))) = len (MXR2MXF A) by A3, A8, MATRIXR1:def_9;
width (MXR2MXF (ColVec2Mx (A * x))) = 1 by A3, A8, MATRIXR1:def_9
.= width (MXR2MXF (ColVec2Mx x)) by A2, MATRIXR1:def_9 ;
hence A * (ColVec2Mx x) = ColVec2Mx (A * x) by A23, A5, A12, MATRIX_3:def_4; ::_thesis: verum
end;
theorem Th59: :: MATRIXR2:59
for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds
(A * B) * x = A * (B * x)
proof
let x be FinSequence of REAL ; ::_thesis: for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds
(A * B) * x = A * (B * x)
let A, B be Matrix of REAL; ::_thesis: ( len x = width B & width A = len B & len x > 0 & len B > 0 implies (A * B) * x = A * (B * x) )
assume that
A1: len x = width B and
A2: width A = len B and
A3: len x > 0 and
A4: len B > 0 ; ::_thesis: (A * B) * x = A * (B * x)
len (ColVec2Mx x) = len x by A3, MATRIXR1:def_9;
hence (A * B) * x = Col ((A * (B * (ColVec2Mx x))),1) by A1, A2, MATRIX_3:33
.= A * (B * x) by A1, A3, A4, Th58 ;
::_thesis: verum
end;
theorem :: MATRIXR2:60
for n, m, k being Element of NAT
for B being Matrix of n,m, REAL
for A being Matrix of m,k, REAL st n > 0 holds
for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
proof
let n, m, k be Element of NAT ; ::_thesis: for B being Matrix of n,m, REAL
for A being Matrix of m,k, REAL st n > 0 holds
for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
let B be Matrix of n,m, REAL ; ::_thesis: for A being Matrix of m,k, REAL st n > 0 holds
for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
let A be Matrix of m,k, REAL ; ::_thesis: ( n > 0 implies for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j )
assume A1: n > 0 ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
then A2: width B = m by MATRIX_1:23;
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (B * A) implies (B * A) * (i,j) = ((Line (B,i)) * A) . j )
A3: len A = m by MATRIX_1:def_2;
then A4: len A = len (Line (B,i)) by A2, MATRIX_1:def_7;
assume A5: [i,j] in Indices (B * A) ; ::_thesis: (B * A) * (i,j) = ((Line (B,i)) * A) . j
then A6: j in Seg (width (B * A)) by ZFMISC_1:87;
width B = len A by A1, A3, MATRIX_1:23;
then A7: (B * A) * (i,j) = (Line (B,i)) "*" (Col (A,j)) by A5, MATRPROB:39;
width A = width (B * A) by A3, A2, MATRPROB:39;
then j in Seg (len ((Line (B,i)) * A)) by A6, A4, MATRIXR1:62;
hence (B * A) * (i,j) = ((Line (B,i)) * A) . j by A7, A4, MATRPROB:40; ::_thesis: verum
end;
theorem Th61: :: MATRIXR2:61
for n being Element of NAT
for A, B being Matrix of n, REAL
for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
proof
let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL
for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
let A, B be Matrix of n, REAL ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (B * A) implies (B * A) * (i,j) = ((Line (B,i)) * A) . j )
assume A1: [i,j] in Indices (B * A) ; ::_thesis: (B * A) * (i,j) = ((Line (B,i)) * A) . j
then A2: j in Seg (width (B * A)) by ZFMISC_1:87;
A3: len A = n by MATRIX_1:def_2;
then width B = len A by MATRIX_1:24;
then A4: (B * A) * (i,j) = (Line (B,i)) "*" (Col (A,j)) by A1, MATRPROB:39;
A5: width B = n by MATRIX_1:24;
then A6: len A = len (Line (B,i)) by A3, MATRIX_1:def_7;
width A = width (B * A) by A3, A5, MATRPROB:39;
then j in Seg (len ((Line (B,i)) * A)) by A2, A6, MATRIXR1:62;
hence (B * A) * (i,j) = ((Line (B,i)) * A) . j by A4, A6, MATRPROB:40; ::_thesis: verum
end;
theorem :: MATRIXR2:62
for n being Element of NAT
for A, B being Matrix of n, REAL st n > 0 holds
for i, j being Element of NAT st [i,j] in Indices (A * B) holds
(A * B) * (i,j) = (A * (Col (B,j))) . i
proof
let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL st n > 0 holds
for i, j being Element of NAT st [i,j] in Indices (A * B) holds
(A * B) * (i,j) = (A * (Col (B,j))) . i
let A, B be Matrix of n, REAL ; ::_thesis: ( n > 0 implies for i, j being Element of NAT st [i,j] in Indices (A * B) holds
(A * B) * (i,j) = (A * (Col (B,j))) . i )
assume A1: n > 0 ; ::_thesis: for i, j being Element of NAT st [i,j] in Indices (A * B) holds
(A * B) * (i,j) = (A * (Col (B,j))) . i
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (A * B) implies (A * B) * (i,j) = (A * (Col (B,j))) . i )
A2: width A = n by MATRIX_1:24;
assume A3: [i,j] in Indices (A * B) ; ::_thesis: (A * B) * (i,j) = (A * (Col (B,j))) . i
then i in dom (A * B) by ZFMISC_1:87;
then A4: i in Seg (len (A * B)) by FINSEQ_1:def_3;
A5: len B = n by MATRIX_1:def_2;
then A6: width A = len (Col (B,j)) by A2, MATRIX_1:def_8;
width A = len B by A5, MATRIX_1:24;
then A7: (A * B) * (i,j) = (Line (A,i)) "*" (Col (B,j)) by A3, MATRPROB:39;
( len (A * B) = n & len A = n ) by MATRIX_1:24;
then i in Seg (len (A * (Col (B,j)))) by A1, A4, A2, A6, MATRIXR1:61;
hence (A * B) * (i,j) = (A * (Col (B,j))) . i by A1, A2, A7, A6, MATRPROB:41; ::_thesis: verum
end;
begin
definition
let n be Element of NAT ;
func 1_Rmatrix n -> Matrix of n, REAL equals :: MATRIXR2:def 2
MXF2MXR (1. (F_Real,n));
correctness
coherence
MXF2MXR (1. (F_Real,n)) is Matrix of n, REAL ;
;
end;
:: deftheorem defines 1_Rmatrix MATRIXR2:def_2_:_
for n being Element of NAT holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n));
theorem Th63: :: MATRIXR2:63
for n being Element of NAT holds
( ( for i being Element of NAT st [i,i] in Indices (1_Rmatrix n) holds
(1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Element of NAT st [i,j] in Indices (1_Rmatrix n) & i <> j holds
(1_Rmatrix n) * (i,j) = 0 ) )
proof
let n be Element of NAT ; ::_thesis: ( ( for i being Element of NAT st [i,i] in Indices (1_Rmatrix n) holds
(1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Element of NAT st [i,j] in Indices (1_Rmatrix n) & i <> j holds
(1_Rmatrix n) * (i,j) = 0 ) )
set K = F_Real ;
thus for i being Element of NAT st [i,i] in Indices (1_Rmatrix n) holds
(1_Rmatrix n) * (i,i) = 1 ::_thesis: for i, j being Element of NAT st [i,j] in Indices (1_Rmatrix n) & i <> j holds
(1_Rmatrix n) * (i,j) = 0
proof
let i be Element of NAT ; ::_thesis: ( [i,i] in Indices (1_Rmatrix n) implies (1_Rmatrix n) * (i,i) = 1 )
assume [i,i] in Indices (1_Rmatrix n) ; ::_thesis: (1_Rmatrix n) * (i,i) = 1
hence (1_Rmatrix n) * (i,i) = 1_ F_Real by MATRIX_1:def_11
.= 1 ;
::_thesis: verum
end;
let i, j be Element of NAT ; ::_thesis: ( [i,j] in Indices (1_Rmatrix n) & i <> j implies (1_Rmatrix n) * (i,j) = 0 )
assume ( [i,j] in Indices (1_Rmatrix n) & i <> j ) ; ::_thesis: (1_Rmatrix n) * (i,j) = 0
hence (1_Rmatrix n) * (i,j) = 0. F_Real by MATRIX_1:def_11
.= 0 ;
::_thesis: verum
end;
theorem Th64: :: MATRIXR2:64
for n being Element of NAT holds (1_Rmatrix n) @ = 1_Rmatrix n
proof
let n be Element of NAT ; ::_thesis: (1_Rmatrix n) @ = 1_Rmatrix n
percases ( n > 0 or n = 0 ) ;
supposeA1: n > 0 ; ::_thesis: (1_Rmatrix n) @ = 1_Rmatrix n
A2: len (1_Rmatrix n) = n by MATRIX_1:24;
A3: Indices (1_Rmatrix n) = [:(Seg n),(Seg n):] by MATRIX_1:24;
A4: for i, j being Nat st [i,j] in Indices (1_Rmatrix n) holds
(1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j)
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (1_Rmatrix n) implies (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) )
reconsider i0 = i, j0 = j as Element of NAT by ORDINAL1:def_12;
assume A5: [i,j] in Indices (1_Rmatrix n) ; ::_thesis: (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j)
then ( i in Seg n & j in Seg n ) by A3, ZFMISC_1:87;
then A6: [j,i] in Indices (1_Rmatrix n) by A3, ZFMISC_1:87;
percases ( i = j or i <> j ) ;
suppose i = j ; ::_thesis: (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j)
hence (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) by A5, MATRIX_1:def_6; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j)
then ( (1_Rmatrix n) * (i0,j0) = 0 & (1_Rmatrix n) * (j0,i0) = 0 ) by A5, A6, Th63;
hence (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) by A6, MATRIX_1:def_6; ::_thesis: verum
end;
end;
end;
A7: width (1_Rmatrix n) = n by MATRIX_1:24;
then ( len ((1_Rmatrix n) @) = width (1_Rmatrix n) & width ((1_Rmatrix n) @) = len (1_Rmatrix n) ) by A1, MATRIX_2:10;
hence (1_Rmatrix n) @ = 1_Rmatrix n by A7, A2, A4, MATRIX_1:21; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (1_Rmatrix n) @ = 1_Rmatrix n
hence (1_Rmatrix n) @ = 1_Rmatrix n by MATRIX_1:35; ::_thesis: verum
end;
end;
end;
theorem Th65: :: MATRIXR2:65
for n, m being Element of NAT st n > 0 holds
(0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)
proof
let n, m be Element of NAT ; ::_thesis: ( n > 0 implies (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) )
assume A1: n > 0 ; ::_thesis: (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)
then ( width (0_Rmatrix (n,m)) = m & len (0_Rmatrix (n,m)) = n ) by MATRIX_1:23;
then (0 + 0) * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) by A1, MATRIXR1:44;
hence (0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) by Th12; ::_thesis: verum
end;
theorem :: MATRIXR2:66
for n, m being Element of NAT
for a being Real st n > 0 holds
a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)
proof
let n, m be Element of NAT ; ::_thesis: for a being Real st n > 0 holds
a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)
let a be Real; ::_thesis: ( n > 0 implies a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) )
A1: ( len (a * (0_Rmatrix (n,m))) = len (0_Rmatrix (n,m)) & width (a * (0_Rmatrix (n,m))) = width (0_Rmatrix (n,m)) ) by MATRIXR1:27;
assume A2: n > 0 ; ::_thesis: a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)
then A3: ( width (0_Rmatrix (n,m)) = m & len (0_Rmatrix (n,m)) = n ) by MATRIX_1:23;
a * (0_Rmatrix (n,m)) = a * ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) by A2, Th65
.= (a * (0_Rmatrix (n,m))) + (a * (0_Rmatrix (n,m))) by A3, MATRIXR1:43 ;
hence a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m) by A3, A1, MATRIXR1:37; ::_thesis: verum
end;
theorem Th67: :: MATRIXR2:67
for K being Field
for A being Matrix of K holds A * (1. (K,(width A))) = A
proof
let K be Field; ::_thesis: for A being Matrix of K holds A * (1. (K,(width A))) = A
let A be Matrix of K; ::_thesis: A * (1. (K,(width A))) = A
set n = width A;
set B = 1. (K,(width A));
A1: width (1. (K,(width A))) = width A by MATRIX_1:24;
A2: len (1. (K,(width A))) = width A by MATRIX_1:24;
then A3: width (A * (1. (K,(width A)))) = width (1. (K,(width A))) by MATRIX_3:def_4;
A4: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_(A_*_(1._(K,(width_A))))_holds_
(A_*_(1._(K,(width_A))))_*_(i,j)_=_A_*_(i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices (A * (1. (K,(width A)))) implies (A * (1. (K,(width A)))) * (i,j) = A * (i,j) )
assume A5: [i,j] in Indices (A * (1. (K,(width A)))) ; ::_thesis: (A * (1. (K,(width A)))) * (i,j) = A * (i,j)
then A6: j in Seg (width (1. (K,(width A)))) by A3, ZFMISC_1:87;
then j in Seg (len (Line (A,i))) by A1, MATRIX_1:def_7;
then A7: j in dom (Line (A,i)) by FINSEQ_1:def_3;
A8: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Col_((1._(K,(width_A))),j))_&_k_<>_j_holds_
(Col_((1._(K,(width_A))),j))_._k_=_0._K
let k be Nat; ::_thesis: ( k in dom (Col ((1. (K,(width A))),j)) & k <> j implies (Col ((1. (K,(width A))),j)) . k = 0. K )
assume that
A9: k in dom (Col ((1. (K,(width A))),j)) and
A10: k <> j ; ::_thesis: (Col ((1. (K,(width A))),j)) . k = 0. K
k in Seg (len (Col ((1. (K,(width A))),j))) by A9, FINSEQ_1:def_3;
then k in Seg (len (1. (K,(width A)))) by MATRIX_1:def_8;
then k in dom (1. (K,(width A))) by FINSEQ_1:def_3;
then [k,j] in Indices (1. (K,(width A))) by A6, ZFMISC_1:87;
hence (Col ((1. (K,(width A))),j)) . k = 0. K by A10, MATRIX_3:16; ::_thesis: verum
end;
A11: j in Seg (width A) by A1, A3, A5, ZFMISC_1:87;
then j in dom (1. (K,(width A))) by A2, FINSEQ_1:def_3;
then [j,j] in Indices (1. (K,(width A))) by A1, A11, ZFMISC_1:87;
then A12: (Col ((1. (K,(width A))),j)) . j = 1_ K by MATRIX_3:16;
j in Seg (len (Col ((1. (K,(width A))),j))) by A2, A1, A6, MATRIX_1:def_8;
then A13: j in dom (Col ((1. (K,(width A))),j)) by FINSEQ_1:def_3;
thus (A * (1. (K,(width A)))) * (i,j) = (Line (A,i)) "*" (Col ((1. (K,(width A))),j)) by A2, A5, MATRIX_3:def_4
.= (Col ((1. (K,(width A))),j)) "*" (Line (A,i)) by FVSUM_1:90
.= Sum (mlt ((Col ((1. (K,(width A))),j)),(Line (A,i)))) by FVSUM_1:def_9
.= (Line (A,i)) . j by A13, A7, A8, A12, MATRIX_3:17
.= A * (i,j) by A11, MATRIX_1:def_7 ; ::_thesis: verum
end;
len (A * (1. (K,(width A)))) = len A by A2, MATRIX_3:def_4;
hence A * (1. (K,(width A))) = A by A1, A3, A4, MATRIX_1:21; ::_thesis: verum
end;
theorem Th68: :: MATRIXR2:68
for K being Field
for A being Matrix of K holds (1. (K,(len A))) * A = A
proof
let K be Field; ::_thesis: for A being Matrix of K holds (1. (K,(len A))) * A = A
let A be Matrix of K; ::_thesis: (1. (K,(len A))) * A = A
set n = len A;
set B = 1. (K,(len A));
A1: len (1. (K,(len A))) = len A by MATRIX_1:24;
A2: width (1. (K,(len A))) = len A by MATRIX_1:24;
then A3: len ((1. (K,(len A))) * A) = len (1. (K,(len A))) by MATRIX_3:def_4;
A4: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_((1._(K,(len_A)))_*_A)_holds_
((1._(K,(len_A)))_*_A)_*_(i,j)_=_A_*_(i,j)
A5: dom A = Seg (len A) by FINSEQ_1:def_3;
let i, j be Nat; ::_thesis: ( [i,j] in Indices ((1. (K,(len A))) * A) implies ((1. (K,(len A))) * A) * (i,j) = A * (i,j) )
assume A6: [i,j] in Indices ((1. (K,(len A))) * A) ; ::_thesis: ((1. (K,(len A))) * A) * (i,j) = A * (i,j)
A7: dom ((1. (K,(len A))) * A) = Seg (len ((1. (K,(len A))) * A)) by FINSEQ_1:def_3;
then A8: i in Seg (width (1. (K,(len A)))) by A1, A2, A3, A6, ZFMISC_1:87;
then i in Seg (len (Line ((1. (K,(len A))),i))) by MATRIX_1:def_7;
then A9: i in dom (Line ((1. (K,(len A))),i)) by FINSEQ_1:def_3;
A10: dom (1. (K,(len A))) = Seg (len (1. (K,(len A)))) by FINSEQ_1:def_3;
then A11: i in dom (1. (K,(len A))) by A3, A6, A7, ZFMISC_1:87;
then [i,i] in Indices (1. (K,(len A))) by A8, ZFMISC_1:87;
then A12: (Line ((1. (K,(len A))),i)) . i = 1_ K by MATRIX_3:15;
i in Seg (len (Col (A,j))) by A2, A8, MATRIX_1:def_8;
then A13: i in dom (Col (A,j)) by FINSEQ_1:def_3;
A14: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Line_((1._(K,(len_A))),i))_&_k_<>_i_holds_
(Line_((1._(K,(len_A))),i))_._k_=_0._K
let k be Nat; ::_thesis: ( k in dom (Line ((1. (K,(len A))),i)) & k <> i implies (Line ((1. (K,(len A))),i)) . k = 0. K )
assume that
A15: k in dom (Line ((1. (K,(len A))),i)) and
A16: k <> i ; ::_thesis: (Line ((1. (K,(len A))),i)) . k = 0. K
k in Seg (len (Line ((1. (K,(len A))),i))) by A15, FINSEQ_1:def_3;
then k in Seg (width (1. (K,(len A)))) by MATRIX_1:def_7;
then [i,k] in Indices (1. (K,(len A))) by A11, ZFMISC_1:87;
hence (Line ((1. (K,(len A))),i)) . k = 0. K by A16, MATRIX_3:15; ::_thesis: verum
end;
thus ((1. (K,(len A))) * A) * (i,j) = (Line ((1. (K,(len A))),i)) "*" (Col (A,j)) by A2, A6, MATRIX_3:def_4
.= Sum (mlt ((Line ((1. (K,(len A))),i)),(Col (A,j)))) by FVSUM_1:def_9
.= (Col (A,j)) . i by A9, A13, A14, A12, MATRIX_3:17
.= A * (i,j) by A1, A5, A10, A11, MATRIX_1:def_8 ; ::_thesis: verum
end;
width ((1. (K,(len A))) * A) = width A by A2, MATRIX_3:def_4;
hence (1. (K,(len A))) * A = A by A1, A3, A4, MATRIX_1:21; ::_thesis: verum
end;
theorem :: MATRIXR2:69
for n, m being Element of NAT
for A being Matrix of REAL holds
( ( n = width A implies A * (1_Rmatrix n) = A ) & ( m = len A implies (1_Rmatrix m) * A = A ) ) by Th67, Th68;
theorem Th70: :: MATRIXR2:70
for n being Element of NAT
for A being Matrix of n, REAL holds (1_Rmatrix n) * A = A
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL holds (1_Rmatrix n) * A = A
let A be Matrix of n, REAL ; ::_thesis: (1_Rmatrix n) * A = A
n = len A by MATRIX_1:def_2;
hence (1_Rmatrix n) * A = A by Th68; ::_thesis: verum
end;
theorem Th71: :: MATRIXR2:71
for n being Element of NAT
for A being Matrix of n, REAL holds A * (1_Rmatrix n) = A
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL holds A * (1_Rmatrix n) = A
let A be Matrix of n, REAL ; ::_thesis: A * (1_Rmatrix n) = A
A1: n = len A by MATRIX_1:def_2;
now__::_thesis:_(_(_n_<>_0_&_n_=_width_A_)_or_(_n_=_0_&_n_=_width_A_)_)
percases ( n <> 0 or n = 0 ) ;
case n <> 0 ; ::_thesis: n = width A
hence n = width A by A1, MATRIX_1:20; ::_thesis: verum
end;
case n = 0 ; ::_thesis: n = width A
hence n = width A by A1, MATRIX_1:def_3; ::_thesis: verum
end;
end;
end;
hence A * (1_Rmatrix n) = A by Th67; ::_thesis: verum
end;
theorem Th72: :: MATRIXR2:72
for n being Element of NAT holds Det (1_Rmatrix n) = 1
proof
let n be Element of NAT ; ::_thesis: Det (1_Rmatrix n) = 1
percases ( n >= 1 or n < 1 ) ;
suppose n >= 1 ; ::_thesis: Det (1_Rmatrix n) = 1
hence Det (1_Rmatrix n) = 1_ F_Real by MATRIX_7:16
.= 1 ;
::_thesis: verum
end;
suppose n < 1 ; ::_thesis: Det (1_Rmatrix n) = 1
then n = 0 by NAT_1:25;
hence Det (1_Rmatrix n) = 1. F_Real by Th41
.= 1 ;
::_thesis: verum
end;
end;
end;
definition
let n be Element of NAT ;
func 0_Rmatrix n -> Matrix of n, REAL equals :: MATRIXR2:def 3
0_Rmatrix (n,n);
correctness
coherence
0_Rmatrix (n,n) is Matrix of n, REAL ;
;
end;
:: deftheorem defines 0_Rmatrix MATRIXR2:def_3_:_
for n being Element of NAT holds 0_Rmatrix n = 0_Rmatrix (n,n);
theorem :: MATRIXR2:73
for n being Element of NAT st n > 0 holds
Det (0_Rmatrix n) = 0
proof
let n be Element of NAT ; ::_thesis: ( n > 0 implies Det (0_Rmatrix n) = 0 )
set K = F_Real ;
assume n > 0 ; ::_thesis: Det (0_Rmatrix n) = 0
then n >= 0 + 1 by NAT_1:13;
then Det (0_Rmatrix n) = 0. F_Real by MATRIX_7:15
.= 0 ;
hence Det (0_Rmatrix n) = 0 ; ::_thesis: verum
end;
definition
let n, i be Nat;
func Base_FinSeq (n,i) -> FinSequence of REAL equals :: MATRIXR2:def 4
(n |-> 0) +* (i,1);
coherence
(n |-> 0) +* (i,1) is FinSequence of REAL
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
(n |-> 0) +* (i,1) = Replace ((n |-> 0),i,1) ;
hence (n |-> 0) +* (i,1) is FinSequence of REAL ; ::_thesis: verum
end;
end;
:: deftheorem defines Base_FinSeq MATRIXR2:def_4_:_
for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1);
theorem Th74: :: MATRIXR2:74
for n, i being Nat holds len (Base_FinSeq (n,i)) = n
proof
let n, i be Nat; ::_thesis: len (Base_FinSeq (n,i)) = n
len ((n |-> 0) +* (i,1)) = len (n |-> 0) by FUNCT_7:97
.= n by CARD_1:def_7 ;
hence len (Base_FinSeq (n,i)) = n ; ::_thesis: verum
end;
theorem Th75: :: MATRIXR2:75
for i, n being Nat st 1 <= i & i <= n holds
(Base_FinSeq (n,i)) . i = 1
proof
let i, n be Nat; ::_thesis: ( 1 <= i & i <= n implies (Base_FinSeq (n,i)) . i = 1 )
A1: len (n |-> 0) = n by CARD_1:def_7;
assume ( 1 <= i & i <= n ) ; ::_thesis: (Base_FinSeq (n,i)) . i = 1
then i in dom (n |-> 0) by A1, FINSEQ_3:25;
hence (Base_FinSeq (n,i)) . i = 1 by FUNCT_7:31; ::_thesis: verum
end;
theorem Th76: :: MATRIXR2:76
for j, n, i being Nat st 1 <= j & j <= n & i <> j holds
(Base_FinSeq (n,i)) . j = 0
proof
let j, n, i be Nat; ::_thesis: ( 1 <= j & j <= n & i <> j implies (Base_FinSeq (n,i)) . j = 0 )
assume that
A1: ( 1 <= j & j <= n ) and
A2: i <> j ; ::_thesis: (Base_FinSeq (n,i)) . j = 0
A3: j in Seg n by A1, FINSEQ_1:1;
thus (Base_FinSeq (n,i)) . j = (n |-> 0) . j by A2, FUNCT_7:32
.= 0 by A3, FINSEQ_2:57 ; ::_thesis: verum
end;
theorem :: MATRIXR2:77
( Base_FinSeq (1,1) = <*1*> & Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
proof
thus Base_FinSeq (1,1) = Replace (<*0*>,1,1) by FINSEQ_2:59
.= <*1*> by FINSEQ_7:12 ; ::_thesis: ( Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (2,1) = Replace (<*0,0*>,1,1) by FINSEQ_2:61
.= <*1,0*> by FINSEQ_7:13 ; ::_thesis: ( Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (2,2) = Replace (<*0,0*>,2,1) by FINSEQ_2:61
.= <*0,1*> by FINSEQ_7:14 ; ::_thesis: ( Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (3,1) = Replace (<*0,0,0*>,1,1) by FINSEQ_2:62
.= <*1,0,0*> by FINSEQ_7:15 ; ::_thesis: ( Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )
thus Base_FinSeq (3,2) = Replace (<*0,0,0*>,2,1) by FINSEQ_2:62
.= <*0,1,0*> by FINSEQ_7:16 ; ::_thesis: Base_FinSeq (3,3) = <*0,0,1*>
thus Base_FinSeq (3,3) = Replace (<*0,0,0*>,3,1) by FINSEQ_2:62
.= <*0,0,1*> by FINSEQ_7:17 ; ::_thesis: verum
end;
theorem Th78: :: MATRIXR2:78
for i being Nat
for n being Element of NAT st 1 <= i & i <= n holds
(1_Rmatrix n) . i = Base_FinSeq (n,i)
proof
let i be Nat; ::_thesis: for n being Element of NAT st 1 <= i & i <= n holds
(1_Rmatrix n) . i = Base_FinSeq (n,i)
let n be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies (1_Rmatrix n) . i = Base_FinSeq (n,i) )
assume A1: ( 1 <= i & i <= n ) ; ::_thesis: (1_Rmatrix n) . i = Base_FinSeq (n,i)
then 1 <= n by XXREAL_0:2;
then A2: 1 in Seg n ;
i in NAT by ORDINAL1:def_12;
then i in Seg n by A1;
then [i,1] in [:(Seg n),(Seg n):] by A2, ZFMISC_1:87;
then [i,1] in Indices (1. (F_Real,n)) by MATRIX_1:24;
then consider q being FinSequence of REAL such that
A3: q = (1_Rmatrix n) . i and
(1_Rmatrix n) * (i,1) = q . 1 by MATRIX_1:def_5;
len (1_Rmatrix n) = n by MATRIX_1:24;
then i in dom (1_Rmatrix n) by A1, FINSEQ_3:25;
then q in rng (1_Rmatrix n) by A3, FUNCT_1:def_3;
then A4: len q = n by MATRIX_1:def_2;
A5: for j being Nat st 1 <= j & j <= n holds
q . j = (Base_FinSeq (n,i)) . j
proof
i in NAT by ORDINAL1:def_12;
then A6: i in Seg n by A1;
let j be Nat; ::_thesis: ( 1 <= j & j <= n implies q . j = (Base_FinSeq (n,i)) . j )
assume A7: ( 1 <= j & j <= n ) ; ::_thesis: q . j = (Base_FinSeq (n,i)) . j
j in NAT by ORDINAL1:def_12;
then j in Seg n by A7;
then [i,j] in [:(Seg n),(Seg n):] by A6, ZFMISC_1:87;
then A8: [i,j] in Indices (1. (F_Real,n)) by MATRIX_1:24;
then A9: ex q0 being FinSequence of REAL st
( q0 = (1_Rmatrix n) . i & (1_Rmatrix n) * (i,j) = q0 . j ) by MATRIX_1:def_5;
percases ( i = j or i <> j ) ;
supposeA10: i = j ; ::_thesis: q . j = (Base_FinSeq (n,i)) . j
then (1. (F_Real,n)) * (i,i) = 1_ F_Real by A8, MATRIX_1:def_11;
hence q . j = (Base_FinSeq (n,i)) . j by A1, A3, A9, A10, Th75; ::_thesis: verum
end;
supposeA11: i <> j ; ::_thesis: q . j = (Base_FinSeq (n,i)) . j
then (1. (F_Real,n)) * (i,j) = 0. F_Real by A8, MATRIX_1:def_11;
hence q . j = (Base_FinSeq (n,i)) . j by A3, A7, A9, A11, Th76; ::_thesis: verum
end;
end;
end;
len (Base_FinSeq (n,i)) = n by Th74;
hence (1_Rmatrix n) . i = Base_FinSeq (n,i) by A3, A4, A5, FINSEQ_1:14; ::_thesis: verum
end;
begin
definition
let n be Element of NAT ;
let A be Matrix of n, REAL ;
attrA is invertible means :Def5: :: MATRIXR2:def 5
ex B being Matrix of n, REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n );
end;
:: deftheorem Def5 defines invertible MATRIXR2:def_5_:_
for n being Element of NAT
for A being Matrix of n, REAL holds
( A is invertible iff ex B being Matrix of n, REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ) );
definition
let n be Element of NAT ;
let A be Matrix of n, REAL ;
assume A1: A is invertible ;
func Inv A -> Matrix of n, REAL means :Def6: :: MATRIXR2:def 6
( it * A = 1_Rmatrix n & A * it = 1_Rmatrix n );
existence
ex b1 being Matrix of n, REAL st
( b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n ) by A1, Def5;
uniqueness
for b1, b2 being Matrix of n, REAL st b1 * A = 1_Rmatrix n & A * b1 = 1_Rmatrix n & b2 * A = 1_Rmatrix n & A * b2 = 1_Rmatrix n holds
b1 = b2
proof
let B1, B2 be Matrix of n, REAL ; ::_thesis: ( B1 * A = 1_Rmatrix n & A * B1 = 1_Rmatrix n & B2 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n implies B1 = B2 )
assume that
B1 * A = 1_Rmatrix n and
A2: A * B1 = 1_Rmatrix n and
A3: B2 * A = 1_Rmatrix n and
A * B2 = 1_Rmatrix n ; ::_thesis: B1 = B2
A4: ( len A = n & width A = n ) by MATRIX_1:24;
( len B1 = n & width B2 = n ) by MATRIX_1:24;
then (B2 * A) * B1 = B2 * (1_Rmatrix n) by A2, A4, MATRIX_3:33;
then B1 = B2 * (1_Rmatrix n) by A3, Th70;
hence B1 = B2 by Th71; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Inv MATRIXR2:def_6_:_
for n being Element of NAT
for A being Matrix of n, REAL st A is invertible holds
for b3 being Matrix of n, REAL holds
( b3 = Inv A iff ( b3 * A = 1_Rmatrix n & A * b3 = 1_Rmatrix n ) );
registration
let n be Element of NAT ;
cluster 1_Rmatrix n -> invertible ;
coherence
1_Rmatrix n is invertible
proof
(1_Rmatrix n) * (1_Rmatrix n) = 1_Rmatrix n by Th70;
hence 1_Rmatrix n is invertible by Def5; ::_thesis: verum
end;
end;
theorem :: MATRIXR2:79
for n being Element of NAT holds Inv (1_Rmatrix n) = 1_Rmatrix n
proof
let n be Element of NAT ; ::_thesis: Inv (1_Rmatrix n) = 1_Rmatrix n
(1_Rmatrix n) * (1_Rmatrix n) = 1_Rmatrix n by Th70;
hence Inv (1_Rmatrix n) = 1_Rmatrix n by Def6; ::_thesis: verum
end;
theorem Th80: :: MATRIXR2:80
for n being Element of NAT
for A, B1, B2 being Matrix of n, REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds
( B1 = B2 & A is invertible )
proof
let n be Element of NAT ; ::_thesis: for A, B1, B2 being Matrix of n, REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds
( B1 = B2 & A is invertible )
let A, B1, B2 be Matrix of n, REAL ; ::_thesis: ( B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n implies ( B1 = B2 & A is invertible ) )
assume that
A1: B1 * A = 1_Rmatrix n and
A2: A * B2 = 1_Rmatrix n ; ::_thesis: ( B1 = B2 & A is invertible )
A3: (B1 * A) * B2 = B1 * (A * B2) by Th28
.= B1 by A2, Th71 ;
hence B1 = B2 by A1, Th70; ::_thesis: A is invertible
(B1 * A) * B2 = B2 by A1, Th70;
hence A is invertible by A1, A2, A3, Def5; ::_thesis: verum
end;
theorem :: MATRIXR2:81
for n being Element of NAT
for A being Matrix of n, REAL st A is invertible holds
Det (Inv A) = (Det A) "
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds
Det (Inv A) = (Det A) "
let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies Det (Inv A) = (Det A) " )
assume A is invertible ; ::_thesis: Det (Inv A) = (Det A) "
then A * (Inv A) = 1_Rmatrix n by Def6;
then Det (A * (Inv A)) = 1 by Th72;
then A1: (Det A) * (Det (Inv A)) = 1 by Th46;
percases ( Det A <> 0 or Det A = 0 ) ;
suppose Det A <> 0 ; ::_thesis: Det (Inv A) = (Det A) "
hence Det (Inv A) = (Det A) " by A1, XCMPLX_0:def_7; ::_thesis: verum
end;
suppose Det A = 0 ; ::_thesis: Det (Inv A) = (Det A) "
hence Det (Inv A) = (Det A) " by A1; ::_thesis: verum
end;
end;
end;
theorem :: MATRIXR2:82
for n being Element of NAT
for A being Matrix of n, REAL st A is invertible holds
Det A <> 0
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds
Det A <> 0
let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies Det A <> 0 )
assume A is invertible ; ::_thesis: Det A <> 0
then A * (Inv A) = 1_Rmatrix n by Def6;
then Det (A * (Inv A)) = 1 by Th72;
then (Det A) * (Det (Inv A)) = 1 by Th46;
hence Det A <> 0 ; ::_thesis: verum
end;
theorem :: MATRIXR2:83
for n being Element of NAT
for A, B being Matrix of n, REAL st A is invertible & B is invertible holds
( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )
proof
let n be Element of NAT ; ::_thesis: for A, B being Matrix of n, REAL st A is invertible & B is invertible holds
( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )
let A, B be Matrix of n, REAL ; ::_thesis: ( A is invertible & B is invertible implies ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) ) )
assume that
A1: A is invertible and
A2: B is invertible ; ::_thesis: ( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )
A3: ((Inv B) * (Inv A)) * (A * B) = (((Inv B) * (Inv A)) * A) * B by Th28
.= ((Inv B) * ((Inv A) * A)) * B by Th28
.= ((Inv B) * (1_Rmatrix n)) * B by A1, Def6
.= (Inv B) * B by Th71
.= 1_Rmatrix n by A2, Def6 ;
A4: (A * B) * ((Inv B) * (Inv A)) = A * (B * ((Inv B) * (Inv A))) by Th28
.= A * ((B * (Inv B)) * (Inv A)) by Th28
.= A * ((1_Rmatrix n) * (Inv A)) by A2, Def6
.= (A * (1_Rmatrix n)) * (Inv A) by Th28
.= A * (Inv A) by Th71
.= 1_Rmatrix n by A1, Def6 ;
hence A * B is invertible by A3, Def5; ::_thesis: Inv (A * B) = (Inv B) * (Inv A)
hence Inv (A * B) = (Inv B) * (Inv A) by A3, A4, Def6; ::_thesis: verum
end;
theorem :: MATRIXR2:84
for n being Element of NAT
for A being Matrix of n, REAL st A is invertible holds
Inv (Inv A) = A
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds
Inv (Inv A) = A
let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies Inv (Inv A) = A )
assume A is invertible ; ::_thesis: Inv (Inv A) = A
then A1: ( (Inv A) * A = 1_Rmatrix n & A * (Inv A) = 1_Rmatrix n ) by Def6;
then Inv A is invertible by Def5;
hence Inv (Inv A) = A by A1, Def6; ::_thesis: verum
end;
theorem :: MATRIXR2:85
( 1_Rmatrix 0 = 0_Rmatrix 0 & 1_Rmatrix 0 = {} )
proof
A1: len (1_Rmatrix 0) = 0 by MATRIX_1:24;
len (0_Rmatrix 0) = 0 by MATRIX_1:24;
then 0_Rmatrix 0 = {} ;
hence 1_Rmatrix 0 = 0_Rmatrix 0 by A1; ::_thesis: 1_Rmatrix 0 = {}
thus 1_Rmatrix 0 = {} by A1; ::_thesis: verum
end;
theorem Th86: :: MATRIXR2:86
for n being Element of NAT
for x being FinSequence of REAL st len x = n & n > 0 holds
(1_Rmatrix n) * x = x
proof
let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = n & n > 0 holds
(1_Rmatrix n) * x = x
let x be FinSequence of REAL ; ::_thesis: ( len x = n & n > 0 implies (1_Rmatrix n) * x = x )
assume that
A1: len x = n and
A2: n > 0 ; ::_thesis: (1_Rmatrix n) * x = x
A3: len (ColVec2Mx x) = len x by A1, A2, MATRIXR1:def_9;
A4: len (Col ((ColVec2Mx x),1)) = len (ColVec2Mx x) by MATRIX_1:def_8;
A5: for k being Nat st 1 <= k & k <= len (Col ((ColVec2Mx x),1)) holds
(Col ((ColVec2Mx x),1)) . k = x . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len (Col ((ColVec2Mx x),1)) implies (Col ((ColVec2Mx x),1)) . k = x . k )
assume A6: ( 1 <= k & k <= len (Col ((ColVec2Mx x),1)) ) ; ::_thesis: (Col ((ColVec2Mx x),1)) . k = x . k
k in NAT by ORDINAL1:def_12;
then A7: k in Seg (len (ColVec2Mx x)) by A4, A6;
then A8: k in dom (ColVec2Mx x) by FINSEQ_1:def_3;
then A9: (Col ((ColVec2Mx x),1)) . k = (ColVec2Mx x) * (k,1) by MATRIX_1:def_8;
( 1 in Seg 1 & Indices (ColVec2Mx x) = [:(dom (ColVec2Mx x)),(Seg 1):] ) by A1, A2, MATRIXR1:def_9;
then [k,1] in Indices (ColVec2Mx x) by A8, ZFMISC_1:87;
then consider p being FinSequence of REAL such that
A10: p = (ColVec2Mx x) . k and
A11: (ColVec2Mx x) * (k,1) = p . 1 by MATRIX_1:def_5;
k in dom x by A3, A7, FINSEQ_1:def_3;
then p = <*(x . k)*> by A1, A2, A10, MATRIXR1:def_9;
hence (Col ((ColVec2Mx x),1)) . k = x . k by A9, A11, FINSEQ_1:40; ::_thesis: verum
end;
(1_Rmatrix n) * x = Col ((MXF2MXR (MXR2MXF (ColVec2Mx x))),1) by A1, A3, Th68
.= x by A3, A4, A5, FINSEQ_1:14 ;
hence (1_Rmatrix n) * x = x ; ::_thesis: verum
end;
theorem Th87: :: MATRIXR2:87
for n being Element of NAT
for x, y being FinSequence of REAL
for A being Matrix of n, REAL st A is invertible & len x = n & len y = n & n > 0 holds
( A * x = y iff x = (Inv A) * y )
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSequence of REAL
for A being Matrix of n, REAL st A is invertible & len x = n & len y = n & n > 0 holds
( A * x = y iff x = (Inv A) * y )
let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st A is invertible & len x = n & len y = n & n > 0 holds
( A * x = y iff x = (Inv A) * y )
let A be Matrix of n, REAL ; ::_thesis: ( A is invertible & len x = n & len y = n & n > 0 implies ( A * x = y iff x = (Inv A) * y ) )
assume that
A1: A is invertible and
A2: len x = n and
A3: len y = n and
A4: n > 0 ; ::_thesis: ( A * x = y iff x = (Inv A) * y )
A5: ( width A = n & width (Inv A) = n ) by MATRIX_1:24;
A6: len A = n by MATRIX_1:24;
thus ( A * x = y implies x = (Inv A) * y ) ::_thesis: ( x = (Inv A) * y implies A * x = y )
proof
assume A7: A * x = y ; ::_thesis: x = (Inv A) * y
thus x = (1_Rmatrix n) * x by A2, A4, Th86
.= ((Inv A) * A) * x by A1, Def6
.= (Inv A) * y by A2, A4, A6, A5, A7, Th59 ; ::_thesis: verum
end;
A8: len (Inv A) = n by MATRIX_1:24;
( x = (Inv A) * y implies A * x = y )
proof
assume A9: x = (Inv A) * y ; ::_thesis: A * x = y
thus y = (1_Rmatrix n) * y by A3, A4, Th86
.= (A * (Inv A)) * y by A1, Def6
.= A * x by A3, A4, A8, A5, A9, Th59 ; ::_thesis: verum
end;
hence ( x = (Inv A) * y implies A * x = y ) ; ::_thesis: verum
end;
theorem Th88: :: MATRIXR2:88
for n being Element of NAT
for x being FinSequence of REAL st len x = n holds
x * (1_Rmatrix n) = x
proof
let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = n holds
x * (1_Rmatrix n) = x
let x be FinSequence of REAL ; ::_thesis: ( len x = n implies x * (1_Rmatrix n) = x )
A1: width (LineVec2Mx x) = len x by MATRIXR1:def_10;
assume len x = n ; ::_thesis: x * (1_Rmatrix n) = x
then x * (1_Rmatrix n) = Line ((MXF2MXR (MXR2MXF (LineVec2Mx x))),1) by A1, Th67
.= x by MATRIXR1:48 ;
hence x * (1_Rmatrix n) = x ; ::_thesis: verum
end;
theorem Th89: :: MATRIXR2:89
for n being Element of NAT
for x, y being FinSequence of REAL
for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds
( x * A = y iff x = y * (Inv A) )
proof
let n be Element of NAT ; ::_thesis: for x, y being FinSequence of REAL
for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds
( x * A = y iff x = y * (Inv A) )
let x, y be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds
( x * A = y iff x = y * (Inv A) )
let A be Matrix of n, REAL ; ::_thesis: ( A is invertible & len x = n & len y = n implies ( x * A = y iff x = y * (Inv A) ) )
assume that
A1: A is invertible and
A2: len x = n and
A3: len y = n ; ::_thesis: ( x * A = y iff x = y * (Inv A) )
A4: ( len A = n & len (Inv A) = n ) by MATRIX_1:24;
A5: width A = n by MATRIX_1:24;
thus ( x * A = y implies x = y * (Inv A) ) ::_thesis: ( x = y * (Inv A) implies x * A = y )
proof
assume A6: x * A = y ; ::_thesis: x = y * (Inv A)
thus x = x * (1_Rmatrix n) by A2, Th88
.= x * (A * (Inv A)) by A1, Def6
.= y * (Inv A) by A2, A5, A4, A6, Th57 ; ::_thesis: verum
end;
assume A7: x = y * (Inv A) ; ::_thesis: x * A = y
A8: width (Inv A) = n by MATRIX_1:24;
thus y = y * (1_Rmatrix n) by A3, Th88
.= y * ((Inv A) * A) by A1, Def6
.= x * A by A3, A4, A8, A7, Th57 ; ::_thesis: verum
end;
theorem :: MATRIXR2:90
for n being Element of NAT
for A being Matrix of n, REAL st n > 0 & A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y )
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st n > 0 & A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y )
let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & A is invertible implies for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) )
assume that
A1: n > 0 and
A2: A is invertible ; ::_thesis: for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y )
let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st
( len x = n & A * x = y ) )
assume A3: len y = n ; ::_thesis: ex x being FinSequence of REAL st
( len x = n & A * x = y )
reconsider x0 = (Inv A) * y as FinSequence of REAL ;
( len (Inv A) = n & width (Inv A) = n ) by MATRIX_1:24;
then A4: len x0 = n by A1, A3, MATRIXR1:61;
then A * x0 = y by A1, A2, A3, Th87;
hence ex x being FinSequence of REAL st
( len x = n & A * x = y ) by A4; ::_thesis: verum
end;
theorem :: MATRIXR2:91
for n being Element of NAT
for A being Matrix of n, REAL st A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )
let A be Matrix of n, REAL ; ::_thesis: ( A is invertible implies for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) )
assume A1: A is invertible ; ::_thesis: for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )
let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st
( len x = n & x * A = y ) )
assume A2: len y = n ; ::_thesis: ex x being FinSequence of REAL st
( len x = n & x * A = y )
reconsider x0 = y * (Inv A) as FinSequence of REAL ;
len (Inv A) = n by MATRIX_1:24;
then A3: len x0 = width (Inv A) by A2, MATRIXR1:62
.= n by MATRIX_1:24 ;
then x0 * A = y by A1, A2, Th89;
hence ex x being FinSequence of REAL st
( len x = n & x * A = y ) by A3; ::_thesis: verum
end;
theorem :: MATRIXR2:92
for n being Element of NAT
for A being Matrix of n, REAL
for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds
for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL
for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds
for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|
let A be Matrix of n, REAL ; ::_thesis: for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds
for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|
let x, y be FinSequence of REAL ; ::_thesis: ( len x = n & len y = n & x * A = y implies for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))| )
assume that
A1: len x = n and
A2: len y = n and
A3: x * A = y ; ::_thesis: for j being Element of NAT st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies y . j = |(x,(Col (A,j)))| )
assume ( 1 <= j & j <= n ) ; ::_thesis: y . j = |(x,(Col (A,j)))|
then j in Seg (len (x * A)) by A2, A3;
hence y . j = |(x,(Col (A,j)))| by A1, A3, MATRIX_1:24, MATRPROB:40; ::_thesis: verum
end;
theorem Th93: :: MATRIXR2:93
for n being Element of NAT
for A being Matrix of n, REAL st ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ) holds
ex B being Matrix of n, REAL st B * A = 1_Rmatrix n
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ) holds
ex B being Matrix of n, REAL st B * A = 1_Rmatrix n
let A be Matrix of n, REAL ; ::_thesis: ( ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ) implies ex B being Matrix of n, REAL st B * A = 1_Rmatrix n )
defpred S1[ set , set ] means for s being Element of NAT
for q being FinSequence of REAL st s = $1 & q = $2 holds
( len q = n & q * A = Base_FinSeq (n,s) );
assume A1: for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ; ::_thesis: ex B being Matrix of n, REAL st B * A = 1_Rmatrix n
A2: for i being Nat ex x being FinSequence of REAL st
( len x = n & x * A = Base_FinSeq (n,i) )
proof
let i be Nat; ::_thesis: ex x being FinSequence of REAL st
( len x = n & x * A = Base_FinSeq (n,i) )
len (Base_FinSeq (n,i)) = n by Th74;
hence ex x being FinSequence of REAL st
( len x = n & x * A = Base_FinSeq (n,i) ) by A1; ::_thesis: verum
end;
A3: for j being Nat st j in Seg n holds
ex d being Element of REAL * st S1[j,d]
proof
let j be Nat; ::_thesis: ( j in Seg n implies ex d being Element of REAL * st S1[j,d] )
assume j in Seg n ; ::_thesis: ex d being Element of REAL * st S1[j,d]
consider x being FinSequence of REAL such that
A4: ( len x = n & x * A = Base_FinSeq (n,j) ) by A2;
reconsider d0 = x as Element of REAL * by FINSEQ_1:def_11;
for s being Element of NAT
for q being FinSequence of REAL st s = j & q = d0 holds
( len q = n & q * A = Base_FinSeq (n,s) ) by A4;
hence ex d being Element of REAL * st S1[j,d] ; ::_thesis: verum
end;
consider f being FinSequence of REAL * such that
A5: ( len f = n & ( for j being Nat st j in Seg n holds
S1[j,f /. j] ) ) from FINSEQ_4:sch_1(A3);
for x being set st x in rng f holds
ex p being FinSequence of REAL st
( x = p & len p = n )
proof
let x be set ; ::_thesis: ( x in rng f implies ex p being FinSequence of REAL st
( x = p & len p = n ) )
assume x in rng f ; ::_thesis: ex p being FinSequence of REAL st
( x = p & len p = n )
then consider z being set such that
A6: z in dom f and
A7: f . z = x by FUNCT_1:def_3;
reconsider j0 = z as Element of NAT by A6;
reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def_11;
z in Seg (len f) by A6, FINSEQ_1:def_3;
then A8: len q0 = n by A5;
q0 = x by A6, A7, PARTFUN1:def_6;
hence ex p being FinSequence of REAL st
( x = p & len p = n ) by A8; ::_thesis: verum
end;
then reconsider M = f as Matrix of REAL by MATRIX_1:9;
for p being FinSequence of REAL st p in rng M holds
len p = n
proof
let p be FinSequence of REAL ; ::_thesis: ( p in rng M implies len p = n )
assume p in rng M ; ::_thesis: len p = n
then consider z being set such that
A9: z in dom f and
A10: M . z = p by FUNCT_1:def_3;
reconsider j0 = z as Element of NAT by A9;
reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def_11;
( z in Seg (len f) & q0 = p ) by A9, A10, FINSEQ_1:def_3, PARTFUN1:def_6;
hence len p = n by A5; ::_thesis: verum
end;
then reconsider B = M as Matrix of n, REAL by A5, MATRIX_1:def_2;
for i4, j4 being Nat st [i4,j4] in Indices (B * A) holds
(B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4)
proof
let i4, j4 be Nat; ::_thesis: ( [i4,j4] in Indices (B * A) implies (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4) )
reconsider i = i4, j = j4 as Element of NAT by ORDINAL1:def_12;
consider n2 being Nat such that
A11: for x being set st x in rng (M * A) holds
ex p being FinSequence of REAL st
( x = p & len p = n2 ) by MATRIX_1:9;
assume A12: [i4,j4] in Indices (B * A) ; ::_thesis: (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4)
then j in Seg (width (M * A)) by ZFMISC_1:87;
then A13: ( 1 <= j & j <= width (M * A) ) by FINSEQ_1:1;
i in dom (M * A) by A12, ZFMISC_1:87;
then A14: (M * A) . i in rng (M * A) by FUNCT_1:def_3;
then consider p2 being FinSequence of REAL such that
A15: (M * A) . i = p2 and
A16: len p2 = n2 by A11;
A17: len B = n by MATRIX_1:24;
A18: [i,j] in [:(Seg n),(Seg n):] by A12, MATRIX_1:24;
then [i,j] in Indices (1_Rmatrix n) by MATRIX_1:24;
then A19: ex p3 being FinSequence of REAL st
( p3 = (1_Rmatrix n) . i & (1_Rmatrix n) * (i,j) = p3 . j ) by MATRIX_1:def_5;
A20: width (B * A) = n by MATRIX_1:24;
j in Seg n by A18, ZFMISC_1:87;
then A21: ( 1 <= j & j <= n ) by FINSEQ_1:1;
A22: i in Seg n by A18, ZFMISC_1:87;
then A23: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A24: ( len (B * A) = n & ( for p being FinSequence of REAL st p in rng (B * A) holds
len p = n ) ) by MATRIX_1:def_2;
now__::_thesis:_(_(_i_=_j_&_(1_Rmatrix_n)_*_(i,j)_=_p2_._j_)_or_(_i_<>_j_&_(1_Rmatrix_n)_*_(i,j)_=_p2_._j_)_)
percases ( i = j or i <> j ) ;
caseA25: i = j ; ::_thesis: (1_Rmatrix n) * (i,j) = p2 . j
reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def_11;
A26: g * A = Base_FinSeq (n,i) by A5, A22;
len B = n by MATRIX_1:24;
then f /. i = M . i by A23, FINSEQ_4:15;
then A27: g = Line (B,i) by A23, A17, Lm2;
A28: (1_Rmatrix n) * (i,j) = (Base_FinSeq (n,i)) . i by A19, A23, A25, Th78
.= 1 by A23, Th75 ;
p2 . j = (B * A) * (i,j) by A24, A14, A15, A16, A13, A23, A20, Th2
.= (Base_FinSeq (n,i)) . j by A12, A26, A27, Th61
.= 1 by A23, A25, Th75 ;
hence (1_Rmatrix n) * (i,j) = p2 . j by A28; ::_thesis: verum
end;
caseA29: i <> j ; ::_thesis: (1_Rmatrix n) * (i,j) = p2 . j
reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def_11;
len B = n by MATRIX_1:24;
then f /. i = M . i by A23, FINSEQ_4:15;
then g = Line (B,i) by A23, A17, Lm2;
then A30: (Line (B,i)) * A = Base_FinSeq (n,i) by A5, A22;
A31: (1_Rmatrix n) * (i,j) = (Base_FinSeq (n,i)) . j by A19, A23, Th78
.= 0 by A21, A29, Th76 ;
p2 . j = (B * A) * (i,j) by A24, A14, A15, A16, A13, A23, A20, Th2
.= (Base_FinSeq (n,i)) . j by A12, A30, Th61
.= 0 by A21, A29, Th76 ;
hence (1_Rmatrix n) * (i,j) = p2 . j by A31; ::_thesis: verum
end;
end;
end;
hence (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4) by A12, A15, MATRIX_1:def_5; ::_thesis: verum
end;
hence ex B being Matrix of n, REAL st B * A = 1_Rmatrix n by MATRIX_1:27; ::_thesis: verum
end;
theorem :: MATRIXR2:94
for n being Element of NAT
for x being FinSequence of REAL
for A being Matrix of n, REAL st n > 0 & len x = n holds
(A @) * x = x * A
proof
let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL
for A being Matrix of n, REAL st n > 0 & len x = n holds
(A @) * x = x * A
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st n > 0 & len x = n holds
(A @) * x = x * A
let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & len x = n implies (A @) * x = x * A )
A1: ( len A = n & width A = n ) by MATRIX_1:24;
assume ( n > 0 & len x = n ) ; ::_thesis: (A @) * x = x * A
hence (A @) * x = x * A by A1, MATRIXR1:52; ::_thesis: verum
end;
theorem Th95: :: MATRIXR2:95
for n being Element of NAT
for x being FinSequence of REAL
for A being Matrix of n, REAL st n > 0 & len x = n holds
x * (A @) = A * x
proof
let n be Element of NAT ; ::_thesis: for x being FinSequence of REAL
for A being Matrix of n, REAL st n > 0 & len x = n holds
x * (A @) = A * x
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of n, REAL st n > 0 & len x = n holds
x * (A @) = A * x
let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & len x = n implies x * (A @) = A * x )
A1: ( len A = n & width A = n ) by MATRIX_1:24;
assume ( n > 0 & len x = n ) ; ::_thesis: x * (A @) = A * x
hence x * (A @) = A * x by A1, MATRIXR1:53; ::_thesis: verum
end;
theorem Th96: :: MATRIXR2:96
for n being Element of NAT
for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ) holds
ex B being Matrix of n, REAL st A * B = 1_Rmatrix n
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ) holds
ex B being Matrix of n, REAL st A * B = 1_Rmatrix n
let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ) implies ex B being Matrix of n, REAL st A * B = 1_Rmatrix n )
assume that
A1: n > 0 and
A2: for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ; ::_thesis: ex B being Matrix of n, REAL st A * B = 1_Rmatrix n
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * (A @) = y )
proof
let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st
( len x = n & x * (A @) = y ) )
assume len y = n ; ::_thesis: ex x being FinSequence of REAL st
( len x = n & x * (A @) = y )
then consider x0 being FinSequence of REAL such that
A3: len x0 = n and
A4: A * x0 = y by A2;
x0 * (A @) = A * x0 by A1, A3, Th95;
hence ex x being FinSequence of REAL st
( len x = n & x * (A @) = y ) by A3, A4; ::_thesis: verum
end;
then consider B being Matrix of n, REAL such that
A5: B * (A @) = 1_Rmatrix n by Th93;
(B * (A @)) @ = 1_Rmatrix n by A5, Th64;
then ((A @) @) * (B @) = 1_Rmatrix n by Th30;
then A * (B @) = 1_Rmatrix n by Th29;
hence ex B being Matrix of n, REAL st A * B = 1_Rmatrix n ; ::_thesis: verum
end;
theorem :: MATRIXR2:97
for n being Element of NAT
for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds
A is invertible
proof
let n be Element of NAT ; ::_thesis: for A being Matrix of n, REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds
A is invertible
let A be Matrix of n, REAL ; ::_thesis: ( n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) implies A is invertible )
assume that
A1: n > 0 and
A2: for y being FinSequence of REAL st len y = n holds
ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ; ::_thesis: A is invertible
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )
proof
let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st
( len x = n & x * A = y ) )
assume len y = n ; ::_thesis: ex x being FinSequence of REAL st
( len x = n & x * A = y )
then ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A2;
hence ex x being FinSequence of REAL st
( len x = n & x * A = y ) ; ::_thesis: verum
end;
then A3: ex B1 being Matrix of n, REAL st B1 * A = 1_Rmatrix n by Th93;
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y )
proof
let y be FinSequence of REAL ; ::_thesis: ( len y = n implies ex x being FinSequence of REAL st
( len x = n & A * x = y ) )
assume len y = n ; ::_thesis: ex x being FinSequence of REAL st
( len x = n & A * x = y )
then ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A2;
hence ex x being FinSequence of REAL st
( len x = n & A * x = y ) ; ::_thesis: verum
end;
then ex B2 being Matrix of n, REAL st A * B2 = 1_Rmatrix n by A1, Th96;
hence A is invertible by A3, Th80; ::_thesis: verum
end;