:: MATRIXR1 semantic presentation
begin
theorem :: MATRIXR1:1
for r1, r2 being Real
for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds
r1 + r2 = fr1 + fr2 ;
theorem :: MATRIXR1:2
for r1, r2 being Real
for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds
r1 * r2 = fr1 * fr2 ;
theorem Th3: :: MATRIXR1:3
for F being FinSequence of REAL holds
( F + (- F) = 0* (len F) & F - F = 0* (len F) )
proof
let F be FinSequence of REAL ; ::_thesis: ( F + (- F) = 0* (len F) & F - F = 0* (len F) )
set n = len F;
reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: R + (- R) = (len F) |-> 0 by RVSUM_1:22;
hence F + (- F) = 0* (len F) by EUCLID:def_4; ::_thesis: F - F = 0* (len F)
thus F - F = 0* (len F) by A1, EUCLID:def_4; ::_thesis: verum
end;
theorem :: MATRIXR1:4
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 - F2 = F1 + (- F2) ;
theorem :: MATRIXR1:5
for F being FinSequence of REAL holds F - (0* (len F)) = F
proof
let F be FinSequence of REAL ; ::_thesis: F - (0* (len F)) = F
set n = len F;
reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
R - ((len F) |-> 0) = R by RVSUM_1:32;
hence F - (0* (len F)) = F by EUCLID:def_4; ::_thesis: verum
end;
theorem :: MATRIXR1:6
for F being FinSequence of REAL holds (0* (len F)) - F = - F
proof
let F be FinSequence of REAL ; ::_thesis: (0* (len F)) - F = - F
set n = len F;
reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
((len F) |-> 0) - R = - R by RVSUM_1:33;
hence (0* (len F)) - F = - F by EUCLID:def_4; ::_thesis: verum
end;
theorem :: MATRIXR1:7
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 - (- F2) = F1 + F2 ;
theorem :: MATRIXR1:8
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
- (F1 - F2) = F2 - F1 by RVSUM_1:35;
theorem :: MATRIXR1:9
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
- (F1 - F2) = (- F1) + F2 by RVSUM_1:36;
theorem :: MATRIXR1:10
for F1, F2 being FinSequence of REAL st len F1 = len F2 & F1 - F2 = 0* (len F1) holds
F1 = F2
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 & F1 - F2 = 0* (len F1) implies F1 = F2 )
set n = len F1;
assume len F1 = len F2 ; ::_thesis: ( not F1 - F2 = 0* (len F1) or F1 = F2 )
then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
( R1 - R2 = (len F1) |-> 0 implies R1 = R2 ) by RVSUM_1:38;
hence ( not F1 - F2 = 0* (len F1) or F1 = F2 ) by EUCLID:def_4; ::_thesis: verum
end;
theorem :: MATRIXR1:11
for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds
(F1 - F2) - F3 = F1 - (F2 + F3) by RVSUM_1:39;
theorem :: MATRIXR1:12
for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds
F1 + (F2 - F3) = (F1 + F2) - F3 by RVSUM_1:40;
theorem :: MATRIXR1:13
for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds
F1 - (F2 - F3) = (F1 - F2) + F3 by RVSUM_1:41;
theorem Th14: :: MATRIXR1:14
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 = (F1 + F2) - F2
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies F1 = (F1 + F2) - F2 )
set n = len F1;
assume len F1 = len F2 ; ::_thesis: F1 = (F1 + F2) - F2
then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
R1 = (R1 + R2) - R2 by RVSUM_1:42;
hence F1 = (F1 + F2) - F2 ; ::_thesis: verum
end;
theorem :: MATRIXR1:15
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 = (F1 - F2) + F2
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies F1 = (F1 - F2) + F2 )
set n = len F1;
assume len F1 = len F2 ; ::_thesis: F1 = (F1 - F2) + F2
then reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
R1 = (R1 - R2) + R2 by RVSUM_1:43;
hence F1 = (F1 - F2) + F2 ; ::_thesis: verum
end;
begin
theorem Th16: :: MATRIXR1:16
for K being non empty multMagma
for p being FinSequence of K
for a being Element of K holds len (a * p) = len p
proof
let K be non empty multMagma ; ::_thesis: for p being FinSequence of K
for a being Element of K holds len (a * p) = len p
let p be FinSequence of K; ::_thesis: for a being Element of K holds len (a * p) = len p
let a be Element of K; ::_thesis: len (a * p) = len p
reconsider q = p as Element of (len p) -tuples_on the carrier of K by FINSEQ_2:92;
a * q in (len p) -tuples_on the carrier of K ;
then a * q in { s where s is Element of the carrier of K * : len s = len p } by FINSEQ_2:def_4;
then ex s being Element of the carrier of K * st
( a * q = s & len s = len p ) ;
hence len (a * p) = len p ; ::_thesis: verum
end;
theorem Th17: :: MATRIXR1:17
for r being Real
for fr being Element of F_Real
for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
proof
let r be Real; ::_thesis: for fr being Element of F_Real
for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let fr be Element of F_Real; ::_thesis: for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let p be FinSequence of REAL ; ::_thesis: for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp
let fp be FinSequence of F_Real; ::_thesis: ( r = fr & p = fp implies r * p = fr * fp )
assume that
A1: r = fr and
A2: p = fp ; ::_thesis: r * p = fr * fp
A3: len (r * p) = len fp by A2, RVSUM_1:117;
then A4: len (r * p) = len (fr * fp) by Th16;
for i being Nat st 1 <= i & i <= len (r * p) holds
(r * p) . i = (fr * fp) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (r * p) implies (r * p) . i = (fr * fp) . i )
assume ( 1 <= i & i <= len (r * p) ) ; ::_thesis: (r * p) . i = (fr * fp) . i
then i in Seg (len fp) by A3, FINSEQ_1:1;
then A5: i in dom (fr * fp) by A3, A4, FINSEQ_1:def_3;
reconsider s = fp . i as Element of F_Real ;
thus (r * p) . i = fr * s by A1, A2, RVSUM_1:44
.= (fr * fp) . i by A5, FVSUM_1:50 ; ::_thesis: verum
end;
hence r * p = fr * fp by A4, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: MATRIXR1:18
for K being Field
for a being Element of K
for A being Matrix of K holds Indices (a * A) = Indices A
proof
let K be Field; ::_thesis: for a being Element of K
for A being Matrix of K holds Indices (a * A) = Indices A
let a be Element of K; ::_thesis: for A being Matrix of K holds Indices (a * A) = Indices A
let A be Matrix of K; ::_thesis: Indices (a * A) = Indices A
( len (a * A) = len A & width (a * A) = width A ) by MATRIX_3:def_5;
hence Indices (a * A) = Indices A by FINSEQ_3:29; ::_thesis: verum
end;
theorem Th19: :: MATRIXR1:19
for i being Nat
for K being Field
for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
proof
let i be Nat; ::_thesis: for K being Field
for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let K be Field; ::_thesis: for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let a be Element of K; ::_thesis: for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let M be Matrix of K; ::_thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )
assume A1: ( 1 <= i & i <= width M ) ; ::_thesis: Col ((a * M),i) = a * (Col (M,i))
A2: Seg (len (a * M)) = dom (a * M) by FINSEQ_1:def_3;
A3: len (a * M) = len M by MATRIX_3:def_5;
then A4: dom M = dom (a * M) by FINSEQ_3:29;
A5: ( len (a * (Col (M,i))) = len (Col (M,i)) & len (Col (M,i)) = len M ) by Th16, MATRIX_1:def_8;
then A6: dom (a * (Col (M,i))) = Seg (len (a * M)) by A3, FINSEQ_1:def_3;
for j being Nat st j in dom (a * M) holds
(a * (Col (M,i))) . j = (a * M) * (j,i)
proof
let j be Nat; ::_thesis: ( j in dom (a * M) implies (a * (Col (M,i))) . j = (a * M) * (j,i) )
assume A7: j in dom (a * M) ; ::_thesis: (a * (Col (M,i))) . j = (a * M) * (j,i)
i in Seg (width M) by A1, FINSEQ_1:1;
then [j,i] in Indices M by A4, A7, ZFMISC_1:87;
then A8: (a * M) * (j,i) = a * (M * (j,i)) by MATRIX_3:def_5;
(Col (M,i)) . j = M * (j,i) by A4, A7, MATRIX_1:def_8;
hence (a * (Col (M,i))) . j = (a * M) * (j,i) by A6, A2, A7, A8, FVSUM_1:50; ::_thesis: verum
end;
hence Col ((a * M),i) = a * (Col (M,i)) by A5, A3, MATRIX_1:def_8; ::_thesis: verum
end;
theorem :: MATRIXR1:20
for K being Field
for a being Element of K
for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
proof
let K be Field; ::_thesis: for a being Element of K
for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
let a be Element of K; ::_thesis: for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
let M be Matrix of K; ::_thesis: for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))
let i be Nat; ::_thesis: ( 1 <= i & i <= len M implies Line ((a * M),i) = a * (Line (M,i)) )
assume A1: ( 1 <= i & i <= len M ) ; ::_thesis: Line ((a * M),i) = a * (Line (M,i))
A2: width (a * M) = width M by MATRIX_3:def_5;
A3: Seg (width M) = Seg (width (a * M)) by MATRIX_3:def_5;
A4: ( len (a * (Line (M,i))) = len (Line (M,i)) & len (Line (M,i)) = width M ) by Th16, MATRIX_1:def_7;
then A5: dom (a * (Line (M,i))) = Seg (width (a * M)) by A2, FINSEQ_1:def_3;
for j being Nat st j in Seg (width (a * M)) holds
(a * (Line (M,i))) . j = (a * M) * (i,j)
proof
let j be Nat; ::_thesis: ( j in Seg (width (a * M)) implies (a * (Line (M,i))) . j = (a * M) * (i,j) )
assume A6: j in Seg (width (a * M)) ; ::_thesis: (a * (Line (M,i))) . j = (a * M) * (i,j)
i in dom M by A1, FINSEQ_3:25;
then [i,j] in Indices M by A3, A6, ZFMISC_1:87;
then A7: (a * M) * (i,j) = a * (M * (i,j)) by MATRIX_3:def_5;
(Line (M,i)) . j = M * (i,j) by A3, A6, MATRIX_1:def_7;
hence (a * (Line (M,i))) . j = (a * M) * (i,j) by A5, A6, A7, FVSUM_1:50; ::_thesis: verum
end;
hence Line ((a * M),i) = a * (Line (M,i)) by A4, A2, MATRIX_1:def_7; ::_thesis: verum
end;
theorem :: MATRIXR1:21
for K being Field
for A, B being Matrix of K st width A = len B holds
ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
proof
let K be Field; ::_thesis: for A, B being Matrix of K st width A = len B holds
ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
let A, B be Matrix of K; ::_thesis: ( width A = len B implies ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) )
assume A1: width A = len B ; ::_thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
deffunc H1( Nat, Nat) -> Element of the carrier of K = (Line (A,$1)) "*" (Col (B,$2));
consider M being Matrix of len A, width B, the carrier of K such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = H1(i,j) from MATRIX_1:sch_1();
percases ( len A > 0 or len A = 0 ) ;
suppose len A > 0 ; ::_thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
then ( len M = len A & width M = width B ) by MATRIX_1:23;
hence ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) by A2; ::_thesis: verum
end;
supposeA3: len A = 0 ; ::_thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) )
then A4: len M = 0 by MATRIX_1:25;
len B = 0 by A1, A3, MATRIX_1:def_3;
then width B = 0 by MATRIX_1:def_3;
then width M = width B by A4, MATRIX_1:def_3;
hence ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * (i,j) = (Line (A,i)) "*" (Col (B,j)) ) ) by A2, A3, A4; ::_thesis: verum
end;
end;
end;
theorem Th22: :: MATRIXR1:22
for K being Field
for a being Element of K
for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
proof
let K be Field; ::_thesis: for a being Element of K
for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
let a be Element of K; ::_thesis: for A, B being Matrix of K st width A = len B holds
A * (a * B) = a * (A * B)
let A, B be Matrix of K; ::_thesis: ( width A = len B implies A * (a * B) = a * (A * B) )
set C = a * B;
set D = a * (A * B);
A1: len (a * (A * B)) = len (A * B) by MATRIX_3:def_5;
assume A2: width A = len B ; ::_thesis: A * (a * B) = a * (A * B)
then width (A * B) = width B by MATRIX_3:def_4;
then A3: width (a * (A * B)) = width B by MATRIX_3:def_5
.= width (a * B) by MATRIX_3:def_5 ;
A4: width B = width (a * B) by MATRIX_3:def_5;
A5: for i, j being Nat st [i,j] in Indices (a * (A * B)) holds
(a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j))
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (A * B)) implies (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) )
reconsider xo = Col (B,j) as Element of (width A) -tuples_on the carrier of K by A2;
assume A6: [i,j] in Indices (a * (A * B)) ; ::_thesis: (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j))
then j in Seg (width B) by A4, A3, ZFMISC_1:87;
then A7: ( 1 <= j & j <= width B ) by FINSEQ_1:1;
dom (A * B) = dom (a * (A * B)) by A1, FINSEQ_3:29;
then A8: [i,j] in Indices (A * B) by A6, MATRIX_3:def_5;
then (a * (A * B)) * (i,j) = a * ((A * B) * (i,j)) by MATRIX_3:def_5;
then (a * (A * B)) * (i,j) = a * ((Line (A,i)) "*" (Col (B,j))) by A2, A8, MATRIX_3:def_4
.= a * (Sum (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:def_9
.= Sum (a * (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:73
.= Sum (mlt ((Line (A,i)),(a * xo))) by FVSUM_1:69
.= Sum (mlt ((Line (A,i)),(Col ((a * B),j)))) by A7, Th19 ;
hence (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) by FVSUM_1:def_9; ::_thesis: verum
end;
( len (a * B) = len B & len (A * B) = len A ) by A2, MATRIX_3:def_4, MATRIX_3:def_5;
hence A * (a * B) = a * (A * B) by A2, A1, A3, A5, MATRIX_3:def_4; ::_thesis: verum
end;
definition
let A be Matrix of REAL;
func MXR2MXF A -> Matrix of F_Real equals :: MATRIXR1:def 1
A;
coherence
A is Matrix of F_Real ;
end;
:: deftheorem defines MXR2MXF MATRIXR1:def_1_:_
for A being Matrix of REAL holds MXR2MXF A = A;
definition
let A be Matrix of F_Real;
func MXF2MXR A -> Matrix of REAL equals :: MATRIXR1:def 2
A;
coherence
A is Matrix of REAL ;
end;
:: deftheorem defines MXF2MXR MATRIXR1:def_2_:_
for A being Matrix of F_Real holds MXF2MXR A = A;
theorem :: MATRIXR1:23
for D1, D2 being set
for A being Matrix of D1
for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
proof
let D1, D2 be set ; ::_thesis: for A being Matrix of D1
for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
let A be Matrix of D1; ::_thesis: for B being Matrix of D2 st A = B holds
for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
let B be Matrix of D2; ::_thesis: ( A = B implies for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j) )
assume A1: A = B ; ::_thesis: for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = B * (i,j)
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies A * (i,j) = B * (i,j) )
assume A2: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j)
then A3: ex p being FinSequence of D1 st
( p = A . i & A * (i,j) = p . j ) by MATRIX_1:def_5;
ex q being FinSequence of D2 st
( q = B . i & B * (i,j) = q . j ) by A1, A2, MATRIX_1:def_5;
hence A * (i,j) = B * (i,j) by A1, A3; ::_thesis: verum
end;
theorem :: MATRIXR1:24
for K being Field
for A, B being Matrix of K holds Indices (A + B) = Indices A
proof
let K be Field; ::_thesis: for A, B being Matrix of K holds Indices (A + B) = Indices A
let A, B be Matrix of K; ::_thesis: Indices (A + B) = Indices A
( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def_3;
hence Indices (A + B) = Indices A by MATRIX_4:55; ::_thesis: verum
end;
definition
let A, B be Matrix of REAL;
funcA + B -> Matrix of REAL equals :: MATRIXR1:def 3
MXF2MXR ((MXR2MXF A) + (MXR2MXF B));
coherence
MXF2MXR ((MXR2MXF A) + (MXR2MXF B)) is Matrix of REAL ;
end;
:: deftheorem defines + MATRIXR1:def_3_:_
for A, B being Matrix of REAL holds A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF B));
theorem Th25: :: MATRIXR1:25
for A, B being Matrix of REAL holds
( len (A + B) = len A & width (A + B) = width A & ( for i, j being 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 + B) = len A & width (A + B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ) )
thus ( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def_3; ::_thesis: for i, j being Nat st [i,j] in Indices A holds
(A + B) * (i,j) = (A * (i,j)) + (B * (i,j))
let i, j be Nat; ::_thesis: ( [i,j] in Indices A implies (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) )
assume [i,j] in Indices A ; ::_thesis: (A + B) * (i,j) = (A * (i,j)) + (B * (i,j))
then (A + B) * (i,j) = ((MXR2MXF A) * (i,j)) + ((MXR2MXF B) * (i,j)) by MATRIX_3:def_3;
hence (A + B) * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: verum
end;
theorem Th26: :: MATRIXR1:26
for A, B, C being Matrix of REAL st len C = len A & width C = width A & ( for i, j being 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 C = len A & width C = width A & ( for i, j being 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 C = len A & width C = width A ) and
A2: for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) + (B * (i,j)) ; ::_thesis: C = A + B
set B2 = MXR2MXF B;
set A2 = MXR2MXF A;
set D = MXR2MXF C;
for i, j being Nat st [i,j] in Indices (MXR2MXF A) holds
(MXR2MXF C) * (i,j) = ((MXR2MXF A) * (i,j)) + ((MXR2MXF B) * (i,j)) by A2;
hence C = A + B by A1, MATRIX_3:def_3; ::_thesis: verum
end;
definition
let A be Matrix of REAL;
func - A -> Matrix of REAL equals :: MATRIXR1:def 4
MXF2MXR (- (MXR2MXF A));
coherence
MXF2MXR (- (MXR2MXF A)) is Matrix of REAL ;
end;
:: deftheorem defines - MATRIXR1:def_4_:_
for A being Matrix of REAL holds - A = MXF2MXR (- (MXR2MXF A));
definition
let A, B be Matrix of REAL;
funcA - B -> Matrix of REAL equals :: MATRIXR1:def 5
MXF2MXR ((MXR2MXF A) - (MXR2MXF B));
coherence
MXF2MXR ((MXR2MXF A) - (MXR2MXF B)) is Matrix of REAL ;
funcA * B -> Matrix of REAL equals :: MATRIXR1:def 6
MXF2MXR ((MXR2MXF A) * (MXR2MXF B));
coherence
MXF2MXR ((MXR2MXF A) * (MXR2MXF B)) is Matrix of REAL ;
end;
:: deftheorem defines - MATRIXR1:def_5_:_
for A, B being Matrix of REAL holds A - B = MXF2MXR ((MXR2MXF A) - (MXR2MXF B));
:: deftheorem defines * MATRIXR1:def_6_:_
for A, B being Matrix of REAL holds A * B = MXF2MXR ((MXR2MXF A) * (MXR2MXF B));
definition
let a be real number ;
let A be Matrix of REAL;
funca * A -> Matrix of REAL means :Def7: :: MATRIXR1:def 7
for ea being Element of F_Real st ea = a holds
it = MXF2MXR (ea * (MXR2MXF A));
existence
ex b1 being Matrix of REAL st
for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A))
proof
reconsider aa = a as Element of F_Real by XREAL_0:def_1;
set C = MXF2MXR (aa * (MXR2MXF A));
for ea being Element of F_Real st ea = a holds
MXF2MXR (aa * (MXR2MXF A)) = MXF2MXR (ea * (MXR2MXF A)) ;
hence ex b1 being Matrix of REAL st
for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A)) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of REAL st ( for ea being Element of F_Real st ea = a holds
b1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
b2 = MXF2MXR (ea * (MXR2MXF A)) ) holds
b1 = b2
proof
reconsider aa = a as Element of F_Real by XREAL_0:def_1;
let C1, C2 be Matrix of REAL; ::_thesis: ( ( for ea being Element of F_Real st ea = a holds
C1 = MXF2MXR (ea * (MXR2MXF A)) ) & ( for ea being Element of F_Real st ea = a holds
C2 = MXF2MXR (ea * (MXR2MXF A)) ) implies C1 = C2 )
assume that
A1: for ea being Element of F_Real st ea = a holds
C1 = MXF2MXR (ea * (MXR2MXF A)) and
A2: for ea being Element of F_Real st ea = a holds
C2 = MXF2MXR (ea * (MXR2MXF A)) ; ::_thesis: C1 = C2
C2 = MXF2MXR (aa * (MXR2MXF A)) by A2;
hence C1 = C2 by A1; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines * MATRIXR1:def_7_:_
for a being real number
for A, b3 being Matrix of REAL holds
( b3 = a * A iff for ea being Element of F_Real st ea = a holds
b3 = MXF2MXR (ea * (MXR2MXF A)) );
theorem Th27: :: MATRIXR1:27
for a being Real
for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )
proof
let a be Real; ::_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 ;
thus len (a * A) = len (MXF2MXR (ea * (MXR2MXF A))) by Def7
.= len A by MATRIX_3:def_5 ; ::_thesis: width (a * A) = width A
thus width (a * A) = width (MXF2MXR (ea * (MXR2MXF A))) by Def7
.= width A by MATRIX_3:def_5 ; ::_thesis: verum
end;
theorem Th28: :: MATRIXR1:28
for a being Real
for A being Matrix of REAL holds Indices (a * A) = Indices A
proof
let a be Real; ::_thesis: for A being Matrix of REAL holds Indices (a * A) = Indices A
let A be Matrix of REAL; ::_thesis: Indices (a * A) = Indices A
( len A = len (a * A) & width (a * A) = width A ) by Th27;
hence Indices (a * A) = Indices A by MATRIX_4:55; ::_thesis: verum
end;
theorem Th29: :: MATRIXR1:29
for a being Real
for A being Matrix of REAL
for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * (i2,j2) = a * (A * (i2,j2))
proof
let a be Real; ::_thesis: for A being Matrix of REAL
for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * (i2,j2) = a * (A * (i2,j2))
let A be Matrix of REAL; ::_thesis: for i2, j2 being Nat st [i2,j2] in Indices A holds
(a * A) * (i2,j2) = a * (A * (i2,j2))
let i2, j2 be Nat; ::_thesis: ( [i2,j2] in Indices A implies (a * A) * (i2,j2) = a * (A * (i2,j2)) )
reconsider ea = a as Element of F_Real ;
assume [i2,j2] in Indices A ; ::_thesis: (a * A) * (i2,j2) = a * (A * (i2,j2))
then (MXF2MXR (ea * (MXR2MXF A))) * (i2,j2) = ea * ((MXR2MXF A) * (i2,j2)) by MATRIX_3:def_5
.= a * (A * (i2,j2)) ;
hence (a * A) * (i2,j2) = a * (A * (i2,j2)) by Def7; ::_thesis: verum
end;
theorem Th30: :: MATRIXR1:30
for a being Real
for A being Matrix of REAL st width A > 0 holds
(a * A) @ = a * (A @)
proof
let a be Real; ::_thesis: for A being Matrix of REAL st width A > 0 holds
(a * A) @ = a * (A @)
let A be Matrix of REAL; ::_thesis: ( width A > 0 implies (a * A) @ = a * (A @) )
assume width A > 0 ; ::_thesis: (a * A) @ = a * (A @)
then A1: len (A @) = width A by MATRIX_2:10;
A2: for i, j being Nat holds
( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) )
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) )
( Indices (a * (A @)) = Indices (A @) & Indices (a * A) = Indices A ) by Th28;
hence ( [i,j] in Indices (a * (A @)) iff [j,i] in Indices (a * A) ) by MATRIX_1:def_6; ::_thesis: verum
end;
A3: for i, j being Nat st [j,i] in Indices (a * A) holds
(a * (A @)) * (i,j) = (a * A) * (j,i)
proof
let i, j be Nat; ::_thesis: ( [j,i] in Indices (a * A) implies (a * (A @)) * (i,j) = (a * A) * (j,i) )
assume [j,i] in Indices (a * A) ; ::_thesis: (a * (A @)) * (i,j) = (a * A) * (j,i)
then A4: [j,i] in Indices A by Th28;
then [i,j] in Indices (A @) by MATRIX_1:def_6;
then (a * (A @)) * (i,j) = a * ((A @) * (i,j)) by Th29;
then (a * (A @)) * (i,j) = a * (A * (j,i)) by A4, MATRIX_1:def_6
.= (a * A) * (j,i) by A4, Th29 ;
hence (a * (A @)) * (i,j) = (a * A) * (j,i) ; ::_thesis: verum
end;
( len (a * (A @)) = len (A @) & width A = width (a * A) ) by Th27;
hence (a * A) @ = a * (A @) by A1, A2, A3, MATRIX_1:def_6; ::_thesis: verum
end;
theorem :: MATRIXR1:31
for a being Real
for i being Nat
for A being Matrix of REAL st len A > 0 & i in dom A holds
( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
proof
let a be Real; ::_thesis: for i being Nat
for A being Matrix of REAL st len A > 0 & i in dom A holds
( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
let i be Nat; ::_thesis: for A being Matrix of REAL st len A > 0 & i in dom A holds
( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
let A be Matrix of REAL; ::_thesis: ( len A > 0 & i in dom A implies ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) ) )
assume that
A1: len A > 0 and
A2: i in dom A ; ::_thesis: ( ex p being FinSequence of REAL st p = A . i & ( for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q ) )
consider n3 being Nat such that
A3: for x being set st x in rng A holds
ex s2 being FinSequence st
( s2 = x & len s2 = n3 ) by MATRIX_1:def_1;
A . i in rng A by A2, FUNCT_1:def_3;
then A4: ex qq0 being FinSequence st
( qq0 = A . i & len qq0 = n3 ) by A3;
len (a * A) = len A by Th27;
then consider s being FinSequence such that
A5: s in rng (a * A) and
A6: len s = width (a * A) by A1, MATRIX_1:def_3;
A7: width (a * A) = width A by Th27;
consider s3 being FinSequence such that
A8: s3 in rng A and
A9: len s3 = width A by A1, MATRIX_1:def_3;
consider n2 being Nat such that
A10: for x being set st x in rng (a * A) holds
ex s2 being FinSequence st
( s2 = x & len s2 = n2 ) by MATRIX_1:def_1;
len (a * A) = len A by Th27;
then A11: dom (a * A) = dom A by FINSEQ_3:29;
then (a * A) . i in rng (a * A) by A2, FUNCT_1:def_3;
then consider qq being FinSequence such that
A12: qq = (a * A) . i and
A13: len qq = n2 by A10;
consider n being Nat such that
A14: for x being set st x in rng A holds
ex p being FinSequence of REAL st
( x = p & len p = n ) by MATRIX_1:9;
A . i in rng A by A2, FUNCT_1:def_3;
then ex p2 being FinSequence of REAL st
( A . i = p2 & len p2 = n ) by A14;
hence ex p being FinSequence of REAL st p = A . i ; ::_thesis: for q being FinSequence of REAL st q = A . i holds
(a * A) . i = a * q
let q be FinSequence of REAL ; ::_thesis: ( q = A . i implies (a * A) . i = a * q )
assume A15: q = A . i ; ::_thesis: (a * A) . i = a * q
A16: ex s4 being FinSequence st
( s4 = s3 & len s4 = n3 ) by A8, A3;
then A17: len (a * q) = width A by A15, A9, A4, RVSUM_1:117;
A18: for j being Nat st 1 <= j & j <= len (a * q) holds
qq . j = (a * q) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len (a * q) implies qq . j = (a * q) . j )
assume ( 1 <= j & j <= len (a * q) ) ; ::_thesis: qq . j = (a * q) . j
then A19: j in Seg (width A) by A17, FINSEQ_1:1;
then A20: [i,j] in Indices A by A2, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
[i,j] in Indices (a * A) by A2, A7, A11, A19, ZFMISC_1:87;
then A21: ex p being FinSequence of REAL st
( p = (a * A) . i & (a * A) * (i,j) = p . j ) by MATRIX_1:def_5;
ex p2 being FinSequence of REAL st
( p2 = A . i & A * (i,j) = p2 . j ) by A20, MATRIX_1:def_5;
then qq . j = a * (q . j) by A15, A12, A20, A21, Th29;
hence qq . j = (a * q) . j by RVSUM_1:44; ::_thesis: verum
end;
ex s2 being FinSequence st
( s2 = s & len s2 = n2 ) by A5, A10;
then width A = len qq by A6, A13, Th27;
hence (a * A) . i = a * q by A15, A9, A16, A12, A4, A18, FINSEQ_1:14, RVSUM_1:117; ::_thesis: verum
end;
theorem :: MATRIXR1:32
for A being Matrix of REAL holds 1 * A = A
proof
let A be Matrix of REAL; ::_thesis: 1 * A = A
1 * A = MXF2MXR ((1_ F_Real) * (MXR2MXF A)) by Def7;
hence 1 * A = A by MATRIX_5:9; ::_thesis: verum
end;
theorem :: MATRIXR1:33
for A being Matrix of REAL holds A + A = 2 * A
proof
set e2 = (1_ F_Real) + (1_ F_Real);
let A be Matrix of REAL; ::_thesis: A + A = 2 * A
A1: (1_ F_Real) * (MXR2MXF A) = MXR2MXF A by MATRIX_5:9;
2 * A = MXF2MXR (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A)) by Def7
.= MXF2MXR ((MXR2MXF A) + (MXR2MXF A)) by A1, MATRIX_5:12 ;
hence A + A = 2 * A ; ::_thesis: verum
end;
theorem :: MATRIXR1:34
for A being Matrix of REAL holds (A + A) + A = 3 * A
proof
reconsider e3 = ((1_ F_Real) + (1_ F_Real)) + (1_ F_Real) as Element of F_Real ;
let A be Matrix of REAL; ::_thesis: (A + A) + A = 3 * A
A1: ( len A = len (MXR2MXF A) & width A = width (MXR2MXF A) ) ;
3 * A = MXF2MXR (e3 * (MXR2MXF A)) by Def7
.= MXF2MXR (((1_ F_Real) * (MXR2MXF A)) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:12
.= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) + (1_ F_Real)) * (MXR2MXF A))) by MATRIX_5:9
.= MXF2MXR ((MXR2MXF A) + (((1_ F_Real) * (MXR2MXF A)) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:12
.= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + ((1_ F_Real) * (MXR2MXF A)))) by MATRIX_5:9
.= MXF2MXR ((MXR2MXF A) + ((MXR2MXF A) + (MXR2MXF A))) by MATRIX_5:9
.= MXF2MXR (((MXR2MXF A) + (MXR2MXF A)) + (MXR2MXF A)) by A1, MATRIX_3:3 ;
hence (A + A) + A = 3 * A ; ::_thesis: verum
end;
definition
let n, m be Nat;
func 0_Rmatrix (n,m) -> Matrix of REAL equals :: MATRIXR1:def 8
MXF2MXR (0. (F_Real,n,m));
coherence
MXF2MXR (0. (F_Real,n,m)) is Matrix of REAL ;
end;
:: deftheorem defines 0_Rmatrix MATRIXR1:def_8_:_
for n, m being Nat holds 0_Rmatrix (n,m) = MXF2MXR (0. (F_Real,n,m));
theorem :: MATRIXR1:35
for A, B being Matrix of REAL holds A - (- B) = A + B
proof
let A, B be Matrix of REAL; ::_thesis: A - (- B) = A + B
A + B = MXF2MXR ((MXR2MXF A) + (MXR2MXF (- (- B)))) by MATRIX_4:1;
hence A - (- B) = A + B by MATRIX_4:def_1; ::_thesis: verum
end;
theorem Th36: :: MATRIXR1:36
for n, m being Nat
for A being Matrix of REAL st len A = n & width A = m & n > 0 holds
( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )
proof
let n, m be Nat; ::_thesis: for A being Matrix of REAL st len A = n & width A = m & n > 0 holds
( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )
let A be Matrix of REAL; ::_thesis: ( len A = n & width A = m & n > 0 implies ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) )
assume that
A1: ( len A = n & width A = m ) and
A2: n > 0 ; ::_thesis: ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A )
reconsider D = MXR2MXF A as Matrix of n,m,F_Real by A1, A2, MATRIX_1:20;
( len (0. (F_Real,n,m)) = n & width (0. (F_Real,n,m)) = m ) by A2, MATRIX_1:23;
then A3: (0_Rmatrix (n,m)) + A = MXF2MXR (D + (0. (F_Real,n,m))) by A1, MATRIX_3:2
.= A by MATRIX_3:4 ;
MXR2MXF A is Matrix of n,m,F_Real by A1, A2, MATRIX_1:20;
hence ( A + (0_Rmatrix (n,m)) = A & (0_Rmatrix (n,m)) + A = A ) by A3, MATRIX_3:4; ::_thesis: verum
end;
theorem :: MATRIXR1:37
for A, B being Matrix of REAL st len A = len B & width A = width B & A = A + B holds
B = 0_Rmatrix ((len A),(width A))
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & A = A + B implies B = 0_Rmatrix ((len A),(width A)) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: A = A + B ; ::_thesis: B = 0_Rmatrix ((len A),(width A))
0_Rmatrix ((len A),(width A)) = (A + B) + (- A) by A2, MATRIX_4:2
.= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) + (- (MXR2MXF A))) by A1, MATRIX_3:2
.= MXF2MXR (((MXR2MXF B) + (MXR2MXF A)) - (MXR2MXF A)) by MATRIX_4:def_1
.= B by A1, MATRIX_4:21 ;
hence B = 0_Rmatrix ((len A),(width A)) ; ::_thesis: verum
end;
theorem :: MATRIXR1:38
for A, B being Matrix of REAL st len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) holds
B = - A
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & A + B = 0_Rmatrix ((len A),(width A)) implies B = - A )
assume that
A1: ( len A = len B & width A = width B ) and
A2: A + B = 0_Rmatrix ((len A),(width A)) ; ::_thesis: B = - A
A3: ( len (- (MXR2MXF B)) = len (MXR2MXF B) & width (- (MXR2MXF B)) = width (MXR2MXF B) ) by MATRIX_3:def_2;
MXR2MXF (0_Rmatrix ((len A),(width A))) = (MXR2MXF A) + (- (- (MXR2MXF B))) by A2, MATRIX_4:1
.= (MXR2MXF A) - (- (MXR2MXF B)) by MATRIX_4:def_1 ;
then MXR2MXF A = - (MXR2MXF B) by A1, A3, MATRIX_4:7;
hence B = - A by MATRIX_4:1; ::_thesis: verum
end;
theorem :: MATRIXR1:39
for A, B being Matrix of REAL st len A = len B & width A = width B & B - A = B holds
A = 0_Rmatrix ((len A),(width A))
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & B - A = B implies A = 0_Rmatrix ((len A),(width A)) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: B - A = B ; ::_thesis: A = 0_Rmatrix ((len A),(width A))
(MXR2MXF B) + (MXR2MXF A) = MXR2MXF B by A1, A2, MATRIX_4:22;
hence A = 0_Rmatrix ((len A),(width A)) by A1, MATRIX_4:6; ::_thesis: verum
end;
theorem Th40: :: MATRIXR1:40
for a being Real
for A, B being Matrix of REAL st width A = len B holds
A * (a * B) = a * (A * B)
proof
let a be Real; ::_thesis: for A, B being Matrix of REAL st width A = len B holds
A * (a * B) = a * (A * B)
let A, B be Matrix of REAL; ::_thesis: ( width A = len B implies A * (a * B) = a * (A * B) )
assume A1: width A = len B ; ::_thesis: A * (a * B) = a * (A * B)
reconsider ea = a as Element of F_Real ;
thus A * (a * B) = MXF2MXR ((MXR2MXF A) * (MXR2MXF (MXF2MXR (ea * (MXR2MXF B))))) by Def7
.= MXF2MXR (ea * (MXR2MXF (MXF2MXR ((MXR2MXF A) * (MXR2MXF B))))) by A1, Th22
.= a * (A * B) by Def7 ; ::_thesis: verum
end;
theorem :: MATRIXR1:41
for a being Real
for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds
(a * A) * B = a * (A * B)
proof
let a be Real; ::_thesis: for A, B being Matrix of REAL st width A = len B & len A > 0 & len B > 0 & width B > 0 holds
(a * A) * B = a * (A * B)
let A, B be Matrix of REAL; ::_thesis: ( width A = len B & len A > 0 & len B > 0 & width B > 0 implies (a * A) * B = a * (A * B) )
assume that
A1: width A = len B and
A2: len A > 0 and
A3: len B > 0 and
A4: width B > 0 ; ::_thesis: (a * A) * B = a * (A * B)
( len (A @) = width A & width (B @) = len B ) by A1, A3, A4, MATRIX_2:10;
then (B @) * (a * (A @)) = a * ((B @) * (A @)) by A1, Th40;
then A5: (B @) * (a * (A @)) = a * ((A * B) @) by A1, A4, MATRIX_3:22;
A6: width (a * (A * B)) = width (A * B) by Th27
.= width B by A1, MATRIX_3:def_4 ;
A7: len (a * (A * B)) = len (A * B) by Th27
.= len A by A1, MATRIX_3:def_4 ;
A8: len (a * A) = len A by Th27;
A9: width (a * A) = width A by Th27;
width (A * B) = width B by A1, MATRIX_3:def_4;
then (B @) * (a * (A @)) = (a * (A * B)) @ by A4, A5, Th30;
then (B @) * ((a * A) @) = (a * (A * B)) @ by A1, A3, Th30;
then A10: ((a * A) * B) @ = (a * (A * B)) @ by A1, A4, A9, MATRIX_3:22;
( len ((a * A) * B) = len (a * A) & width ((a * A) * B) = width B ) by A1, A9, MATRIX_3:def_4;
then (a * A) * B = ((a * (A * B)) @) @ by A2, A4, A8, A10, MATRIX_2:13;
hence (a * A) * B = a * (A * B) by A2, A4, A7, A6, MATRIX_2:13; ::_thesis: verum
end;
theorem :: MATRIXR1:42
for M being Matrix of REAL holds M + (0_Rmatrix ((len M),(width M))) = M
proof
let M be Matrix of REAL; ::_thesis: M + (0_Rmatrix ((len M),(width M))) = M
A1: ( len M = len (MXR2MXF M) & width M = width (MXR2MXF M) ) ;
M + (0_Rmatrix ((len M),(width M))) = M + (- (0_Rmatrix ((len M),(width M)))) by MATRIX_4:9
.= M + (- (M - M)) by MATRIX_4:3
.= MXF2MXR ((MXR2MXF M) - ((MXR2MXF M) - (MXR2MXF M))) by MATRIX_4:def_1
.= M by A1, MATRIX_4:11 ;
hence M + (0_Rmatrix ((len M),(width M))) = M ; ::_thesis: verum
end;
theorem :: MATRIXR1:43
for a being real number
for A, B being Matrix of REAL st len A = len B & width A = width B holds
a * (A + B) = (a * A) + (a * B)
proof
let a be real number ; ::_thesis: for A, B being Matrix of REAL st len A = len B & width A = width B holds
a * (A + B) = (a * A) + (a * B)
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B implies a * (A + B) = (a * A) + (a * B) )
assume A1: ( len A = len B & width A = width B ) ; ::_thesis: a * (A + B) = (a * A) + (a * B)
reconsider ea = a as Element of F_Real by XREAL_0:def_1;
A2: (a * A) + (a * B) = MXF2MXR ((MXR2MXF (MXF2MXR (ea * (MXR2MXF A)))) + (MXR2MXF (a * B))) by Def7
.= MXF2MXR ((ea * (MXR2MXF A)) + (MXR2MXF (MXF2MXR (ea * (MXR2MXF B))))) by Def7
.= MXF2MXR ((ea * (MXR2MXF A)) + (ea * (MXR2MXF B))) ;
a * (A + B) = MXF2MXR (ea * (MXR2MXF (A + B))) by Def7
.= MXF2MXR ((ea * (MXR2MXF A)) + (ea * (MXR2MXF B))) by A1, MATRIX_5:20 ;
hence a * (A + B) = (a * A) + (a * B) by A2; ::_thesis: verum
end;
theorem :: MATRIXR1:44
for A being Matrix of REAL st len A > 0 holds
0 * A = 0_Rmatrix ((len A),(width A))
proof
let A be Matrix of REAL; ::_thesis: ( len A > 0 implies 0 * A = 0_Rmatrix ((len A),(width A)) )
assume A1: len A > 0 ; ::_thesis: 0 * A = 0_Rmatrix ((len A),(width A))
0 * A = MXF2MXR ((0. F_Real) * (MXR2MXF A)) by Def7
.= 0_Rmatrix ((len A),(width A)) by A1, MATRIX_5:24 ;
hence 0 * A = 0_Rmatrix ((len A),(width A)) ; ::_thesis: verum
end;
definition
let x be FinSequence of REAL ;
assume A1: len x > 0 ;
func ColVec2Mx x -> Matrix of REAL means :Def9: :: MATRIXR1:def 9
( len it = len x & width it = 1 & ( for j being Nat st j in dom x holds
it . j = <*(x . j)*> ) );
existence
ex b1 being Matrix of REAL st
( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) )
proof
reconsider n = len x as Element of NAT ;
deffunc H1( Nat) -> FinSequence of REAL = <*(x . $1)*>;
consider C being FinSequence such that
A2: ( len C = n & ( for j being Nat st j in dom C holds
C . j = H1(j) ) ) from FINSEQ_1:sch_2();
for y being set st y in rng C holds
ex p being FinSequence of REAL st
( y = p & len p = 1 )
proof
let y be set ; ::_thesis: ( y in rng C implies ex p being FinSequence of REAL st
( y = p & len p = 1 ) )
assume y in rng C ; ::_thesis: ex p being FinSequence of REAL st
( y = p & len p = 1 )
then consider z being set such that
A3: z in dom C and
A4: y = C . z by FUNCT_1:def_3;
reconsider z = z as Element of NAT by A3;
len <*(x . z)*> = 1 by FINSEQ_1:39;
hence ex p being FinSequence of REAL st
( y = p & len p = 1 ) by A2, A3, A4; ::_thesis: verum
end;
then reconsider B = C as Matrix of REAL by MATRIX_1:9;
for p being FinSequence of REAL st p in rng B holds
len p = 1
proof
let p be FinSequence of REAL ; ::_thesis: ( p in rng B implies len p = 1 )
assume p in rng B ; ::_thesis: len p = 1
then consider i being Nat such that
A5: ( i in dom B & B . i = p ) by FINSEQ_2:10;
len <*(x . i)*> = 1 by FINSEQ_1:39;
hence len p = 1 by A2, A5; ::_thesis: verum
end;
then reconsider A = B as Matrix of len B,1, REAL by MATRIX_1:def_2;
A6: Seg (len x) = dom x by FINSEQ_1:def_3;
( dom C = Seg n & width A = 1 ) by A1, A2, FINSEQ_1:def_3, MATRIX_1:23;
hence ex b1 being Matrix of REAL st
( len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) ) by A2, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len x & width b1 = 1 & ( for j being Nat st j in dom x holds
b1 . j = <*(x . j)*> ) & len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds
b2 . j = <*(x . j)*> ) holds
b1 = b2
proof
let A, B be Matrix of REAL; ::_thesis: ( len A = len x & width A = 1 & ( for j being Nat st j in dom x holds
A . j = <*(x . j)*> ) & len B = len x & width B = 1 & ( for j being Nat st j in dom x holds
B . j = <*(x . j)*> ) implies A = B )
assume that
A7: len A = len x and
width A = 1 and
A8: for k being Nat st k in dom x holds
A . k = <*(x . k)*> and
A9: len B = len x and
width B = 1 and
A10: for k being Nat st k in dom x holds
B . k = <*(x . k)*> ; ::_thesis: A = B
A11: now__::_thesis:_for_k_being_Nat_st_k_in_dom_x_holds_
A_._k_=_B_._k
let k be Nat; ::_thesis: ( k in dom x implies A . k = B . k )
assume A12: k in dom x ; ::_thesis: A . k = B . k
hence A . k = <*(x . k)*> by A8
.= B . k by A10, A12 ;
::_thesis: verum
end;
( dom A = dom x & dom B = dom x ) by A7, A9, FINSEQ_3:29;
hence A = B by A11, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines ColVec2Mx MATRIXR1:def_9_:_
for x being FinSequence of REAL st len x > 0 holds
for b2 being Matrix of REAL holds
( b2 = ColVec2Mx x iff ( len b2 = len x & width b2 = 1 & ( for j being Nat st j in dom x holds
b2 . j = <*(x . j)*> ) ) );
theorem :: MATRIXR1:45
for x being FinSequence of REAL
for M being Matrix of REAL st len x > 0 holds
( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )
proof
let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL st len x > 0 holds
( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )
let M be Matrix of REAL; ::_thesis: ( len x > 0 implies ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) ) )
consider n being Nat such that
A1: for x being set st x in rng M holds
ex s2 being FinSequence st
( s2 = x & len s2 = n ) by MATRIX_1:def_1;
assume A2: len x > 0 ; ::_thesis: ( M = ColVec2Mx x iff ( Col (M,1) = x & width M = 1 ) )
thus ( M = ColVec2Mx x implies ( Col (M,1) = x & width M = 1 ) ) ::_thesis: ( Col (M,1) = x & width M = 1 implies M = ColVec2Mx x )
proof
assume A3: M = ColVec2Mx x ; ::_thesis: ( Col (M,1) = x & width M = 1 )
then A4: width M = 1 by A2, Def9;
A5: len M = len x by A2, A3, Def9;
then A6: dom M = dom x by FINSEQ_3:29;
for j being Nat st j in dom M holds
x . j = M * (j,1)
proof
let j be Nat; ::_thesis: ( j in dom M implies x . j = M * (j,1) )
assume A7: j in dom M ; ::_thesis: x . j = M * (j,1)
then reconsider j = j as Element of NAT ;
A8: M . j = <*(x . j)*> by A2, A3, A6, A7, Def9;
then reconsider q = M . j as FinSequence of REAL ;
A9: q . 1 = x . j by A8, FINSEQ_1:40;
1 in Seg (width M) by A4, FINSEQ_1:1;
then [j,1] in Indices M by A7, ZFMISC_1:87;
hence x . j = M * (j,1) by A9, MATRIX_1:def_5; ::_thesis: verum
end;
hence ( Col (M,1) = x & width M = 1 ) by A2, A3, A5, Def9, MATRIX_1:def_8; ::_thesis: verum
end;
assume that
A10: Col (M,1) = x and
A11: width M = 1 ; ::_thesis: M = ColVec2Mx x
A12: len x = len M by A10, MATRIX_1:def_8;
then consider s being FinSequence such that
A13: s in rng M and
A14: len s = 1 by A2, A11, MATRIX_1:def_3;
A15: dom x = dom M by A12, FINSEQ_3:29;
A16: ex s2 being FinSequence st
( s2 = s & len s2 = n ) by A13, A1;
for j being Nat st j in dom x holds
M . j = <*(x . j)*>
proof
let j be Nat; ::_thesis: ( j in dom x implies M . j = <*(x . j)*> )
assume A17: j in dom x ; ::_thesis: M . j = <*(x . j)*>
then M . j in rng M by A15, FUNCT_1:def_3;
then A18: ex s3 being FinSequence st
( s3 = M . j & len s3 = 1 ) by A14, A1, A16;
1 in Seg (width M) by A11, FINSEQ_1:1;
then [j,1] in Indices M by A15, A17, ZFMISC_1:87;
then A19: ex p being FinSequence of REAL st
( p = M . j & M * (j,1) = p . 1 ) by MATRIX_1:def_5;
x . j = M * (j,1) by A10, A15, A17, MATRIX_1:def_8;
hence M . j = <*(x . j)*> by A19, A18, FINSEQ_1:40; ::_thesis: verum
end;
hence M = ColVec2Mx x by A2, A11, A12, Def9; ::_thesis: verum
end;
theorem Th46: :: MATRIXR1:46
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, Def9;
A4: Seg (width (ColVec2Mx x1)) = Seg 1 by A2, Def9;
A5: dom x1 = dom x2 by A1, FINSEQ_3:29;
A6: len (ColVec2Mx x1) = len x1 by A2, Def9;
then A7: dom (ColVec2Mx x1) = dom x1 by FINSEQ_3:29;
( len (ColVec2Mx x2) = len x2 & width (ColVec2Mx x2) = 1 ) by A1, A2, Def9;
then A8: Indices (ColVec2Mx x2) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55;
A9: len (x1 + x2) = len x1 by A1, RVSUM_1:115;
then A10: dom (x1 + x2) = dom x1 by FINSEQ_3:29;
A11: ( len (ColVec2Mx (x1 + x2)) = len (x1 + x2) & width (ColVec2Mx (x1 + x2)) = 1 ) by A2, A9, Def9;
then A12: Indices (ColVec2Mx (x1 + x2)) = Indices (ColVec2Mx x1) by A1, A6, A3, MATRIX_4:55, RVSUM_1:115;
for i, j being 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 Nat; ::_thesis: ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) )
thus ( [i,j] in Indices (ColVec2Mx x1) implies (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) ) ::_thesis: verum
proof
assume A13: [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
A14: q1 = (ColVec2Mx x1) . i and
A15: (ColVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5;
j in Seg 1 by A4, A13, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A16: j = 1 by XXREAL_0:1;
A17: i in dom x1 by A7, A13, ZFMISC_1:87;
then (ColVec2Mx x1) . i = <*(x1 . i)*> by A2, Def9;
then A18: q1 . j = x1 . i by A16, A14, FINSEQ_1:40;
consider p being FinSequence of REAL such that
A19: p = (ColVec2Mx (x1 + x2)) . i and
A20: (ColVec2Mx (x1 + x2)) * (i,j) = p . j by A12, A13, MATRIX_1:def_5;
consider q2 being FinSequence of REAL such that
A21: q2 = (ColVec2Mx x2) . i and
A22: (ColVec2Mx x2) * (i,j) = q2 . j by A8, A13, MATRIX_1:def_5;
(ColVec2Mx x2) . i = <*(x2 . i)*> by A1, A2, A5, A17, Def9;
then A23: q2 . j = x2 . i by A16, A21, FINSEQ_1:40;
(ColVec2Mx (x1 + x2)) . i = <*((x1 + x2) . i)*> by A2, A9, A10, A17, Def9;
then p . j = (x1 + x2) . i by A16, A19, FINSEQ_1:40;
hence (ColVec2Mx (x1 + x2)) * (i,j) = ((ColVec2Mx x1) * (i,j)) + ((ColVec2Mx x2) * (i,j)) by A10, A17, A20, A15, A18, A22, A23, VALUED_1:def_1; ::_thesis: verum
end;
end;
hence ColVec2Mx (x1 + x2) = (ColVec2Mx x1) + (ColVec2Mx x2) by A1, A6, A11, A3, Th26, RVSUM_1:115; ::_thesis: verum
end;
theorem Th47: :: MATRIXR1:47
for a being Real
for x being FinSequence of REAL st len x > 0 holds
ColVec2Mx (a * x) = a * (ColVec2Mx x)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL st len x > 0 holds
ColVec2Mx (a * x) = a * (ColVec2Mx x)
let x be FinSequence of REAL ; ::_thesis: ( len x > 0 implies ColVec2Mx (a * x) = a * (ColVec2Mx x) )
assume A1: len x > 0 ; ::_thesis: ColVec2Mx (a * x) = a * (ColVec2Mx x)
A2: len (a * (ColVec2Mx x)) = len (ColVec2Mx x) by Th27
.= len x by A1, Def9 ;
A3: len (a * x) = len x by RVSUM_1:117;
then A4: dom (a * x) = dom x by FINSEQ_3:29;
A5: for j being Nat st j in dom (a * x) holds
(a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
proof
len (ColVec2Mx x) = len x by A1, Def9;
then A6: dom (ColVec2Mx x) = dom x by FINSEQ_3:29;
let j be Nat; ::_thesis: ( j in dom (a * x) implies (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> )
consider n being Nat such that
A7: for x2 being set st x2 in rng (a * (ColVec2Mx x)) holds
ex s2 being FinSequence st
( s2 = x2 & len s2 = n ) by MATRIX_1:def_1;
assume A8: j in dom (a * x) ; ::_thesis: (a * (ColVec2Mx x)) . j = <*((a * x) . j)*>
then A9: (ColVec2Mx x) . j = <*(x . j)*> by A1, A4, Def9;
A10: j in dom (a * (ColVec2Mx x)) by A2, A3, A8, FINSEQ_3:29;
then (a * (ColVec2Mx x)) . j in rng (a * (ColVec2Mx x)) by FUNCT_1:def_3;
then reconsider q = (a * (ColVec2Mx x)) . j as FinSequence of REAL by FINSEQ_1:def_11;
q in rng (a * (ColVec2Mx x)) by A10, FUNCT_1:def_3;
then A11: ex s2 being FinSequence st
( s2 = q & len s2 = n ) by A7;
consider s being FinSequence such that
A12: s in rng (a * (ColVec2Mx x)) and
A13: len s = width (a * (ColVec2Mx x)) by A1, A2, MATRIX_1:def_3;
ex s3 being FinSequence st
( s3 = s & len s3 = n ) by A12, A7;
then A14: len q = width (ColVec2Mx x) by A13, A11, Th27
.= 1 by A1, Def9
.= len <*((a * x) . j)*> by FINSEQ_1:40 ;
width (ColVec2Mx x) = 1 by A1, Def9;
then A15: 1 in Seg (width (MXR2MXF (ColVec2Mx x))) by FINSEQ_1:1;
j in dom x by A3, A8, FINSEQ_3:29;
then A16: [j,1] in Indices (MXR2MXF (ColVec2Mx x)) by A6, A15, ZFMISC_1:87;
then A17: ex p3 being FinSequence of REAL st
( p3 = (ColVec2Mx x) . j & (ColVec2Mx x) * (j,1) = p3 . 1 ) by MATRIX_1:def_5;
[j,1] in Indices (a * (ColVec2Mx x)) by A16, Th28;
then A18: ex p being FinSequence of REAL st
( p = (a * (ColVec2Mx x)) . j & (a * (ColVec2Mx x)) * (j,1) = p . 1 ) by MATRIX_1:def_5;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A19: q . 1 = a * ((ColVec2Mx x) * (j,1)) by A16, A18, Th29
.= a * (x . j) by A17, A9, FINSEQ_1:40
.= (a * x) . j by RVSUM_1:44
.= <*((a * x) . j)*> . 1 by FINSEQ_1:40 ;
for i being Nat st 1 <= i & i <= len <*((a * x) . j)*> holds
q . i = <*((a * x) . j)*> . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len <*((a * x) . j)*> implies q . i = <*((a * x) . j)*> . i )
A20: len <*((a * x) . j)*> = 1 by FINSEQ_1:40;
assume ( 1 <= i & i <= len <*((a * x) . j)*> ) ; ::_thesis: q . i = <*((a * x) . j)*> . i
then i = 1 by A20, XXREAL_0:1;
hence q . i = <*((a * x) . j)*> . i by A19; ::_thesis: verum
end;
hence (a * (ColVec2Mx x)) . j = <*((a * x) . j)*> by A14, FINSEQ_1:14; ::_thesis: verum
end;
width (a * (ColVec2Mx x)) = width (ColVec2Mx x) by Th27
.= 1 by A1, Def9 ;
hence ColVec2Mx (a * x) = a * (ColVec2Mx x) by A1, A2, A3, A5, Def9; ::_thesis: verum
end;
definition
let x be FinSequence of REAL ;
func LineVec2Mx x -> Matrix of REAL means :Def10: :: MATRIXR1:def 10
( width it = len x & len it = 1 & ( for j being Nat st j in dom x holds
it * (1,j) = x . j ) );
existence
ex b1 being Matrix of REAL st
( width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds
b1 * (1,j) = x . j ) )
proof
set B = <*x*>;
A1: rng <*x*> = {x} by FINSEQ_1:39;
for y being set st y in rng <*x*> holds
ex p being FinSequence of REAL st
( y = p & len p = len x )
proof
let y be set ; ::_thesis: ( y in rng <*x*> implies ex p being FinSequence of REAL st
( y = p & len p = len x ) )
assume y in rng <*x*> ; ::_thesis: ex p being FinSequence of REAL st
( y = p & len p = len x )
then y = x by A1, TARSKI:def_1;
hence ex p being FinSequence of REAL st
( y = p & len p = len x ) ; ::_thesis: verum
end;
then reconsider C = <*x*> as Matrix of REAL by MATRIX_1:9;
take C ; ::_thesis: ( width C = len x & len C = 1 & ( for j being Nat st j in dom x holds
C * (1,j) = x . j ) )
A2: len <*x*> = 1 by FINSEQ_1:39;
then dom C = Seg 1 by FINSEQ_1:def_3;
then A3: 1 in dom C by FINSEQ_1:1;
for p being FinSequence of REAL st p in rng C holds
len p = len x by A1, TARSKI:def_1;
then ( len <*x*> = 1 & C is Matrix of 1, len x, REAL ) by A2, MATRIX_1:def_2;
hence A4: width C = len x by MATRIX_1:20; ::_thesis: ( len C = 1 & ( for j being Nat st j in dom x holds
C * (1,j) = x . j ) )
thus len C = 1 by FINSEQ_1:40; ::_thesis: for j being Nat st j in dom x holds
C * (1,j) = x . j
let j be Nat; ::_thesis: ( j in dom x implies C * (1,j) = x . j )
assume j in dom x ; ::_thesis: C * (1,j) = x . j
then j in Seg (len x) by FINSEQ_1:def_3;
then ( <*x*> . 1 = x & [1,j] in Indices C ) by A4, A3, FINSEQ_1:40, ZFMISC_1:def_2;
hence C * (1,j) = x . j by MATRIX_1:def_5; ::_thesis: verum
end;
uniqueness
for b1, b2 being Matrix of REAL st width b1 = len x & len b1 = 1 & ( for j being Nat st j in dom x holds
b1 * (1,j) = x . j ) & width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds
b2 * (1,j) = x . j ) holds
b1 = b2
proof
let A, B be Matrix of REAL; ::_thesis: ( width A = len x & len A = 1 & ( for j being Nat st j in dom x holds
A * (1,j) = x . j ) & width B = len x & len B = 1 & ( for j being Nat st j in dom x holds
B * (1,j) = x . j ) implies A = B )
assume that
A5: width A = len x and
A6: len A = 1 and
A7: for k being Nat st k in dom x holds
A * (1,k) = x . k and
A8: ( width B = len x & len B = 1 ) and
A9: for k being Nat st k in dom x holds
B * (1,k) = x . k ; ::_thesis: A = B
A10: dom A = Seg 1 by A6, FINSEQ_1:def_3;
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) )
assume A11: [i,j] in Indices A ; ::_thesis: A * (i,j) = B * (i,j)
then i in Seg 1 by A10, ZFMISC_1:87;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A12: i = 1 by XXREAL_0:1;
j in Seg (len x) by A5, A11, ZFMISC_1:87;
then A13: j in dom x by FINSEQ_1:def_3;
then A * (i,j) = x . j by A7, A12;
hence A * (i,j) = B * (i,j) by A9, A13, A12; ::_thesis: verum
end;
hence A = B by A5, A6, A8, MATRIX_1:21; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines LineVec2Mx MATRIXR1:def_10_:_
for x being FinSequence of REAL
for b2 being Matrix of REAL holds
( b2 = LineVec2Mx x iff ( width b2 = len x & len b2 = 1 & ( for j being Nat st j in dom x holds
b2 * (1,j) = x . j ) ) );
theorem :: MATRIXR1:48
for x being FinSequence of REAL
for M being Matrix of REAL holds
( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )
proof
let x be FinSequence of REAL ; ::_thesis: for M being Matrix of REAL holds
( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )
let M be Matrix of REAL; ::_thesis: ( M = LineVec2Mx x iff ( Line (M,1) = x & len M = 1 ) )
thus ( M = LineVec2Mx x implies ( Line (M,1) = x & len M = 1 ) ) ::_thesis: ( Line (M,1) = x & len M = 1 implies M = LineVec2Mx x )
proof
assume A1: M = LineVec2Mx x ; ::_thesis: ( Line (M,1) = x & len M = 1 )
then A2: for j being Nat st j in dom x holds
M * (1,j) = x . j by Def10;
A3: width M = len x by A1, Def10;
then dom x = Seg (width M) by FINSEQ_1:def_3;
hence ( Line (M,1) = x & len M = 1 ) by A1, A3, A2, Def10, MATRIX_1:def_7; ::_thesis: verum
end;
assume that
A4: Line (M,1) = x and
A5: len M = 1 ; ::_thesis: M = LineVec2Mx x
A6: for j being Nat st j in Seg (width M) holds
x . j = M * (1,j) by A4, MATRIX_1:def_7;
A7: len x = width M by A4, MATRIX_1:def_7;
then Seg (width M) = dom x by FINSEQ_1:def_3;
hence M = LineVec2Mx x by A5, A7, A6, Def10; ::_thesis: verum
end;
theorem Th49: :: MATRIXR1:49
for x being FinSequence of REAL st len x > 0 holds
( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )
proof
let x be FinSequence of REAL ; ::_thesis: ( len x > 0 implies ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x ) )
A1: dom (LineVec2Mx x) = Seg (len (LineVec2Mx x)) by FINSEQ_1:def_3;
A2: width (LineVec2Mx x) = len x by Def10;
assume A3: len x > 0 ; ::_thesis: ( (LineVec2Mx x) @ = ColVec2Mx x & (ColVec2Mx x) @ = LineVec2Mx x )
then A4: len (ColVec2Mx x) = len x by Def9;
A5: len (LineVec2Mx x) = 1 by Def10;
A6: width (ColVec2Mx x) = 1 by A3, Def9;
A7: dom (ColVec2Mx x) = Seg (len (ColVec2Mx x)) by FINSEQ_1:def_3;
A8: for i, j being Nat holds
( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )
proof
let i, j be Nat; ::_thesis: ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) )
( [i,j] in Indices (ColVec2Mx x) iff ( i in dom (ColVec2Mx x) & j in Seg (width (ColVec2Mx x)) ) ) by ZFMISC_1:87;
hence ( [i,j] in Indices (ColVec2Mx x) iff [j,i] in Indices (LineVec2Mx x) ) by A2, A5, A4, A6, A7, A1, ZFMISC_1:87; ::_thesis: verum
end;
A9: for i, j being Nat st [j,i] in Indices (LineVec2Mx x) holds
(ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)
proof
let i, j be Nat; ::_thesis: ( [j,i] in Indices (LineVec2Mx x) implies (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i) )
assume A10: [j,i] in Indices (LineVec2Mx x) ; ::_thesis: (ColVec2Mx x) * (i,j) = (LineVec2Mx x) * (j,i)
then [i,j] in Indices (ColVec2Mx x) by A8;
then A11: ex p being FinSequence of REAL st
( p = (ColVec2Mx x) . i & (ColVec2Mx x) * (i,j) = p . j ) by MATRIX_1:def_5;
j in Seg 1 by A5, A1, A10, ZFMISC_1:87;
then ( 1 <= j & j <= 1 ) by FINSEQ_1:1;
then A12: j = 1 by XXREAL_0:1;
i in Seg (len x) by A2, A10, ZFMISC_1:87;
then A13: i in dom x by FINSEQ_1:def_3;
then (ColVec2Mx x) . i = <*(x . i)*> by A3, Def9;
hence (ColVec2Mx x) * (i,j) = x . i by A12, A11, FINSEQ_1:40
.= (LineVec2Mx x) * (j,i) by A12, A13, Def10 ;
::_thesis: verum
end;
hence (LineVec2Mx x) @ = ColVec2Mx x by A2, A4, A8, MATRIX_1:def_6; ::_thesis: (ColVec2Mx x) @ = LineVec2Mx x
A14: for i, j being Nat st [j,i] in Indices (ColVec2Mx x) holds
(LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)
proof
let i, j be Nat; ::_thesis: ( [j,i] in Indices (ColVec2Mx x) implies (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) )
assume [j,i] in Indices (ColVec2Mx x) ; ::_thesis: (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i)
then [i,j] in Indices (LineVec2Mx x) by A8;
hence (LineVec2Mx x) * (i,j) = (ColVec2Mx x) * (j,i) by A9; ::_thesis: verum
end;
for i, j being Nat holds
( [i,j] in Indices (LineVec2Mx x) iff [j,i] in Indices (ColVec2Mx x) ) by A8;
hence (ColVec2Mx x) @ = LineVec2Mx x by A5, A6, A14, MATRIX_1:def_6; ::_thesis: verum
end;
theorem Th50: :: MATRIXR1:50
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) )
assume A1: len x1 = len x2 ; ::_thesis: LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2)
then A2: dom x1 = dom x2 by FINSEQ_3:29;
len (x1 + x2) = len x1 by A1, RVSUM_1:115;
then A3: dom (x1 + x2) = dom x1 by FINSEQ_3:29;
A4: ( width (LineVec2Mx x1) = len x1 & len (LineVec2Mx x1) = 1 ) by Def10;
( width (LineVec2Mx x2) = len x2 & len (LineVec2Mx x2) = 1 ) by Def10;
then A5: Indices (LineVec2Mx x2) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55;
A6: Seg (width (LineVec2Mx x1)) = Seg (len x1) by Def10
.= dom x1 by FINSEQ_1:def_3 ;
A7: dom (LineVec2Mx x1) = Seg (len (LineVec2Mx x1)) by FINSEQ_1:def_3
.= Seg 1 by Def10 ;
A8: ( width (LineVec2Mx (x1 + x2)) = len (x1 + x2) & len (LineVec2Mx (x1 + x2)) = 1 ) by Def10;
then A9: Indices (LineVec2Mx (x1 + x2)) = Indices (LineVec2Mx x1) by A1, A4, MATRIX_4:55, RVSUM_1:115;
for i, j being 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 Nat; ::_thesis: ( [i,j] in Indices (LineVec2Mx x1) implies (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) )
assume A10: [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
A11: (LineVec2Mx x1) * (i,j) = q1 . j by MATRIX_1:def_5;
consider p being FinSequence of REAL such that
p = (LineVec2Mx (x1 + x2)) . i and
A12: (LineVec2Mx (x1 + x2)) * (i,j) = p . j by A9, A10, MATRIX_1:def_5;
consider q2 being FinSequence of REAL such that
q2 = (LineVec2Mx x2) . i and
A13: (LineVec2Mx x2) * (i,j) = q2 . j by A5, A10, MATRIX_1:def_5;
A14: j in dom x1 by A6, A10, ZFMISC_1:87;
i in Seg 1 by A7, A10, ZFMISC_1:87;
then ( 1 <= i & i <= 1 ) by FINSEQ_1:1;
then A15: i = 1 by XXREAL_0:1;
then A16: q1 . j = x1 . j by A14, A11, Def10;
A17: q2 . j = x2 . j by A2, A14, A15, A13, Def10;
p . j = (x1 + x2) . j by A3, A14, A15, A12, Def10;
hence (LineVec2Mx (x1 + x2)) * (i,j) = ((LineVec2Mx x1) * (i,j)) + ((LineVec2Mx x2) * (i,j)) by A3, A14, A12, A11, A16, A13, A17, VALUED_1:def_1; ::_thesis: verum
end;
hence LineVec2Mx (x1 + x2) = (LineVec2Mx x1) + (LineVec2Mx x2) by A1, A8, A4, Th26, RVSUM_1:115; ::_thesis: verum
end;
theorem :: MATRIXR1:51
for a being Real
for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL holds LineVec2Mx (a * x) = a * (LineVec2Mx x)
let x be FinSequence of REAL ; ::_thesis: LineVec2Mx (a * x) = a * (LineVec2Mx x)
A1: len (a * (LineVec2Mx x)) = len (LineVec2Mx x) by Th27
.= 1 by Def10 ;
A2: len (a * x) = len x by RVSUM_1:117;
then A3: dom (a * x) = dom x by FINSEQ_3:29;
A4: for j being Nat st j in dom (a * x) holds
(a * (LineVec2Mx x)) * (1,j) = (a * x) . j
proof
len (LineVec2Mx x) = 1 by Def10;
then 1 in Seg (len (LineVec2Mx x)) by FINSEQ_1:1;
then A5: 1 in dom (LineVec2Mx x) by FINSEQ_1:def_3;
1 in Seg (len (a * (LineVec2Mx x))) by A1, FINSEQ_1:1;
then 1 in dom (a * (LineVec2Mx x)) by FINSEQ_1:def_3;
then (a * (LineVec2Mx x)) . 1 in rng (a * (LineVec2Mx x)) by FUNCT_1:def_3;
then reconsider q = (a * (LineVec2Mx x)) . 1 as FinSequence of REAL by FINSEQ_1:def_11;
let j be Nat; ::_thesis: ( j in dom (a * x) implies (a * (LineVec2Mx x)) * (1,j) = (a * x) . j )
A6: width (LineVec2Mx x) = len x by Def10;
A7: Indices (a * (LineVec2Mx x)) = Indices (LineVec2Mx x) by Th28;
assume A8: j in dom (a * x) ; ::_thesis: (a * (LineVec2Mx x)) * (1,j) = (a * x) . j
then j in Seg (len x) by A2, FINSEQ_1:def_3;
then A9: [1,j] in Indices (a * (LineVec2Mx x)) by A6, A5, A7, ZFMISC_1:87;
then A10: ex p being FinSequence of REAL st
( p = (a * (LineVec2Mx x)) . 1 & (a * (LineVec2Mx x)) * (1,j) = p . j ) by MATRIX_1:def_5;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
q . j = a * ((LineVec2Mx x) * (1,j)) by A7, A9, A10, Th29
.= a * (x . j) by A3, A8, Def10
.= (a * x) . j by RVSUM_1:44 ;
hence (a * (LineVec2Mx x)) * (1,j) = (a * x) . j by A9, MATRIX_1:def_5; ::_thesis: verum
end;
width (a * (LineVec2Mx x)) = width (LineVec2Mx x) by Th27
.= len x by Def10 ;
hence LineVec2Mx (a * x) = a * (LineVec2Mx x) by A1, A2, A4, Def10; ::_thesis: verum
end;
definition
let M be Matrix of REAL;
let x be FinSequence of REAL ;
funcM * x -> FinSequence of REAL equals :: MATRIXR1:def 11
Col ((M * (ColVec2Mx x)),1);
coherence
Col ((M * (ColVec2Mx x)),1) is FinSequence of REAL ;
funcx * M -> FinSequence of REAL equals :: MATRIXR1:def 12
Line (((LineVec2Mx x) * M),1);
coherence
Line (((LineVec2Mx x) * M),1) is FinSequence of REAL ;
end;
:: deftheorem defines * MATRIXR1:def_11_:_
for M being Matrix of REAL
for x being FinSequence of REAL holds M * x = Col ((M * (ColVec2Mx x)),1);
:: deftheorem defines * MATRIXR1:def_12_:_
for M being Matrix of REAL
for x being FinSequence of REAL holds x * M = Line (((LineVec2Mx x) * M),1);
theorem Th52: :: MATRIXR1:52
for x being FinSequence of REAL
for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds
(A @) * x = x * A
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds
(A @) * x = x * A
let A be Matrix of REAL; ::_thesis: ( len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) implies (A @) * x = x * A )
assume that
A1: len A > 0 and
A2: width A > 0 and
A3: ( len A = len x or width (A @) = len x ) ; ::_thesis: (A @) * x = x * A
A4: len A = len x by A2, A3, MATRIX_2:10;
A5: len A = width (A @) by A2, MATRIX_2:10;
then len (ColVec2Mx x) = len x by A1, A3, Def9;
then A6: width ((A @) * (ColVec2Mx x)) = width (ColVec2Mx x) by A3, A5, MATRIX_3:def_4;
width (ColVec2Mx x) = 1 by A1, A3, A5, Def9;
then A7: 1 in Seg (width ((A @) * (ColVec2Mx x))) by A6, FINSEQ_1:1;
A8: len (LineVec2Mx x) = 1 by Def10;
A9: width (LineVec2Mx x) = len x by Def10;
then width (LineVec2Mx x) = len A by A2, A3, MATRIX_2:10;
then ( len ((LineVec2Mx x) * A) = len (LineVec2Mx x) & width ((LineVec2Mx x) * A) = width A ) by MATRIX_3:def_4;
then Line (((LineVec2Mx x) * A),1) = Line (((((LineVec2Mx x) * A) @) @),1) by A2, A8, MATRIX_2:13
.= Line ((((A @) * ((LineVec2Mx x) @)) @),1) by A2, A4, A9, MATRIX_3:22
.= Line ((((A @) * (ColVec2Mx x)) @),1) by A1, A4, Th49
.= Col (((A @) * (ColVec2Mx x)),1) by A7, MATRIX_2:15 ;
hence (A @) * x = x * A ; ::_thesis: verum
end;
theorem Th53: :: MATRIXR1:53
for x being FinSequence of REAL
for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds
A * x = x * (A @)
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) holds
A * x = x * (A @)
let A be Matrix of REAL; ::_thesis: ( len A > 0 & width A > 0 & ( width A = len x or len (A @) = len x ) implies A * x = x * (A @) )
assume that
A1: len A > 0 and
A2: width A > 0 and
A3: ( width A = len x or len (A @) = len x ) ; ::_thesis: A * x = x * (A @)
( len (A @) = width A & width (A @) = len A ) by A2, MATRIX_2:10;
then ((A @) @) * x = x * (A @) by A1, A2, A3, Th52;
hence A * x = x * (A @) by A1, A2, MATRIX_2:13; ::_thesis: verum
end;
theorem Th54: :: MATRIXR1:54
for A, B being Matrix of REAL st len A = len 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 implies for i being Nat st 1 <= i & i <= width A holds
Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) )
assume A1: len A = len B ; ::_thesis: for i being Nat st 1 <= i & i <= width A holds
Col ((A + B),i) = (Col (A,i)) + (Col (B,i))
then A2: dom A = dom B by FINSEQ_3:29;
let i be Nat; ::_thesis: ( 1 <= i & i <= width A implies Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) )
A3: len (Col (A,i)) = len A by MATRIX_1:def_8;
len (Col (B,i)) = len B by MATRIX_1:def_8;
then A4: len ((Col (A,i)) + (Col (B,i))) = len (Col (A,i)) by A1, A3, RVSUM_1:115;
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 (A + B) = len A by Th25;
Seg (len (A + B)) = dom (A + B) by FINSEQ_1:def_3;
then A7: dom ((Col (A,i)) + (Col (B,i))) = dom (A + B) by A3, A6, A4, FINSEQ_1:def_3;
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 A8: 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 A6, 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 A2, A9, MATRIX_1:def_8;
then ((Col (A,i)) . j) + ((Col (B,i)) . j) = (A + B) * (j,i) by A10, Th25;
hence ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) by A7, A8, VALUED_1:def_1; ::_thesis: verum
end;
hence Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) by A3, A6, A4, MATRIX_1:def_8; ::_thesis: verum
end;
theorem Th55: :: MATRIXR1:55
for A, B being Matrix of REAL st 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: ( 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 A1: 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))
let i be Nat; ::_thesis: ( 1 <= i & i <= len A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
A2: len (Line (A,i)) = width A by MATRIX_1:def_7;
assume ( 1 <= i & i <= len A ) ; ::_thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
then A3: i in dom A by FINSEQ_3:25;
A4: width (A + B) = width A by Th25;
len (Line (B,i)) = width B by MATRIX_1:def_7;
then A5: len ((Line (A,i)) + (Line (B,i))) = len (Line (A,i)) by A1, A2, RVSUM_1:115;
then A6: dom ((Line (A,i)) + (Line (B,i))) = Seg (width A) by A2, FINSEQ_1:def_3;
for j being Nat st j in Seg (width (A + B)) holds
((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j)
proof
let j be Nat; ::_thesis: ( j in Seg (width (A + B)) implies ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) )
assume A7: j in Seg (width (A + B)) ; ::_thesis: ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j)
then A8: j in Seg (width A) by Th25;
then A9: ( [i,j] in Indices A & (Line (A,i)) . j = A * (i,j) ) by A3, MATRIX_1:def_7, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
(Line (B,i)) . j = B * (i,j) by A1, A8, MATRIX_1:def_7;
then ((Line (A,i)) . j) + ((Line (B,i)) . j) = (A + B) * (i,j) by A9, Th25;
hence ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) by A4, A6, A7, VALUED_1:def_1; ::_thesis: verum
end;
hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A2, A4, A5, MATRIX_1:def_7; ::_thesis: verum
end;
theorem Th56: :: MATRIXR1:56
for a being Real
for M being Matrix of REAL
for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
proof
let a be Real; ::_thesis: for M being Matrix of REAL
for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let M be Matrix of REAL; ::_thesis: for i being Nat st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
reconsider ea = a as Element of F_Real ;
let i be Nat; ::_thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )
assume A1: ( 1 <= i & i <= width M ) ; ::_thesis: Col ((a * M),i) = a * (Col (M,i))
Col ((a * M),i) = Col ((MXF2MXR (ea * (MXR2MXF M))),i) by Def7
.= ea * (Col ((MXR2MXF M),i)) by A1, Th19 ;
hence Col ((a * M),i) = a * (Col (M,i)) by Th17; ::_thesis: verum
end;
theorem :: MATRIXR1:57
for x1, x2 being FinSequence of REAL
for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds
A * (x1 + x2) = (A * x1) + (A * x2)
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 holds
A * (x1 + x2) = (A * x1) + (A * x2)
let A be Matrix of REAL; ::_thesis: ( len x1 = len x2 & width A = len x1 & len x1 > 0 & len A > 0 implies A * (x1 + x2) = (A * x1) + (A * x2) )
assume that
A1: len x1 = len x2 and
A2: width A = len x1 and
A3: len x1 > 0 and
A4: len A > 0 ; ::_thesis: A * (x1 + x2) = (A * x1) + (A * x2)
A5: len (ColVec2Mx x2) = len x2 by A1, A3, Def9;
A6: len (ColVec2Mx x1) = len x1 by A3, Def9;
then A7: len (A * (ColVec2Mx x1)) = len A by A2, MATRIX_3:def_4
.= len (A * (ColVec2Mx x2)) by A1, A2, A5, MATRIX_3:def_4 ;
A8: width (ColVec2Mx x1) = 1 by A3, Def9;
then A9: 1 <= width (A * (ColVec2Mx x1)) by A2, A6, MATRIX_3:def_4;
A10: width (ColVec2Mx x2) = 1 by A1, A3, Def9;
thus A * (x1 + x2) = Col ((A * ((ColVec2Mx x1) + (ColVec2Mx x2))),1) by A1, A3, Th46
.= Col (((A * (ColVec2Mx x1)) + (A * (ColVec2Mx x2))),1) by A1, A2, A3, A4, A6, A5, A8, A10, MATRIX_4:62
.= (A * x1) + (A * x2) by A7, A9, Th54 ; ::_thesis: verum
end;
theorem :: MATRIXR1:58
for x1, x2 being FinSequence of REAL
for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds
(x1 + x2) * A = (x1 * A) + (x2 * A)
proof
let x1, x2 be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len x1 = len x2 & len A = len x1 & len x1 > 0 holds
(x1 + x2) * A = (x1 * A) + (x2 * A)
let A be Matrix of REAL; ::_thesis: ( len x1 = len x2 & len A = len x1 & len x1 > 0 implies (x1 + x2) * A = (x1 * A) + (x2 * A) )
assume that
A1: len x1 = len x2 and
A2: len A = len x1 and
A3: len x1 > 0 ; ::_thesis: (x1 + x2) * A = (x1 * A) + (x2 * A)
A4: width (LineVec2Mx x2) = len x2 by Def10;
A5: width (LineVec2Mx x1) = len x1 by Def10;
then A6: width ((LineVec2Mx x1) * A) = width A by A2, MATRIX_3:def_4
.= width ((LineVec2Mx x2) * A) by A1, A2, A4, MATRIX_3:def_4 ;
A7: len (LineVec2Mx x1) = 1 by Def10;
then A8: 1 <= len ((LineVec2Mx x1) * A) by A2, A5, MATRIX_3:def_4;
A9: len (LineVec2Mx x2) = 1 by Def10;
thus (x1 + x2) * A = Line ((((LineVec2Mx x1) + (LineVec2Mx x2)) * A),1) by A1, Th50
.= Line ((((LineVec2Mx x1) * A) + ((LineVec2Mx x2) * A)),1) by A1, A2, A3, A5, A4, A7, A9, MATRIX_4:63
.= (x1 * A) + (x2 * A) by A6, A8, Th55 ; ::_thesis: verum
end;
theorem Th59: :: MATRIXR1:59
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, Def9;
width (ColVec2Mx x) = 1 by A2, Def9;
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, Th47
.= Col ((a * (A * (ColVec2Mx x))),1) by A1, A3, Th40
.= a * (A * x) by A4, Th56 ; ::_thesis: verum
end;
theorem :: MATRIXR1:60
for a being Real
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(a * x) * A = a * (x * A)
proof
let a be Real; ::_thesis: for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(a * x) * A = a * (x * A)
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
(a * x) * A = a * (x * A)
let A be Matrix of REAL; ::_thesis: ( len A = len x & len x > 0 & width A > 0 implies (a * x) * A = a * (x * A) )
assume that
A1: len A = len x and
A2: len x > 0 and
A3: width A > 0 ; ::_thesis: (a * x) * A = a * (x * A)
A4: (A @) * x = x * A by A1, A2, A3, Th52;
A5: width (A @) = len x by A1, A3, MATRIX_2:10;
then A6: (A @) * (a * x) = a * ((A @) * x) by A2, Th59;
A7: len (a * x) = len x by RVSUM_1:117;
len (A @) > 0 by A3, MATRIX_2:10;
then (a * x) * ((A @) @) = (A @) * (a * x) by A2, A5, A7, Th53;
hence (a * x) * A = a * (x * A) by A1, A2, A3, A6, A4, MATRIX_2:13; ::_thesis: verum
end;
theorem Th61: :: MATRIXR1:61
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
len (A * x) = len A
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st width A = len x & len x > 0 holds
len (A * x) = len A
let A be Matrix of REAL; ::_thesis: ( width A = len x & len x > 0 implies len (A * x) = len A )
assume that
A1: width A = len x and
A2: len x > 0 ; ::_thesis: len (A * x) = len A
A3: len (ColVec2Mx x) = len x by A2, Def9;
len (Col ((A * (ColVec2Mx x)),1)) = len (A * (ColVec2Mx x)) by MATRIX_1:def_8
.= len A by A1, A3, MATRIX_3:def_4 ;
hence len (A * x) = len A ; ::_thesis: verum
end;
theorem Th62: :: MATRIXR1:62
for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x holds
len (x * A) = width A
proof
let x be FinSequence of REAL ; ::_thesis: for A being Matrix of REAL st len A = len x holds
len (x * A) = width A
let A be Matrix of REAL; ::_thesis: ( len A = len x implies len (x * A) = width A )
assume A1: len A = len x ; ::_thesis: len (x * A) = width A
A2: width (LineVec2Mx x) = len x by Def10;
len (Line (((LineVec2Mx x) * A),1)) = width (MXF2MXR ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))) by MATRIX_1:def_7
.= width A by A1, A2, MATRIX_3:def_4 ;
hence len (x * A) = width A ; ::_thesis: verum
end;
theorem Th63: :: MATRIXR1:63
for x being FinSequence of REAL
for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len A > 0 & len x > 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 A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 holds
(A + B) * x = (A * x) + (B * x)
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & width A = len x & len A > 0 & len x > 0 implies (A + B) * x = (A * x) + (B * x) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: width A = len x and
A3: len A > 0 and
A4: len x > 0 ; ::_thesis: (A + B) * x = (A * x) + (B * x)
A5: len (ColVec2Mx x) = len x by A4, Def9;
then A6: len (A * (ColVec2Mx x)) = len A by A2, MATRIX_3:def_4
.= len (B * (ColVec2Mx x)) by A1, A2, A5, MATRIX_3:def_4 ;
A7: width (A * (ColVec2Mx x)) = width (ColVec2Mx x) by A2, A5, MATRIX_3:def_4
.= 1 by A4, Def9 ;
thus (A + B) * x = Col (((A * (ColVec2Mx x)) + (B * (ColVec2Mx x))),1) by A1, A2, A3, A4, A5, MATRIX_4:63
.= (A * x) + (B * x) by A6, A7, Th54 ; ::_thesis: verum
end;
theorem Th64: :: MATRIXR1:64
for x being FinSequence of REAL
for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x & len x > 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 A = len B & width A = width B & len A = len x & len x > 0 holds
x * (A + B) = (x * A) + (x * B)
let A, B be Matrix of REAL; ::_thesis: ( len A = len B & width A = width B & len A = len x & len x > 0 implies x * (A + B) = (x * A) + (x * B) )
assume that
A1: ( len A = len B & width A = width B ) and
A2: len A = len x and
A3: len x > 0 ; ::_thesis: x * (A + B) = (x * A) + (x * B)
A4: width (LineVec2Mx x) = len x by Def10;
then A5: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A2, MATRIX_3:def_4
.= 1 by Def10 ;
A6: width ((LineVec2Mx x) * A) = width A by A2, A4, MATRIX_3:def_4
.= width ((LineVec2Mx x) * B) by A1, A2, A4, MATRIX_3:def_4 ;
len (LineVec2Mx x) = 1 by Def10;
hence x * (A + B) = Line ((((LineVec2Mx x) * A) + ((LineVec2Mx x) * B)),1) by A1, A2, A3, A4, MATRIX_4:62
.= (x * A) + (x * B) by A6, A5, Th55 ;
::_thesis: verum
end;
theorem :: MATRIXR1:65
for n, m being Element of NAT
for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds
(0_Rmatrix (n,m)) * x = 0* n
proof
let n, m be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds
(0_Rmatrix (n,m)) * x = 0* n
let x be FinSequence of REAL ; ::_thesis: ( len x = m & n > 0 & m > 0 implies (0_Rmatrix (n,m)) * x = 0* n )
assume that
A1: len x = m and
A2: n > 0 and
A3: m > 0 ; ::_thesis: (0_Rmatrix (n,m)) * x = 0* n
A4: width (0_Rmatrix (n,m)) = m by A2, MATRIX_1:23;
then A5: len ((0_Rmatrix (n,m)) * x) = len (0_Rmatrix (n,m)) by A1, A3, Th61;
A6: len (0_Rmatrix (n,m)) = n by A2, MATRIX_1:23;
then (0_Rmatrix (n,m)) * x = ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) * x by A2, A4, Th36
.= ((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x) by A1, A2, A3, A6, A4, Th63 ;
then 0* n = (((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x)) - ((0_Rmatrix (n,m)) * x) by A6, A5, Th3;
hence (0_Rmatrix (n,m)) * x = 0* n by A5, Th14; ::_thesis: verum
end;
theorem :: MATRIXR1:66
for n, m being Element of NAT
for x being FinSequence of REAL st len x = n & n > 0 holds
x * (0_Rmatrix (n,m)) = 0* m
proof
let n, m be Element of NAT ; ::_thesis: for x being FinSequence of REAL st len x = n & n > 0 holds
x * (0_Rmatrix (n,m)) = 0* m
let x be FinSequence of REAL ; ::_thesis: ( len x = n & n > 0 implies x * (0_Rmatrix (n,m)) = 0* m )
assume that
A1: len x = n and
A2: n > 0 ; ::_thesis: x * (0_Rmatrix (n,m)) = 0* m
A3: len (0_Rmatrix (n,m)) = n by A2, MATRIX_1:23;
then A4: len (x * (0_Rmatrix (n,m))) = width (0_Rmatrix (n,m)) by A1, Th62;
A5: width (0_Rmatrix (n,m)) = m by A2, MATRIX_1:23;
then x * (0_Rmatrix (n,m)) = x * ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) by A2, A3, Th36
.= (x * (0_Rmatrix (n,m))) + (x * (0_Rmatrix (n,m))) by A1, A2, A5, A3, Th64 ;
then 0* m = ((x * (0_Rmatrix (n,m))) + (x * (0_Rmatrix (n,m)))) - (x * (0_Rmatrix (n,m))) by A5, A4, Th3;
hence x * (0_Rmatrix (n,m)) = 0* m by A4, Th14; ::_thesis: verum
end;