:: Matrix of $\mathbb Z$-module
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received February 18, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0, FUNCT_1,
XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4,
BINOP_2, RLSUB_2, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM,
ARYTM_1, NAT_1, FUNCT_2, FINSET_1, FUNCOP_1, VALUED_1, RLSUB_1, QC_LANG1,
ZFMISC_1, INT_1, RLVECT_2, INCSP_1, FINSEQ_2, FVSUM_1, ZMODUL01,
ZMODUL03, FINSEQ_4, RLVECT_3, RANKNULL, UNIALG_1, FUNCT_7, GROUP_1,
COMPLEX1, VECTSP_1, MESFUNC1, MATRLIN, FINSEQ_3, RVSUM_1, MATRIX_1,
MATRIX_3, LAPLACE, TREES_1, PRE_POLY, BILINEAR, FUNCT_5, HAHNBAN,
HAHNBAN1, ZMATRLIN, BORSUK_1, INT_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, DOMAIN_1, FUNCOP_1,
FUNCSDOM, VFUNCT_1, FINSET_1, CARD_1, FUNCT_5, NUMBERS, XCMPLX_0, INT_1,
XREAL_0, REAL_1, XXREAL_0, COMPLEX1, NAT_D, BINOP_2, FINSEQ_1, FINSEQ_2,
FINSEQOP, FINSEQ_3, MATRIX_0, STRUCT_0, ALGSTR_0, RLVECT_1, MATRIX_1,
FVSUM_1, GROUP_1, VECTSP_1, GR_CY_1, PRE_POLY, MATRLIN, VECTSP_2, MOD_2,
RLVECT_2, HAHNBAN, VECTSP_4, VECTSP_5, MATRIX_3, VECTSP_7, INT_3,
HAHNBAN1, ZMODUL01, ZMODUL03, ZMODUL05, VECTSP_6, LAPLACE, BILINEAR,
RANKNULL;
constructors BINOP_2, DOMAIN_1, REAL_1, GR_CY_1, EUCLID, VECTSP_9, FUNCT_3,
FVSUM_1, ALGSTR_1, ZMODUL05, MATRIXR2, LAPLACE, INT_3, VECTSP_2,
ZMODUL01, RLVECT_2, HAHNBAN1, VFUNCT_1, FUNCSDOM, VECTSP_4, VECTSP_6,
VECTSP_7, VECTSP_5, HAHNBAN, MOD_2, VECTSP_1, MATRIX_3, RELSET_1,
RANKNULL;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, STRUCT_0, RLVECT_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1,
XBOOLE_0, ORDINAL1, FUNCOP_1, XXREAL_0, NAT_1, RELAT_1, VECTSP_1,
ZFMISC_1, PRE_POLY, FUNCT_3, XCMPLX_0, ZMODUL03, MATRIX_0, INT_3,
MATRIX_6, HAHNBAN1, VECTSP_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, VECTSP_1, HAHNBAN1;
equalities BINOP_1, STRUCT_0, ALGSTR_0, VECTSP_1, FVSUM_1, SUBSET_1, LAPLACE,
MATRIX_0, VECTSP_6, INT_3, HAHNBAN1;
expansions TARSKI, BINOP_1, STRUCT_0, VECTSP_1, FUNCT_1, VECTSP_5, MOD_2,
HAHNBAN1;
theorems BINOP_1, CARD_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1,
FUNCT_2, INT_1, NAT_1, RLVECT_1, TARSKI, ZMODUL01, RLVECT_2, BINOP_2,
ZFMISC_1, RELAT_1, XTUPLE_0, ZMODUL03, PRE_POLY, XBOOLE_0, XBOOLE_1,
FUNCOP_1, XREAL_1, ORDINAL1, STRUCT_0, PARTFUN1, VECTSP_1, ZMODUL02,
NAT_D, NUMBERS, MATRLIN, GROUP_1, ABSVALUE, COMPLEX1, ZMODUL05, MATRIX_0,
MATRIXR2, MATRIX_3, PARTFUN2, LAPLACE, FUNCT_3, FINSEQOP, FVSUM_1,
DOMAIN_1, FUNCT_5, XXREAL_0, MATRIX_7, VECTSP_6, VECTSP_7, MATRIX_1,
MATRIX11, HAHNBAN1;
schemes BINOP_1, FINSEQ_1, FUNCT_2, NAT_1, MATRIX_0, FINSEQ_2, FINSEQ_4;
begin :: Preliminaries
reserve x,y,z for object,
i,j,k,l,n,m for Nat,
D,E for non empty set;
reserve M for Matrix of D;
reserve L for Matrix of E;
theorem EQ2:
for i, j being Nat st M = L & [i,j] in Indices M
holds M*(i,j) = L*(i,j)
proof
let i, j be Nat;
assume AS1: M = L & [i,j] in Indices M; then
consider p being FinSequence of D such that
A1: p = M.i & M*(i,j) = p.j by MATRIX_0:def 5;
consider q being FinSequence of E such that
A2: q = L.i & L*(i,j) = q.j by AS1,MATRIX_0:def 5;
thus M*(i,j) = L*(i,j) by AS1,A1,A2;
end;
theorem
for i being Nat st M = L & i in dom M
holds Line(M,i) = Line(L,i)
proof
let i be Nat;
assume AS1: M = L & i in dom M;
A1: len (Line(M,i)) = width M
& for j st j in Seg width M holds (Line(M,i)).j = M*(i,j)
by MATRIX_0:def 7;
A2: len (Line(L,i)) = width L
& for j st j in Seg width L holds (Line(L,i)).j = L*(i,j)
by MATRIX_0:def 7;
A3: dom (Line(M,i)) = Seg width M by A1,FINSEQ_1:def 3
.= dom (Line(L,i)) by AS1,A2,FINSEQ_1:def 3;
for j st j in dom (Line(M,i)) holds (Line(M,i)).j = (Line(L,i)).j
proof
let j;
assume j in dom (Line(M,i)); then
A4:j in Seg (width M) by A1,FINSEQ_1:def 3;
then [i,j] in Indices M by AS1,ZFMISC_1:87; then
A5: M*(i,j) = L*(i,j) by AS1,EQ2;
thus (Line(M,i)).j = M*(i,j) by A4,MATRIX_0:def 7
.= (Line(L,i)).j by AS1,A4,A5,MATRIX_0:def 7;
end;
hence thesis by A3;
end;
theorem
for i being Nat st M = L & i in Seg width M
holds Col(M,i) = Col(L,i)
proof
let i be Nat;
assume AS1: M = L & i in Seg width M;
A1: len (Col(M,i)) = len M
& for j st j in dom M holds (Col(M,i)).j = M*(j,i) by MATRIX_0:def 8;
A2: len (Col(L,i)) = len L
& for j st j in dom L holds (Col(L,i)).j = L*(j,i) by MATRIX_0:def 8;
A3: dom (Col(M,i)) = Seg len M by A1,FINSEQ_1:def 3
.= dom (Col(L,i)) by AS1,A2,FINSEQ_1:def 3;
for j st j in dom (Col(M,i))
holds (Col(M,i)).j = (Col(L,i)).j
proof
let j;
assume j in dom (Col(M,i));
then j in Seg len M by A1,FINSEQ_1:def 3; then
A4: j in dom M by FINSEQ_1:def 3;
then [j,i] in Indices M by AS1,ZFMISC_1:87; then
A5: M*(j,i) = L*(j,i) by AS1,EQ2;
thus (Col(M,i)).j = M*(j,i) by A4,MATRIX_0:def 8
.= (Col(L,i)).j by AS1,A4,A5,MATRIX_0:def 8;
end;
hence thesis by A3;
end;
theorem EQ40:
len M = len L & width M = width L &
(for i, j being Nat st [i,j] in Indices M holds M*(i,j) = L*(i,j))
implies M = L
proof
assume that
A1: len M = len L and
A2: width M = width L and
A3: for i,j be Nat st [i,j] in Indices M holds M*(i,j) = L*(i,j);
M is Matrix of E
proof
consider n be Nat such that
A0: for x being object st x in rng M holds
ex p being FinSequence of D st x = p & len p = n by MATRIX_0:9;
per cases;
suppose len M = 0;
then M = {};
then rng M c= E*;
hence thesis by FINSEQ_1:def 4;
end;
suppose I0: len M <> 0;
for x being object st x in rng M holds
ex p being FinSequence of E st x = p & len p = n
proof
let x being object;
assume S1: x in rng M;
then consider p being FinSequence of D such that
S3: x = p & len p = n by A0;
X1: width M = n by S1,S3,I0,MATRIX_0:def 3;
for z be object st z in rng p holds z in E
proof
let z be object;
assume z in rng p;
then consider j1 be object such that
S4: j1 in dom p & z = p.j1 by FUNCT_1:def 3;
S5: j1 in Seg n by S3,S4,FINSEQ_1:def 3;
reconsider j1 as Nat by S4;
consider i1 be object such that
S6: i1 in dom M & x = M.i1 by S1,FUNCT_1:def 3;
reconsider i1 as Nat by S6;
S8: [i1,j1] in Indices M by S6,S5,X1,ZFMISC_1:87;
then consider q being FinSequence of D such that
S9: q = M.i1 & M*(i1,j1) = q.j1 by MATRIX_0:def 5;
M*(i1,j1) = L*(i1,j1) by A3,S8;
hence z in E by S3,S4,S6,S9;
end;
then rng p c= E;
then reconsider p as FinSequence of E by FINSEQ_1:def 4;
take p;
thus x = p & len p = n by S3;
end;
hence M is Matrix of E by MATRIX_0:9;
end;
end;
then reconsider L0 = M as Matrix of E;
for i, j being Nat st [i,j] in Indices L0 holds L0*(i,j) = L*(i,j)
proof
let i, j be Nat;
assume X3: [i,j] in Indices L0;
then consider q be FinSequence of D such that
S9: q = M.i & M*(i,j) = q.j by MATRIX_0:def 5;
consider p be FinSequence of E such that
T9: p = L0.i & L0*(i,j) = p.j by X3,MATRIX_0:def 5;
thus L0*(i,j) = L*(i,j) by A3,S9,T9,X3;
end;
hence thesis by A1,A2,MATRIX_0:21;
end;
theorem REALTOINT:
for M being Matrix of D
st for i, j being Nat st [i, j] in Indices M holds M*(i,j) in E
holds M is Matrix of E
proof
let M be Matrix of D;
assume
AS: for i, j being Nat st [i, j] in Indices M holds M*(i,j) in E;
consider n be Nat such that
A0: for x being object st x in rng M holds
ex p being FinSequence of D st x = p & len p = n by MATRIX_0:9;
per cases;
suppose len M = 0;
then M = {};
then rng M c= E*;
hence thesis by FINSEQ_1:def 4;
end;
suppose I0: len M <> 0;
for x being object st x in rng M holds
ex p being FinSequence of E st x = p & len p = n
proof
let x be object;
assume S1: x in rng M;
then consider p be FinSequence of D such that
S3: x = p & len p = n by A0;
X1: width M = n by S1,S3,I0,MATRIX_0:def 3;
for z being object st z in rng p holds z in E
proof
let z be object;
assume z in rng p;
then consider j1 be object such that
S4: j1 in dom p & z = p.j1 by FUNCT_1:def 3;
S5: j1 in Seg n by S3,S4,FINSEQ_1:def 3;
reconsider j1 as Nat by S4;
consider i1 be object such that
S6: i1 in dom M & x = M.i1 by S1,FUNCT_1:def 3;
reconsider i1 as Nat by S6;
S8: [i1,j1] in Indices M by S6,S5,X1,ZFMISC_1:87;
then consider q being FinSequence of D such that
S9: q = M.i1 & M*(i1,j1) = q.j1 by MATRIX_0:def 5;
thus z in E by AS,S3,S4,S6,S8,S9;
end;
then rng p c= E;
then reconsider p as FinSequence of E by FINSEQ_1:def 4;
take p;
thus x = p & len p = n by S3;
end;
hence M is Matrix of E by MATRIX_0:9;
end;
end;
theorem
M = L implies M@ = L@
proof
assume AS: M = L;
for i, j being Nat st [i, j] in Indices M@ holds (M@)*(i,j) in E
proof
let i, j be Nat;
assume [i,j] in Indices M@; then
A2: [j,i] in Indices M by MATRIX_0:def 6;
then (M@)*(i,j) =M*(j,i) by MATRIX_0:def 6
.= L*(j,i) by AS,A2,EQ2;
hence (M@)*(i,j) in E;
end;
then
reconsider M1= (M@) as Matrix of E by REALTOINT;
P1: len (M1) = width L by AS,MATRIX_0:def 6;
P2: for i, j being Nat holds [i,j]
in Indices M1 iff [j,i] in Indices L by AS,MATRIX_0:def 6;
for i, j being Nat st [j,i] in Indices L holds (M1)*(i,j) = L*(j,i)
proof
let i, j be Nat;
assume A2: [j,i] in Indices L;
then [i,j] in Indices M@ by AS,MATRIX_0:def 6;
then (M1)*(i,j) =(M@)*(i,j) by EQ2
.= M*(j,i) by AS,A2,MATRIX_0:def 6;
hence (M1)*(i,j) = L*(j,i) by AS,A2,EQ2;
end;
hence thesis by P1,P2,MATRIX_0:def 6;
end;
theorem INTTOREAL:
for M being Matrix of INT
holds M is Matrix of REAL
proof
let M be Matrix of INT;
INT* c= REAL* by FINSEQ_1:62,NUMBERS:15;
then rng M c= REAL*;
hence thesis by FINSEQ_1:def 4;
end;
definition
let M be Matrix of INT;
func inttorealM(M) -> Matrix of REAL equals
M;
correctness by INTTOREAL;
end;
definition
let n, m be Nat;
let M be Matrix of n,m,INT;
redefine func inttorealM(M) -> Matrix of n,m,REAL; :: redefines inttorealM (ZMATRLIN, definition)
correctness
proof
B2:len M = n by MATRIX_0:25;
per cases;
suppose X11: not 0 < n; then
X1: n = 0;
M = {} by B2,X11;
hence inttorealM(M) is Matrix of n,m,REAL by X1,MATRIX_0:13;
end;
suppose X2: 0 < n;
then width M = m by B2,MATRIX_0:20;
hence inttorealM(M) is Matrix of n, m, REAL by X2,B2,MATRIX_0:20;
end;
end;
end;
definition
let n be Nat;
let M be Matrix of n,INT;
redefine func inttorealM(M) -> Matrix of n,REAL; :: redefines inttorealM (ZMATRLIN, definition)
correctness
proof
inttorealM(M) is Matrix of n,n,REAL;
hence thesis;
end;
end;
definition
let M be Matrix of REAL;
attr M is integer means
M is Matrix of INT;
end;
registration
cluster integer for Matrix of REAL;
correctness
proof
set M = the Matrix of INT;
reconsider L = inttorealM(M) as Matrix of REAL;
take L;
thus L is Matrix of INT;
end;
end;
registration
let n, m be Nat;
cluster integer for Matrix of n,m, REAL;
correctness
proof
set M = the Matrix of n,m,INT;
reconsider L = inttorealM(M) as Matrix of n,m,REAL;
take L;
thus thesis;
end;
end;
definition
let M be integer Matrix of REAL;
func realtointM(M) -> Matrix of INT equals
M;
correctness
proof
M is integer;
then reconsider L = M as Matrix of INT;
L = M;
hence thesis;
end;
end;
definition
let n, m be Nat;
let M be integer Matrix of n,m, REAL;
redefine func realtointM(M) -> Matrix of n,m,INT; :: redefines realtointM (ZMATRLIN, definition)
correctness
proof
B2:len M = n by MATRIX_0:25;
per cases;
suppose X11: not 0 < n; then
X1: n = 0;
M = {} by B2,X11;
hence realtointM(M) is Matrix of n,m,INT by X1,MATRIX_0:13;
end;
suppose X2: 0 < n;
then width M = m by B2,MATRIX_0:20;
hence realtointM(M) is Matrix of n, m, INT by X2,B2,MATRIX_0:20;
end;
end;
end;
definition
let n be Nat;
let M be integer Matrix of n, REAL;
redefine func realtointM(M) -> Matrix of n,INT; :: redefines realtointM (ZMATRLIN, definition)
correctness
proof
realtointM(M) is Matrix of n,n,INT;
hence thesis;
end;
end;
definition
let n, m be Nat;
func 0.(n,m) -> Matrix of n,m,INT.Ring equals
n |-> (m |-> 0.INT.Ring);
correctness by MATRIX_0:10;
end;
begin :: Sequences and Matrices Concerning Linear Transformations
reserve k,t,i,j,m,n for Nat,
D for non empty set;
reserve V for free Z_Module;
reserve a for Element of INT.Ring,
W for Element of V;
reserve KL1,KL2,KL3 for Linear_Combination of V,
X for Subset of V;
Th5:
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X &
Sum KL1 = Sum KL2 implies KL1 = KL2 by ZMODUL03:3;
theorem Th6:
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X
& Carrier KL3 c= X & Sum KL1 = Sum KL2 + Sum KL3 implies KL1 = KL2 + KL3
proof
assume that
A1: X is linearly-independent & Carrier KL1 c= X and
A2: Carrier KL2 c= X & Carrier KL3 c= X and
A3: Sum KL1 = Sum(KL2) + Sum(KL3);
Carrier(KL2 + KL3) c= Carrier(KL2) \/ Carrier(KL3) &
Carrier(KL2) \/ Carrier (KL3) c= X by A2,XBOOLE_1:8,ZMODUL02:26;
then
A4: Carrier(KL2 + KL3) c= X;
Sum(KL1) = Sum(KL2 + KL3) by A3,ZMODUL02:52;
hence thesis by A1,A4,Th5;
end;
theorem Th7:
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X
& a <> 0.INT.Ring & Sum KL1 = a * Sum KL2 implies KL1 = a * KL2
proof
assume that
A1: X is linearly-independent & Carrier KL1 c= X and
A2: Carrier KL2 c= X & a <> 0.INT.Ring & Sum(KL1) = a * Sum(KL2);
Carrier(a * KL2) c= X & Sum(KL1) = Sum(a * KL2)
by A2,ZMODUL02:29,53;
hence thesis by A1,Th5;
end;
reserve V for finite-rank free Z_Module,
W for Element of V;
reserve KL1,KL2,KL3 for Linear_Combination of V,
X for Subset of V;
theorem Th8:
for b2 be Basis of V ex KL be Linear_Combination of V
st W = Sum KL & Carrier KL c= b2
proof
let b2 be Basis of V;
W in the ModuleStr of V;
then W in Lin b2 by VECTSP_7:def 3;
then consider KL1 being Linear_Combination of b2 such that
A1: W = Sum KL1 by ZMODUL02:64;
take KL = KL1;
thus W = Sum KL by A1;
thus thesis by VECTSP_6:def 4;
end;
definition
let V be finite-rank free Z_Module;
mode OrdBasis of V -> FinSequence of V means
:defOrdBasis:
it is one-to-one & rng it is Basis of V;
existence
proof
consider A be finite Subset of V such that
A1: A is Basis of V by ZMODUL03:def 3;
consider p be FinSequence such that
A2: rng p = A and
A3: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of V by A2,FINSEQ_1:def 4;
take f = p;
thus f is one-to-one by A3;
thus thesis by A1,A2;
end;
end;
reserve s for FinSequence,
V1,V2,V3 for finite-rank free Z_Module,
f,f1,f2 for Function of V1,V2,
g for Function of V2,V3,
b1 for OrdBasis of V1,
b2 for OrdBasis of V2,
b3 for OrdBasis of V3,
v1,v2 for Vector of V2,
v,w for Element of V1;
reserve p2,F for FinSequence of V1,
p1,d for FinSequence of INT.Ring,
KL for Linear_Combination of V1;
theorem Th9:
for a being Element of V1, F being FinSequence of V1,
G being FinSequence of INT.Ring st len F = len G &
for k for v being Element of INT.Ring st
k in dom F & v = G.k holds F.k = v * a
holds Sum(F) = Sum(G) * a
proof
let a be Element of V1;
let F be FinSequence of V1;
let G be FinSequence of INT.Ring;
defpred P[Nat] means for H being FinSequence of V1,
I being FinSequence of INT.Ring
st len H = len I & len H = $1 &
(for k for v be Element of INT.Ring st k in dom H & v = I.k holds
H.k = v * a )
holds Sum(H) = Sum(I) * a;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: for H being FinSequence of V1, I being FinSequence of INT.Ring
st len H = len I & len H = n &
(for k for v being Element of INT.Ring st k in dom H & v = I.k
holds H.k = v * a)
holds Sum(H) = Sum(I) * a;
let H be FinSequence of V1, I be FinSequence of INT.Ring;
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k for v being Element of INT.Ring st k in dom H & v = I.k holds
H.k = v * a;
reconsider q = I | (Seg n) as FinSequence of INT.Ring by FINSEQ_1:18;
reconsider p = H | (Seg n) as FinSequence of V1 by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then
A7: len p = n by A4,FINSEQ_1:17;
A8: dom p = Seg n by A4,A6,FINSEQ_1:17;
A9: len q = n by A3,A4,A6,FINSEQ_1:17;
A10: dom q = Seg n by A3,A4,A6,FINSEQ_1:17;
A11:
now
len p <= len H by A4,A6,FINSEQ_1:17;
then
A12: dom p c= dom H by FINSEQ_3:30;
let k;
let v be Element of INT.Ring;
assume that
A13: k in dom p and
A14: v = q.k;
I.k = q.k by A8,A10,A13,FUNCT_1:47;
then H.k = v * a by A5,A13,A14,A12;
hence p.k = v * a by A13,FUNCT_1:47;
end;
reconsider n as Element of NAT by ORDINAL1:def 12;
n + 1 in Seg(n + 1) by FINSEQ_1:4; then
A15: n + 1 in dom H by A4,FINSEQ_1:def 3;
then reconsider v1 = H.(n + 1) as Element of V1 by FINSEQ_2:11;
reconsider v2 = I.(n + 1) as Element of INT.Ring by INT_1:def 2;
A16: v1 = v2 * a by A5,A15;
A17: I = q ^<*v2*> by A3,A4,FINSEQ_3:55;
thus Sum(H) = Sum(p) + v1 by A4,A7,A8,RLVECT_1:38
.= Sum(q) * a + v2 * a by A2,A7,A9,A11,A16
.= (Sum(q) + v2) * a by VECTSP_1:def 15
.= Sum(I) * a by A17,FVSUM_1:71;
end;
A17: P[0]
proof
let H be FinSequence of V1, I be FinSequence of INT.Ring;
assume that
A18: len H = len I and
A19: len H = 0 and
for k for v being Element of INT.Ring st k in dom H & v = I.k holds
H.k = v * a;
H = <*>(the carrier of V1) by A19;
then
A20: Sum(H) = 0.V1 by RLVECT_1:43;
I = <*>(the carrier of INT.Ring) by A18,A19; then
Sum I = 0.INT.Ring by RLVECT_1:43; then
(Sum I) * a = 0.V1 by VECTSP_1:14;
hence thesis by A20;
end;
for n holds P[n] from NAT_1:sch 2(A17,A1);
hence thesis;
end;
theorem Th10:
for a being Element of V1, F being FinSequence of INT.Ring,
G being FinSequence of V1 st len F = len G &
for k st k in dom F holds G.k = (F/.k) * a
holds Sum(G) = Sum(F) * a
proof
let a be Element of V1;
let F be FinSequence of INT.Ring;
let G be FinSequence of V1;
assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = (F/.k) * a;
now
let k;
let v be Element of INT.Ring;
assume that
A3: k in dom G and
A4: v = F.k;
A5: k in dom F by A1,A3,FINSEQ_3:29;
then v = F/.k by A4,PARTFUN1:def 6;
hence G.k = v * a by A2,A5;
end;
hence thesis by A1,Th9;
end;
definition
let V1, p1, p2;
func lmlt(p1,p2) -> FinSequence of V1 equals
(the lmult of V1).:(p1,p2);
coherence;
end;
theorem Th12:
dom p1 = dom p2 implies dom lmlt(p1,p2) = dom p1
proof
assume
A1: dom p1 = dom p2;
A2: [:rng p1,rng p2:] c= [:INT,the carrier of V1:] by ZFMISC_1:96;
A3: rng <:p1,p2:> c= [:rng p1,rng p2:] &
[:INT,the carrier of V1:] = dom (the lmult of V1)
by FUNCT_2:def 1,FUNCT_3:51;
thus dom lmlt(p1,p2) = dom((the lmult of V1)*<:p1,p2:> ) by FUNCOP_1:def 3
.= dom <:p1,p2:> by A2,A3,RELAT_1:27,XBOOLE_1:1
.= dom p1 /\ dom p2 by FUNCT_3:def 7
.= dom p1 by A1;
end;
theorem Th13:
for M being Matrix of the carrier of V1 st len M = 0 holds Sum Sum M = 0.V1
proof
let M be Matrix of the carrier of V1;
assume len M = 0;
then len Sum M = 0 by MATRLIN:def 6;
then Sum M = <*>(the carrier of V1);
hence thesis by RLVECT_1:43;
end;
theorem Th14:
for M being Matrix of m+1,0,the carrier of V1 holds Sum Sum M = 0.V1
proof
let M be Matrix of m+1,0,the carrier of V1;
for k st k in dom Sum M holds (Sum M)/.k = 0.V1
proof
let k such that
A1: k in dom Sum M;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
len M = len Sum M by MATRLIN:def 6;
then dom M = dom Sum M by FINSEQ_3:29;
then M/.k1 in rng M by A1,PARTFUN2:2;
then len(M/.k) = 0 by MATRIX_0:def 2;
then
A2: M/.k = <*>(the carrier of V1);
thus (Sum M)/.k = Sum (M/.k) by A1,MATRLIN:def 6
.= 0.V1 by A2,RLVECT_1:43;
end;
hence thesis by MATRLIN:11;
end;
theorem Th16:
for V1, V2 being Z_Module, f being Function of V1, V2,
p being FinSequence of V1 st f is additive homogeneous holds
f.Sum p = Sum(f*p)
proof
let V1, V2 be Z_Module, f be Function of V1, V2;
let p be FinSequence of V1;
defpred P[FinSequence of V1] means f.Sum($1) = Sum(f*$1);
assume
A1: f is additive homogeneous;
A2: for p being FinSequence of V1 for w being Element of V1 st P[p] holds
P[p^<*w*>]
proof
let p be FinSequence of V1;
let w be Element of V1 such that
A3: f.Sum p = Sum (f*p);
thus f.Sum(p^<*w*>) = f.(Sum(p) + Sum<*w*>) by RLVECT_1:41
.= Sum(f*p) + f.Sum<*w*> by A1,A3
.= Sum(f*p) + f.w by RLVECT_1:44
.= Sum(f*p) + Sum<*f.w*> by RLVECT_1:44
.= Sum(f*p^<*f.w*>) by RLVECT_1:41
.= Sum(f*(p^<*w*>)) by FINSEQOP:8;
end;
set I0 = 0.INT.Ring;
f.Sum(<*>(the carrier of V1)) = f.(0.V1) by RLVECT_1:43
.= f.(I0* 0.V1) by ZMODUL01:1
.= I0 * f.(0.V1) by A1
.= 0.V2 by ZMODUL01:1
.= Sum(<*>(the carrier of V2)) by RLVECT_1:43
.= Sum(f*<*>(the carrier of V1));
then
A4: P[<*>(the carrier of V1)];
for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A4,A2);
hence thesis;
end;
theorem Th17:
for a being FinSequence of INT.Ring, p being FinSequence of V1
st len p = len a holds f is additive homogeneous
implies f*lmlt(a,p) = lmlt(a,f*p)
proof
let a be FinSequence of INT.Ring, p be FinSequence of V1;
assume len p = len a;
then
A1: dom p = dom a by FINSEQ_3:29;
dom f = the carrier of V1 by FUNCT_2:def 1;
then rng p c= dom f;
then
A2: dom p = dom (f*p) by RELAT_1:27;
assume
A3: f is additive homogeneous;
A4:
now
set P = f*p;
let k be Nat;
assume
A5: k in dom (f*lmlt(a,p));
A6: dom (f*lmlt(a,p)) c= dom lmlt(a,p) by RELAT_1:25;
then k in dom lmlt(a,p) by A5;
then
A7: k in dom p by A1,Th12;
then
A8: p/.k = p.k by PARTFUN1:def 6;
A9: k in dom lmlt(a,f*p) by A1,A2,A7,Th12;
A10: a/.k = a.k by A1,A7,PARTFUN1:def 6;
A11: P/.k = (f*p).k by A2,A7,PARTFUN1:def 6;
thus (f*lmlt(a,p)).k = f.(lmlt(a,p).k) by A5,FUNCT_1:12
.= f.((a/.k)*(p/.k)) by A10,A8,A5,A6,FUNCOP_1:22
.= (a/.k)*(f.(p/.k)) by A3
.= (a/.k)*(P/.k) by A7,A8,A11,FUNCT_1:13
.= lmlt(a,f*p).k by A9,A10,A11,FUNCOP_1:22;
end;
dom lmlt(a,p) = dom p by A1,Th12
.= dom lmlt(a,f*p) by A1,A2,Th12;
then len lmlt(a,p) = len lmlt(a,f*p) by FINSEQ_3:29;
then len (f*lmlt(a,p)) = len lmlt(a,f*p) by FINSEQ_2:33;
hence thesis by A4,FINSEQ_2:9;
end;
theorem Th18:
for a being FinSequence of INT.Ring
st len a = len b2 & g is additive homogeneous holds
g.Sum(lmlt(a,b2)) = Sum(lmlt(a,g*b2))
proof
let a be FinSequence of INT.Ring such that
A1: len a = len b2 and
A2: g is additive homogeneous;
thus g.Sum(lmlt(a,b2)) = Sum(g*lmlt(a,b2)) by A2,Th16
.= Sum(lmlt(a,g*b2)) by A1,A2,Th17;
end;
theorem Th19:
for F, F1 being FinSequence of V1, KL being Linear_Combination of V1,
p being Permutation of dom F st F1 = F * p holds KL (#) F1 = (KL (#) F) * p
proof
let F, F1 be FinSequence of V1;
let KL be Linear_Combination of V1;
let p be Permutation of dom F such that
A1: F1 = F * p;
dom F = Seg len F by FINSEQ_1:def 3;
then dom F = Seg len (KL (#) F) by VECTSP_6:def 5;
then
A2: dom F = dom (KL (#) F) by FINSEQ_1:def 3;
then reconsider F2 = (KL (#) F) * p as FinSequence of V1 by FINSEQ_2:47;
A31: len (KL (#) F1) = len F1 by VECTSP_6:def 5
.= len F by A1,FINSEQ_2:44
.= len (KL (#) F) by VECTSP_6:def 5
.= len F2 by A2,FINSEQ_2:44;
then
A3: dom (KL (#) F1) = dom ((KL (#) F) * p) by FINSEQ_3:29;
len (KL (#) F1) = len F1 by VECTSP_6:def 5;
then
A4: dom (KL (#) F1) = dom F1 by FINSEQ_3:29;
now
let k be Nat;
reconsider k0 = k as Element of NAT by ORDINAL1:def 12;
assume
A5: k in dom (KL (#) F1);
then k in dom p by A3,FUNCT_1:11;
then A6: p.k in rng p by FUNCT_1:def 3;
then p.k in dom F;
then reconsider k1 = p.k0 as Element of NAT;
F1/.k = F1.k by A4,A5,PARTFUN1:def 6
.= F.(p.k) by A1,A4,A5,FUNCT_1:12
.= F/.(p.k) by A6,PARTFUN1:def 6;
hence (KL (#) F1).k = KL.(F/.k1) * (F/.k1) by A5,VECTSP_6:def 5
.= (KL (#) F).k1 by A2,A6,VECTSP_6:def 5
.= F2.k by A3,A5,FUNCT_1:12;
end;
hence thesis by A31,FINSEQ_3:29;
end;
theorem Th20:
F is one-to-one & Carrier KL c= rng F implies Sum(KL (#) F) = Sum KL
proof
assume
A1: F is one-to-one;
assume
A2: Carrier KL c= rng F;
then reconsider A = Carrier KL as Subset of rng F;
consider p1 be Permutation of dom F such that
A3: (F-A`)^(F-A) = F * p1 by FINSEQ_3:115;
reconsider G1 = F - A`, G2 = F - A as FinSequence of V1 by FINSEQ_3:86;
A4: G1 is one-to-one by A1,FINSEQ_3:87;
len (KL (#) F) = len F by VECTSP_6:def 5;
then dom (KL (#) F) = dom F by FINSEQ_3:29;
then reconsider p1 as Permutation of dom (KL (#) F);
A5: rng G1 = rng F \ A` by FINSEQ_3:65
.= rng F /\ Carrier KL by XBOOLE_1:48
.= Carrier KL by A2,XBOOLE_1:28;
for k st k in dom (KL (#) G2) holds (KL (#) G2)/.k = 0.V1
proof
let k such that
A6: k in dom (KL (#) G2);
len (KL (#) G2) = len G2 by VECTSP_6:def 5;
then
A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:29;
then G2.k in rng G2 by A6,FUNCT_1:def 3;
then G2.k in rng F \ Carrier KL by FINSEQ_3:65;
then not G2.k in Carrier KL by XBOOLE_0:def 5;
then
A8: not G2/.k in Carrier KL by A6,A7,PARTFUN1:def 6;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
thus (KL (#) G2)/.k = (KL (#) G2).k by A6,PARTFUN1:def 6
.= KL.(G2/.k1) * (G2/.k1) by A6,VECTSP_6:def 5
.= 0.INT.Ring * (G2/.k) by A8
.= 0.V1 by ZMODUL01:1;
end;
then
A9: Sum(KL (#) G2) = 0.V1 by MATRLIN:11;
KL (#) (G1^G2) = (KL (#) F) * p1 by A3,Th19;
hence Sum(KL (#) F) = Sum(KL (#) (G1 ^ G2)) by RLVECT_2:7
.= Sum((KL (#) G1) ^ (KL (#) G2)) by ZMODUL02:51
.= Sum(KL (#) G1) + Sum(KL (#) G2) by RLVECT_1:41
.= Sum KL by A4,A5,A9,VECTSP_6:def 6;
end;
theorem Th21:
for A being set, p being FinSequence of V1 st rng p c= A holds
f1 is additive homogeneous & f2 is additive homogeneous &
(for v st v in A holds f1.v = f2.v) implies f1.Sum p = f2.Sum p
proof
let A be set;
let p be FinSequence of V1 such that
A1: rng p c= A;
defpred P[FinSequence of V1] means rng $1 c= A implies
f1.Sum($1) = f2.Sum($1);
assume that
A2: f1 is additive homogeneous and
A3: f2 is additive homogeneous;
assume
A4: for v st v in A holds f1.v = f2.v;
A5: for p being FinSequence of V1, x being Element of V1 st P[p]
holds P[p^<*x*>]
proof
let p be FinSequence of V1, x be Element of V1 such that
A6: rng p c= A implies f1.Sum p = f2.Sum p;
A7: rng p c= rng p \/ rng <*x*> by XBOOLE_1:7;
assume rng (p^<*x*>) c= A;
then
A8: rng p \/ rng <*x*> c= A by FINSEQ_1:31;
rng <*x*> c= rng p \/ rng <*x*> by XBOOLE_1:7;
then rng <*x*> c= A by A8;
then A9: {x} c= A by FINSEQ_1:39;
thus f1.Sum(p^<*x*>) = f1.(Sum(p) + Sum(<*x*>)) by RLVECT_1:41
.= f2.(Sum p) + f1.(Sum(<*x*>)) by A2,A6,A8,A7
.= f2.(Sum p) + f1.x by RLVECT_1:44
.= f2.(Sum p) + f2.x by A4,A9,ZFMISC_1:31
.= f2.(Sum p) + f2.(Sum(<*x*>)) by RLVECT_1:44
.= f2.(Sum(p) + Sum(<*x*>)) by A3
.= f2.Sum(p^<*x*>) by RLVECT_1:41;
end;
A10: P[<*>(the carrier of V1)]
proof
assume rng<*>(the carrier of V1) c= A;
set I0 = 0.INT.Ring;
thus f1.Sum(<*>(the carrier of V1)) = f1.(0.V1) by RLVECT_1:43
.= f1.(I0* 0.V1) by ZMODUL01:1
.= I0* f1.(0.V1) by A2
.= 0.V2 by ZMODUL01:1
.= I0* f2.(0.V1) by ZMODUL01:1
.= f2.(I0* 0.V1) by A3
.= f2.(0.V1) by ZMODUL01:1
.= f2.Sum(<*>(the carrier of V1)) by RLVECT_1:43;
end;
for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A10,A5);
hence thesis by A1;
end;
theorem Th22:
f1 is additive homogeneous & f2 is additive homogeneous implies
for b1 being OrdBasis of V1 st len b1 > 0 holds f1*b1 = f2*b1
implies f1 = f2
proof
assume that
A1: f1 is additive homogeneous and
A2: f2 is additive homogeneous;
let b1 be OrdBasis of V1 such that
A3: len b1 > 0;
reconsider b = rng b1 as Basis of V1 by defOrdBasis;
assume
A4: f1*b1 = f2*b1;
now
len b1 in Seg len b1 by A3,FINSEQ_1:3;
then reconsider D = dom b1 as non empty set by FINSEQ_1:def 3;
let v be Element of V1;
Lin(b) = the ModuleStr of V1 by VECTSP_7:def 3;
then v in Lin(b);
then consider KL be Linear_Combination of b such that
A5: v = Sum(KL) by ZMODUL02:64;
set p = KL (#) b1;
set A = the set of all KL.(b1/.i)*(b1/.i) where i is Element of D;
A6: rng p c= A
proof
let x be object;
assume x in rng p;
then consider i be Nat such that
A7: i in dom p and
A8: p.i = x by FINSEQ_2:10;
dom p = Seg len p by FINSEQ_1:def 3;
then i in Seg len b1 by A7,VECTSP_6:def 5;
then
A9: i in dom b1 by FINSEQ_1:def 3;
(KL (#) b1).i = KL.(b1/.i) * (b1/.i) by A7,VECTSP_6:def 5;
hence thesis by A8,A9;
end;
A10: for w st w in A holds f1.w = f2.w
proof
let w;
assume w in A;
then consider i be Element of D such that
A11: w = KL.(b1/.i)*(b1/.i);
f1.(b1/.i) = f1.(b1.i) by PARTFUN1:def 6
.= (f2*b1).i by A4,FUNCT_1:13
.= f2.(b1.i) by FUNCT_1:13
.= f2.(b1/.i) by PARTFUN1:def 6;
then f1.(KL.(b1/.i)*(b1/.i)) = KL.(b1/.i)*(f2.(b1/.i)) by A1
.= f2.(KL.(b1/.i)*(b1/.i)) by A2;
hence thesis by A11;
end;
A12: b1 is one-to-one & Carrier KL c= rng b1
by defOrdBasis,VECTSP_6:def 4;
hence f1.v = f1.Sum(KL (#) b1) by A5,Th20
.= f2.Sum p by A1,A2,A6,A10,Th21
.= f2.v by A5,A12,Th20;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th27:
for M1 being Matrix of n,k,the carrier of V,
M2 being Matrix of m,k,the carrier of V
holds Sum(M1^M2) = (Sum M1)^(Sum M2)
proof
let M1 be Matrix of n,k,the carrier of V;
let M2 be Matrix of m,k,the carrier of V;
A1: dom Sum(M1^M2) = Seg len Sum(M1^M2) by FINSEQ_1:def 3;
A2:
now
let i be Nat;
assume
A3: i in dom Sum(M1^M2);
then i in Seg len (M1^M2) by A1,MATRLIN:def 6;
then
A4: i in dom (M1^M2) by FINSEQ_1:def 3;
now
per cases by A4,FINSEQ_1:25;
suppose A5: i in dom M1;
len M1 = len Sum M1 by MATRLIN:def 6;
then
A6: dom M1 = dom Sum M1 by FINSEQ_3:29;
thus Sum(M1^M2).i = (Sum(M1^M2))/.i by A3,PARTFUN1:def 6
.= Sum ((M1^M2)/.i) by A3,MATRLIN:def 6
.= Sum (M1/.i) by A5,FINSEQ_4:68
.= (Sum M1)/.i by A5,A6,MATRLIN:def 6
.= (Sum M1).i by A5,A6,PARTFUN1:def 6
.= ((Sum M1)^(Sum M2)).i by A5,A6,FINSEQ_1:def 7;
end;
suppose A7: ex n being Nat st n in dom M2 & i = len M1 + n;
A8: len M1 = len Sum M1 by MATRLIN:def 6;
len M2 = len Sum M2 by MATRLIN:def 6;
then
A9: dom M2 = dom Sum M2 by FINSEQ_3:29;
consider n be Nat such that
A10: n in dom M2 and
A11: i = len M1 + n by A7;
thus Sum(M1^M2).i = (Sum(M1^M2))/.i by A3,PARTFUN1:def 6
.= Sum ((M1^M2)/.i) by A3,MATRLIN:def 6
.= Sum (M2/.n) by A10,A11,FINSEQ_4:69
.= (Sum M2)/.n by A10,A9,MATRLIN:def 6
.= (Sum M2).n by A10,A9,PARTFUN1:def 6
.= ((Sum M1)^(Sum M2)).i by A10,A11,A8,A9,FINSEQ_1:def 7;
end;
end;
hence Sum(M1^M2).i = ((Sum M1)^(Sum M2)).i;
end;
len Sum(M1^M2) = len (M1^M2) by MATRLIN:def 6
.= len M1 + len M2 by FINSEQ_1:22
.= len Sum M1 + len M2 by MATRLIN:def 6
.= len Sum M1 + len Sum M2 by MATRLIN:def 6
.= len ((Sum M1)^(Sum M2)) by FINSEQ_1:22;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th29:
for M1,M2 being Matrix of the carrier of V1 holds
Sum M1 + Sum M2 = Sum(M1 ^^ M2)
proof
let M1, M2 be Matrix of the carrier of V1;
reconsider m = min(len M1,len M2) as Element of NAT by ORDINAL1:def 12;
A1: Seg m = Seg len M1 /\ Seg len M2 by FINSEQ_2:2
.= Seg len M1 /\ dom M2 by FINSEQ_1:def 3
.= dom M1 /\ dom M2 by FINSEQ_1:def 3
.= dom (M1 ^^ M2) by PRE_POLY:def 4
.= Seg len (M1 ^^ M2) by FINSEQ_1:def 3;
A2: len (Sum M1+Sum M2) = min(len Sum M1,len Sum M2) by FINSEQ_2:71
.= min(len M1,len Sum M2) by MATRLIN:def 6
.= min(len M1,len M2) by MATRLIN:def 6
.= len (M1 ^^ M2) by A1,FINSEQ_1:6
.= len Sum(M1 ^^ M2) by MATRLIN:def 6;
A3: dom (Sum M1 + Sum M2) = Seg len(Sum M1 + Sum M2) by FINSEQ_1:def 3;
now
let i be Nat;
assume
A4: i in dom (Sum M1+Sum M2);
then
A5: i in dom Sum(M1 ^^ M2) by A2,A3,FINSEQ_1:def 3;
i in Seg len (M1 ^^ M2) by A2,A3,A4,MATRLIN:def 6;
then
A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3;
then
A7: i in dom M1 /\ dom M2 by PRE_POLY:def 4;
then
A8: i in dom M1 by XBOOLE_0:def 4;
A9: i in dom M2 by A7,XBOOLE_0:def 4;
reconsider m1 = M1.i,m2 = M2.i as FinSequence;
A10: ((M1/.i) ^ (M2/.i)) = m1 ^ (M2/.i) by A8,PARTFUN1:def 6
.= m1 ^ m2 by A9,PARTFUN1:def 6
.= (M1 ^^ M2).i by A6,PRE_POLY:def 4
.= (M1 ^^ M2)/.i by A6,PARTFUN1:def 6;
i in Seg len M2 by A9,FINSEQ_1:def 3;
then i in Seg len (Sum M2) by MATRLIN:def 6;
then
A11: i in dom (Sum M2) by FINSEQ_1:def 3;
then
A12: (Sum M2)/.i = (Sum M2).i by PARTFUN1:def 6;
i in Seg len M1 by A8,FINSEQ_1:def 3;
then i in Seg len (Sum M1) by MATRLIN:def 6;
then
A13: i in dom (Sum M1) by FINSEQ_1:def 3;
then (Sum M1)/.i = (Sum M1).i by PARTFUN1:def 6;
hence (Sum M1 + Sum M2).i = ((Sum M1)/.i) + ((Sum M2)/.i)
by A4,A12,FUNCOP_1:22
.= Sum (M1/.i) + (Sum M2/.i) by A13,MATRLIN:def 6
.= Sum (M1/.i) + Sum (M2/.i) by A11,MATRLIN:def 6
.= Sum ((M1 ^^ M2)/.i) by A10,RLVECT_1:41
.= Sum(M1 ^^ M2)/.i by A5,MATRLIN:def 6
.= (Sum(M1 ^^ M2)).i by A5,PARTFUN1:def 6;
end;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th30:
for P1,P2 being FinSequence of V1 st len P1 = len P2 holds
Sum(P1 + P2) = (Sum P1) + (Sum P2)
proof
let P1, P2 be FinSequence of V1;
assume len P1 = len P2;
then reconsider R1 = P1, R2 = P2
as Element of (len P1) -tuples_on the carrier of V1 by FINSEQ_2:92;
thus Sum (P1 + P2) = Sum (R1 + R2)
.= (Sum P1) + (Sum P2) by FVSUM_1:76;
end;
theorem Th31:
for M1, M2 being Matrix of the carrier of V1 st len M1 = len M2
holds Sum Sum M1 + Sum Sum M2 = Sum Sum(M1 ^^ M2)
proof
let M1, M2 be Matrix of the carrier of V1 such that
A1: len M1 = len M2;
len Sum M1 = len M1 by MATRLIN:def 6
.= len Sum M2 by A1,MATRLIN:def 6;
hence Sum Sum M1 + Sum Sum M2 = Sum (Sum M1 + Sum M2) by Th30
.= Sum Sum(M1 ^^ M2) by Th29;
end;
theorem Th32:
for M being Matrix of the carrier of V1 holds Sum Sum M = Sum Sum (M@)
proof
defpred X[Nat] means for M being Matrix of the carrier of V1 st len M = $1
holds Sum Sum M = Sum Sum (M@);
let M be Matrix of the carrier of V1;
A1: for P being FinSequence of V1 holds Sum Sum <*P*> = Sum Sum (<*P*>@)
proof
defpred X[FinSequence of V1] means Sum Sum <*$1*> = Sum Sum(<*$1*>@);
let P be FinSequence of V1;
len <*<*>(the carrier of V1)*> = 1 by MATRIX_0:def 2;
then width <*<*>(the carrier of V1)*> = 0 by MATRIX_0:20;
then
A2: len (<*<*>(the carrier of V1)*>@) = 0 by MATRIX_0:def 6;
A3: for P being FinSequence of V1, x being Element of V1 st X[P]
holds X[P^<*x*>]
proof
let P be FinSequence of V1, x be Element of V1 such that
A4: Sum Sum <*P*> = Sum Sum (<*P*>@);
Seg len (<*P*> ^^ <*<*x*>*>) = dom (<*P*> ^^ <*<*x*>*>)
by FINSEQ_1:def 3
.= dom <*P*> /\ dom <*<*x*>*> by PRE_POLY:def 4
.= Seg 1 /\ dom <*<*x*>*> by FINSEQ_1:38
.= Seg 1 /\ Seg 1 by FINSEQ_1:38
.= Seg 1;
then
A5: len (<*P*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6
.= len <*P^<*x*>*> by FINSEQ_1:39;
then
A6: dom (<*P*> ^^ <*<*x*>*>) = Seg len <*P^<*x*>*> by FINSEQ_1:def 3;
A7:
now
let i be Nat;
assume
A8: i in dom (<*P*> ^^ <*<*x*>*>);
then i in { 1 } by A6,FINSEQ_1:2,40;
then
A9: i = 1 by TARSKI:def 1;
reconsider m1 = <*P*>.i, m2 = <*<*x*>*>.i as FinSequence;
thus (<*P*> ^^ <*<*x*>*>).i = m1 ^ m2 by A8,PRE_POLY:def 4
.= P ^ m2 by A9
.= P ^ <*x*> by A9
.= <*P^<*x*>*>.i by A9;
end;
per cases;
suppose len P = 0;
then
A10: P = {};
hence Sum Sum <*P^<*x*>*> = Sum Sum <*<*x*>*> by FINSEQ_1:34
.= Sum Sum (<*<*x*>*>@) by MATRLIN:15
.= Sum Sum (<*P^<*x*>*>@) by A10,FINSEQ_1:34;
end;
suppose A11: len P <> 0;
A12: len <*<*x*>*> = 1 by FINSEQ_1:40;
then
A13: width <*<*x*>*> = len <*x*> by MATRIX_0:20
.= 1 by FINSEQ_1:40;
then
A14: len (<*<*x*>*>@) = 1 by MATRIX_0:def 6;
A15: len <*P*> = 1 by FINSEQ_1:40;
then
A16: width <*P*> = len P by MATRIX_0:20;
then
A17: len (<*P*>@) = len P by MATRIX_0:def 6;
width (<*P*>@) = 1 by A11,A15,A16,MATRIX_0:54;
then reconsider d1 = <*P*>@ as Matrix of len P,1,the carrier of V1
by A11,A17,MATRIX_0:20;
A18: len <*P^<*x*>*> = 1 by FINSEQ_1:40;
then
A19: width <*P^<*x*>*> = len (P^<*x*>) by MATRIX_0:20
.= len P + len <*x*> by FINSEQ_1:22
.= len P + 1 by FINSEQ_1:40;
A20: (<*<*x*>*>@)@ = <*<*x*>*> by A12,A13,MATRIX_0:57;
A21: width (<*P*>@) = len <*P*> by A11,A16,MATRIX_0:54
.= width (<*<*x*>*>@) by A15,A12,A13,MATRIX_0:54;
then width (<*<*x*>*>@) = 1 by A11,A15,A16,MATRIX_0:54;
then reconsider d2 = <*<*x*>*>@ as Matrix of 1,1,the carrier of V1
by A14,MATRIX_0:20;
A22: (d1 ^ d2)@ = ((<*P*>@)@) ^^ ((<*<*x*>*>@)@) by A21,MATRLIN:28
.= <*P*> ^^ <*<*x*>*> by A11,A15,A16,A20,MATRIX_0:57
.= <*P^<*x*>*> by A5,A7,FINSEQ_2:9
.= (<*P^<*x*>*>@)@ by A18,A19,MATRIX_0:57;
A23: len ((<*P*>@) ^ (<*<*x*>*>@)) = len (<*P*>@) + len (<*<*x*>*>@)
by FINSEQ_1:22
.= width <*P*> + len (<*<*x*>*>@) by MATRIX_0:def 6
.= width <*P*> + width <*<*x*>*> by MATRIX_0:def 6
.= len (<*P^<*x*>*>@) by A16,A13,A19,MATRIX_0:def 6;
thus Sum Sum <*P^<*x*>*> = Sum Sum (<*P*> ^^ <*<*x*>*>)
by A5,A7,FINSEQ_2:9
.= Sum Sum (<*P*>@) + Sum Sum <*<*x*>*> by A4,A15,A12,Th31
.= Sum Sum (<*P*>@) + Sum Sum (<*<*x*>*>@) by MATRLIN:15
.= Sum (Sum d1 ^ Sum d2) by RLVECT_1:41
.= Sum Sum (d1 ^ d2) by Th27
.= Sum Sum (<*P^<*x*>*>@) by A23,A22,MATRIX_0:53;
end;
end;
<*<*>(the carrier of V1)*> is Matrix of 0+1,0,the carrier of V1;
then Sum Sum <*<*>(the carrier of V1)*> = 0.V1 by Th14
.= Sum Sum (<*<*>(the carrier of V1)*>@) by A2,Th13;
then
A24: X[<*>(the carrier of V1)];
for P be FinSequence of V1 holds X[P] from FINSEQ_2:sch 2(A24,A3);
hence thesis;
end;
A25: for n st X[n] holds X[n+1]
proof
let n such that
A26: for M being Matrix of the carrier of V1 st len M = n holds
Sum Sum M = Sum Sum (M@);
thus for M being Matrix of the carrier of V1 st len M = n+1 holds
Sum Sum M = Sum Sum (M@)
proof
let M be Matrix of the carrier of V1 such that
A27: len M = n+1;
A28: M <> {} by A27;
A29: dom M = Seg len M by FINSEQ_1:def 3;
per cases;
suppose A30: n = 0;
then M.1 = Line(M,1) by A27,A29,FINSEQ_1:4,MATRIX_0:60;
then reconsider G = M.1 as FinSequence of V1;
M = <*G*> by A27,A30,FINSEQ_1:40;
hence thesis by A1;
end;
suppose A31: n > 0;
A32: M.(n+1) = Line(M,n+1) by A27,A29,FINSEQ_1:4,MATRIX_0:60;
then reconsider M1 = M.(n+1) as FinSequence of V1;
len M1 = width M by A32,MATRIX_0:def 7;
then reconsider R = <*M1*> as Matrix of 1,width M,the carrier of V1;
reconsider M9 = M as Matrix of n+1,width M,the carrier of V1
by A27,MATRIX_0:20;
reconsider W = Del(M9,n+1) as Matrix of n,width M,the carrier of V1
by MATRLIN:3;
A33: width W = width M9 by A31,MATRLIN:2
.= width R by MATRLIN:2;
A34: len (W@) = width W by MATRIX_0:def 6
.= len (R@) by A33,MATRIX_0:def 6;
A35: len Del(M,n+1) = n by A27,PRE_POLY:12;
thus Sum Sum M = Sum Sum (W ^ R) by A28,A27,PRE_POLY:13
.= Sum (Sum W ^ Sum R) by Th27
.= Sum Sum Del(M,n+1) + Sum Sum R by RLVECT_1:41
.= Sum Sum (Del(M,n+1)@) + Sum Sum R by A26,A35
.= Sum Sum (Del(M,n+1)@) + Sum Sum (R@) by A1
.= Sum Sum ((W@) ^^ (R@)) by A34,Th31
.= Sum Sum ((W ^ R)@) by A33,MATRLIN:28
.= Sum Sum (M@) by A28,A27,PRE_POLY:13;
end;
end;
end;
A36: X[0]
proof
let M be Matrix of the carrier of V1;
assume
A37: len M = 0;
then width M = 0 by MATRIX_0:def 3;
then
A38: len (M@) = 0 by MATRIX_0:def 6;
thus Sum Sum M = 0.V1 by A37,Th13
.= Sum Sum (M@) by A38,Th13;
end;
for n holds X[n] from NAT_1:sch 2(A36,A25);
then X[len M];
hence thesis;
end;
theorem Th33:
for M being Matrix of n,m,INT.Ring st n > 0 & m > 0
for p, d being FinSequence of INT.Ring st len p = n & len d = m &
for j st j in dom d holds d/.j = Sum mlt(p,Col(M,j))
for b,c being FinSequence of V1 st len b = m & len c = n &
for i st i in dom c holds c/.i = Sum lmlt(Line(M,i),b) holds
Sum lmlt(p,c) = Sum lmlt(d,b)
proof
let M be Matrix of n,m,INT.Ring such that
A1: n > 0 and
A2: m > 0;
A3: len M = n by A1,MATRIX_0:23;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
let p, d be FinSequence of INT.Ring such that
A4: len p = n and
A5: len d = m and
A6: for j st j in dom d holds d/.j = Sum mlt(p,Col(M,j));
let b, c be FinSequence of V1 such that
A7: len b = m and
A8: len c = n and
A9: for i st i in dom c holds c/.i = Sum lmlt(Line(M,i),b);
deffunc V(Nat,Nat) = (p/.$1) * (M*($1,$2)) * (b/.$2);
consider M1 be Matrix of n1,m1,the carrier of V1 such that
A10: for i, j st [i,j] in Indices M1 holds M1*(i,j) = V(i,j)
from MATRIX_0:sch 1;
A11: width M1 = len (M1@) by MATRIX_0:def 6
.= len Sum (M1@) by MATRLIN:def 6;
A12: dom d = dom b by A5,A7,FINSEQ_3:29;
then
A13: dom lmlt(d,b) = dom b by Th12;
then
A14: len lmlt(d,b) = len b by FINSEQ_3:29
.= len Sum (M1@) by A1,A7,A11,MATRIX_0:23;
then
A15: dom lmlt(d,b) = Seg len Sum(M1@) by FINSEQ_1:def 3;
A16: width M1 = m by A1,MATRIX_0:23;
A17: len M1 = n by A1,MATRIX_0:23;
A19:
now
A20: Seg len Sum(M1@) = dom Sum(M1@) by FINSEQ_1:def 3;
let j be Nat such that
A21: j in dom lmlt(d,b);
A22: j in dom Sum(M1@) by A15,A21,FINSEQ_1:def 3;
A23: j in dom d by A12,A21,Th12;
A24: d/.j = d.j & b/.j = b.j by A12,A13,A21,PARTFUN1:def 6;
len Sum(M1@) = len (M1@) by MATRLIN:def 6;
then
A25: dom Sum(M1@) = dom (M1@) by FINSEQ_3:29;
then
A26: M1@/.j = M1@.j by A22,PARTFUN1:def 6
.= Line(M1@,j) by A22,A25,MATRIX_0:60;
reconsider H = mlt(p,Col(M,j)) as FinSequence of INT.Ring;
deffunc V(Nat) = (H/.$1) * (b/.j);
consider G be FinSequence of V1 such that
A27: len G = len p & for i being Nat st i in dom G holds G.i = V(i)
from FINSEQ_2:sch 1;
A28: len p = len Col(M,j) by A4,A3,MATRIX_0:def 8;
then
A29: len ((the multF of INT.Ring).:(p,Col(M,j))) = len p
by FINSEQ_2:72;
then
A30: dom H = dom G by A27,FINSEQ_3:29;
A31: dom p = dom G by A27,FINSEQ_3:29;
A32: len Line(M1@,j) = width (M1@) by MATRIX_0:def 7
.= len ((M1@)@) by MATRIX_0:def 6
.= len G by A1,A2,A4,A17,A16,A27,MATRIX_0:57; then
A33: dom Line(M1@,j) = Seg len G by FINSEQ_1:def 3;
A34: dom G = Seg len p by A27,FINSEQ_1:def 3;
A35: now
let i be Nat;
A36: dom M = Seg len M by FINSEQ_1:def 3;
assume
A37: i in dom Line(M1@,j);
then
A38: i in Seg len ((the multF of INT.Ring).:(p,Col(M,j)))
by A27,A28,A33,FINSEQ_2:72;
then
A39: i in dom H by FINSEQ_1:def 3;
A40: i in dom ((multint).:(p,Col(M,j))) by A38,FINSEQ_1:def 3;
A41: Seg len G = dom G by FINSEQ_1:def 3;
then p/.i = p.i by A31,A33,A37,PARTFUN1:def 6;
then
A42: (p/.i) * (M*(i,j)) = (multint).(p.i,Col(M,j).i)
by A4,A3,A27,A33,A37,A36,MATRIX_0:def 8
.= ((multint).:(p,Col(M,j))).i by A40,FUNCOP_1:22
.= H/.i by A39,PARTFUN1:def 6;
dom M1 = dom G by A4,A17,A27,FINSEQ_3:29; then
A43: [i,j] in Indices M1 by A11,A15,A21,A33,A37,A41,ZFMISC_1:87;
i in Seg width (M1@) by A32,A33,A37,MATRIX_0:def 7;
hence Line(M1@,j).i = (M1@)*(j,i) by MATRIX_0:def 7
.= M1*(i,j) by A43,MATRIX_0:def 6
.= (H/.i) * (b/.j) by A10,A43,A42
.= G.i by A27,A34,A33,A37;
end;
thus lmlt(d,b).j = (the lmult of V1).(d.j,b.j) by A21,FUNCOP_1:22
.= Sum H * (b/.j) by A6,A23,A24
.= Sum G by A27,A29,A30,Th10
.= Sum (M1@/.j) by A32,A35,A26,FINSEQ_2:9
.= Sum (M1@)/.j by A22,MATRLIN:def 6
.= (Sum (M1@)).j by A15,A21,A20,PARTFUN1:def 6;
end;
A44: dom p = dom c by A4,A8,FINSEQ_3:29;
then
A45: dom lmlt(p,c) = dom p by Th12;
then
A46: len lmlt(p,c) = len p by FINSEQ_3:29
.= len M1 by A4,MATRIX_0:def 2
.= len Sum M1 by MATRLIN:def 6;
now
let i be Nat such that
A47: i in dom Sum M1;
A48: i in dom c by A44,A45,A46,A47,FINSEQ_3:29;
then
A49: c.i = c/.i & p.i = p/.i by A44,PARTFUN1:def 6;
i in Seg len Sum M1 by A47,FINSEQ_1:def 3;
then i in Seg len M1 by MATRLIN:def 6;
then
A50: i in dom M1 by FINSEQ_1:def 3;
then
A51: M1/.i = M1.i by PARTFUN1:def 6
.= Line(M1,i) by A50,MATRIX_0:60;
deffunc V(Nat) = (p/.i) * (lmlt(Line(M,i),b)/.$1);
consider F be FinSequence of V1 such that
A52: len F = len b & for j being Nat st j in dom F holds F.j = V(j)
from FINSEQ_2:sch 1;
A53: len F = width M by A1,A7,A52,MATRIX_0:23;
A54: dom Line(M,i) = Seg len Line(M,i) by FINSEQ_1:def 3
.= dom b by A52,A53,FINSEQ_1:def 3,MATRIX_0:def 7;
then dom lmlt(Line(M,i),b) = dom b by Th12;
then
A55: len F = len lmlt(Line(M,i),b) & dom F = dom lmlt(Line(M,i),b)
by A52,FINSEQ_3:29;
A56: len F = width M1 by A1,A7,A52,MATRIX_0:23;
then
A57: len Line(M1,i) = len F by MATRIX_0:def 7;
then
A58: dom (M1/.i) = Seg len F by A51,FINSEQ_1:def 3;
A59: dom F = Seg len b by A52,FINSEQ_1:def 3;
A60:
now
let j be Nat;
assume
A61: j in dom (M1/.i);
then
A62: Line(M,i).j = M*(i,j) by A53,A58,MATRIX_0:def 7;
A63: [i,j] in Indices M1 by A56,A50,A58,A61,ZFMISC_1:87;
A64: j in dom b by A52,A58,A61,FINSEQ_1:def 3;
then
A65: b.j = b/.j by PARTFUN1:def 6;
A66: j in dom (lmlt(Line(M,i),b)) by A54,A64,Th12;
then
A67: (lmlt(Line(M,i),b)/.j) = lmlt(Line(M,i),b).j by PARTFUN1:def 6
.= M*(i,j) * (b/.j) by A65,A62,A66,FUNCOP_1:22;
thus (M1/.i).j = M1*(i,j) by A56,A51,A58,A61,MATRIX_0:def 7
.= (p/.i) * (M*(i,j)) * (b/.j) by A10,A63
.= (p/.i) * (lmlt(Line(M,i),b)/.j) by A67,VECTSP_1:def 16
.= F.j by A52,A59,A58,A61;
end;
A68: for j being Nat, v being Vector of V1
st j in dom F & v =lmlt(Line(M,i),b).j
holds F.j = (p/.i) * v
proof
let j be Nat, v be Vector of V1;
assume A681: j in dom F & v =lmlt(Line(M,i),b).j;
thus
F.j = (p/.i) * (lmlt(Line(M,i),b)/.j) by A52,A681
.= (p/.i) * v by A55,A681,PARTFUN1:def 6;
end;
i in dom ((the lmult of V1).:(p,c)) by A46,A47,FINSEQ_3:29;
hence lmlt(p,c).i = (the lmult of V1).(p.i,c.i) by FUNCOP_1:22
.= (p/.i) * Sum lmlt(Line(M,i),b) by A9,A48,A49
.= Sum F by A55,A68,ZMODUL01:12
.= Sum (M1/.i) by A57,A51,A60,FINSEQ_2:9
.= (Sum M1)/.i by A47,MATRLIN:def 6
.= (Sum M1).i by A47,PARTFUN1:def 6;
end;
hence Sum lmlt(p,c) = Sum Sum M1 by A46,FINSEQ_2:9
.= Sum Sum (M1@) by Th32
.= Sum lmlt(d,b) by A14,A19,FINSEQ_2:9;
end;
begin :: Decomposition of a Vector in Basis
definition
let V be finite-rank free Z_Module;
let b1 be OrdBasis of V;
let W be Element of V;
func W|--b1 -> FinSequence of INT.Ring means
:Def7:
len it = len b1 &
ex KL be Linear_Combination of V st W = Sum(KL) & Carrier KL c= rng b1 &
for k st 1 <= k & k <= len it holds it/.k = KL.(b1/.k);
existence
proof
reconsider b2 = rng b1 as Basis of V by defOrdBasis;
consider KL be Linear_Combination of V such that
A1: W = Sum(KL) and
A2: Carrier KL c= b2 by Th8;
deffunc V(Nat) = KL.(b1/.$1);
consider A be FinSequence of INT.Ring such that
A3: len A = len b1 and
A4: for k being Nat st k in dom A holds A.k = V(k) from FINSEQ_2:sch 1;
take A;
thus len A = len b1 by A3;
take KL;
thus W = Sum(KL) by A1;
thus Carrier KL c= rng b1 by A2;
let k;
A5: dom A = Seg len b1 by A3,FINSEQ_1:def 3;
assume A6: 1 <= k & k <= len A;
then k in Seg len b1 by A3,FINSEQ_1:1;
then k in dom A by A3,FINSEQ_1:def 3;
then A.k = A/.k by PARTFUN1:def 6;
hence thesis by A3,A4,A5,A6,FINSEQ_1:1;
end;
uniqueness
proof
reconsider b = rng b1 as Basis of V by defOrdBasis;
let F1, F2 be FinSequence of INT.Ring;
assume
A7: len F1 = len b1;
given KL1 be Linear_Combination of V such that
A8: W = Sum(KL1) & Carrier(KL1) c= rng b1 and
A9: for k st 1<=k & k<=len F1 holds F1/.k=KL1.(b1/.k);
assume
A10: len F2 = len b1;
given KL2 be Linear_Combination of V such that
A11: W = Sum(KL2) & Carrier(KL2) c= rng b1 and
A12: for k st 1 <= k & k <= len F2 holds F2/.k = KL2.(b1/.k);
A13: b is linearly-independent by VECTSP_7:def 3;
for k be Nat st 1 <= k & k <= len F1 holds F1.k = F2.k
proof
let k be Nat;
assume
A14: 1 <= k & k <= len F1;
then
A15: k in dom F2 by A7,A10,FINSEQ_3:25;
k in dom F1 by A14,FINSEQ_3:25;
hence F1.k = F1/.k by PARTFUN1:def 6
.= KL1.(b1/.k) by A9,A14
.= KL2.(b1/.k) by A8,A11,A13,Th5
.= F2/.k by A7,A10,A12,A14
.= F2.k by A15,PARTFUN1:def 6;
end;
hence thesis by A7,A10,FINSEQ_1:14;
end;
end;
Lm1: for V being finite-rank free Z_Module for b being
OrdBasis of V for W being Element of V holds dom (W|--b) = dom b
proof
let V be finite-rank free Z_Module, b be OrdBasis of V,
W be Element of V;
len (W|--b) = len b by Def7;
hence thesis by FINSEQ_3:29;
end;
theorem Th34:
v1|--b2 = v2|--b2 implies v1 = v2
proof
consider KL1 be Linear_Combination of V2 such that
A1: v1 = Sum(KL1) and
A2: Carrier KL1 c= rng b2 and
A3: for t st 1<=t & t<=len (v1|--b2) holds (v1|--b2)/.t = KL1.(b2/.t)
by Def7;
consider KL2 be Linear_Combination of V2 such that
A4: v2 = Sum(KL2) and
A5: Carrier KL2 c= rng b2 and
A6: for t st 1<=t & t<=len (v2|--b2) holds (v2|--b2)/.t = KL2.(b2/.t)
by Def7;
assume
A7: v1|--b2 = v2|--b2;
A8:
now
let t be Nat;
assume
A9: 1 <= t & t <= len (v1|--b2);
hence KL1.(b2/.t) = (v2|--b2)/.t by A7,A3
.= KL2.(b2/.t) by A7,A6,A9;
end;
A10: Carrier KL1 \/ Carrier KL2 c= rng b2 by A2,A5,XBOOLE_1:8;
now
let v be Vector of V2;
per cases;
suppose A11: not v in Carrier KL1 \/ Carrier KL2;
then not v in Carrier KL2 by XBOOLE_0:def 3;
then
A12: KL2.v = 0;
not v in Carrier KL1 by A11,XBOOLE_0:def 3;
hence KL1.v = KL2.v by A12;
end;
suppose v in Carrier KL1 \/ Carrier KL2;
then consider x be object such that
A13: x in dom b2 and
A14: v = b2.x by A10,FUNCT_1:def 3;
reconsider x as Nat by A13;
x <= len b2 by A13,FINSEQ_3:25;
then
A15: x <= len (v1|--b2) by Def7;
v = b2/.x & 1 <= x by A13,A14,FINSEQ_3:25,PARTFUN1:def 6;
hence KL1.v = KL2.v by A8,A15;
end;
end;
hence thesis by A1,A4,VECTSP_6:def 7;
end;
theorem Th35:
v = Sum lmlt(v|--b1,b1)
proof
consider KL be Linear_Combination of V1 such that
A1: v = Sum KL & Carrier KL c= rng b1 and
A2: for k st 1 <= k & k <= len (v|--b1) holds (v|--b1)/.k = KL.(b1/.k)
by Def7;
len (v|--b1) = len b1 by Def7;
then
A3: dom (v|--b1) = dom b1 by FINSEQ_3:29;
then
A4: dom b1 = dom lmlt(v|--b1,b1) by Th12;
A51: len (KL (#) b1) = len b1 by VECTSP_6:def 5
.= len lmlt(v|--b1,b1) by A4,FINSEQ_3:29;
then
A5: dom (KL (#) b1) = dom lmlt(v|--b1,b1) by FINSEQ_3:29;
A6:
now
let t be Nat;
assume
A7: t in dom lmlt(v|--b1,b1);
then
A8: b1/.t = b1.t by A4,PARTFUN1:def 6;
t in dom (v|--b1) by A3,A7,Th12;
then
A9: t <= len (v|--b1) by FINSEQ_3:25;
A10: 1 <= t by A7,FINSEQ_3:25;
then
A11: (v|--b1)/.t = (v|--b1).t by A9,FINSEQ_4:15;
t in dom (KL (#) b1) by A51,A7,FINSEQ_3:29;
hence (KL (#) b1).t = KL.(b1/.t) * (b1/.t) by VECTSP_6:def 5
.= ((v|--b1)/.t) * (b1/.t) by A2,A10,A9
.= lmlt(v|--b1,b1).t by A7,A8,A11,FUNCOP_1:22;
end;
thus v = Sum(KL (#) b1) by A1,defOrdBasis,Th20
.= Sum lmlt(v|--b1,b1) by A5,A6,FINSEQ_1:13;
end;
theorem Th36:
len d = len b1 implies d = Sum(lmlt(d,b1)) |-- b1
proof
reconsider T = rng b1 as finite Subset of V1;
defpred X[Element of V1, Element of INT.Ring] means
($1 in rng b1 implies
(for k st k in dom b1 & b1/.k = $1 holds $2 = d/.k)) &
(not $1 in rng b1 implies $2 = 0.INT.Ring);
A1: for v ex u being Element of INT.Ring st X[v,u]
proof
let v be Element of V1;
per cases;
suppose A2: v in rng b1;
then consider k be Element of NAT such that
A3: k in dom b1 and
A4: b1/.k = v by PARTFUN2:2;
take u = d/.k;
now
A5: b1 is one-to-one by defOrdBasis;
let i;
assume that
A6: i in dom b1 and
A7: b1/.i = v;
b1.i = b1/.k by A4,A6,A7,PARTFUN1:def 6
.= b1.k by A3,PARTFUN1:def 6;
hence u = d/.i by A3,A6,A5;
end;
hence thesis by A2;
end;
suppose A8: not v in rng b1;
reconsider I0 = 0.INT.Ring as Element of INT.Ring;
take I0;
thus thesis by A8;
end;
end;
consider KL be Function of V1, the carrier of INT.Ring such that
A9: for v holds X[v,KL.v] from FUNCT_2:sch 3(A1);
now
take f = KL;
thus KL = f & dom f = the carrier of V1 & rng f c= the carrier of
INT.Ring by FUNCT_2:def 1;
end;
then KL in Funcs(the carrier of V1, the carrier of INT.Ring)
by FUNCT_2:def 2;
then reconsider KL1 = KL as Linear_Combination of V1
by A9,VECTSP_6:def 1;
assume
A11: len d = len b1;
now
take KL1;
thus
A13: for k st 1 <= k & k <= len d holds d/.k = KL1.(b1/.k)
proof
let k;
assume A141: 1 <= k & k <= len d;
then A14: k in dom b1 by A11,FINSEQ_3:25;
then b1.k = b1/.k by PARTFUN1:def 6;
then b1/.k in rng b1 by A14,FUNCT_1:def 3;
hence thesis by A9,A11,A141,FINSEQ_3:25;
end;
for x being object holds x in Carrier KL1 implies x in rng b1
proof
let x be object;
assume x in Carrier KL1;
then
A15: ex v st x = v & KL1.v <> 0;
assume not x in rng b1;
hence contradiction by A9,A15;
end;
hence
A16: Carrier KL1 c= rng b1;
A17: dom d = dom b1 by A11,FINSEQ_3:29;
then
A18: dom lmlt(d,b1) = dom b1 by Th12;
then
A19: len lmlt(d,b1) = len b1 by FINSEQ_3:29
.= len (KL1 (#) b1) by VECTSP_6:def 5;
now
let k be Nat;
assume
A20: k in dom lmlt(d,b1);
then
A21: k in dom (KL1 (#) b1) by A19,FINSEQ_3:29;
A22: 1 <= k & k <= len d by A11,A18,A20,FINSEQ_3:25;
A23: d/.k = d.k & b1/.k = b1.k by A17,A18,A20,PARTFUN1:def 6;
thus lmlt(d,b1).k = (the lmult of V1).(d.k,b1.k) by A20,FUNCOP_1:22
.= KL1.(b1/.k) * (b1/.k) by A13,A22,A23
.= (KL1 (#) b1).k by A21,VECTSP_6:def 5;
end;
hence Sum(lmlt(d,b1)) = Sum(KL1 (#) b1) by A19,FINSEQ_2:9
.= Sum KL1 by A16,defOrdBasis,Th20;
end;
hence thesis by A11,Def7;
end;
Lm2: for p being FinSequence, k being set st k in dom p holds len p > 0
proof
let p be FinSequence, k be set;
assume k in dom p;
then p <> {};
hence thesis;
end;
theorem Th37:
for a, d being FinSequence of INT.Ring st len a = len b1
for j being Nat st j in dom b2 & len d = len b1 &
for k st k in dom b1 holds d.k = (f.((b1/.k)) |-- b2)/.j holds
len b1 > 0 implies (Sum(lmlt(a,f*b1)) |-- b2)/.j = Sum(mlt(a,d))
proof
let a, d be FinSequence of INT.Ring such that
A1: len a = len b1;
reconsider B3 = f*b1 as FinSequence of V2;
deffunc V(Nat,Nat) = ((B3/.$1) |-- b2)/.$2;
consider M be Matrix of len b1,len b2,INT.Ring such that
A2: for i, j st [i,j] in Indices M holds M*(i,j) = V(i,j)
from MATRIX_0:sch 1;
deffunc W(Nat) = Sum mlt(a,Col(M,$1));
consider dd be FinSequence of INT.Ring such that
A3: len dd = len b2 & for j being Nat st j in dom dd holds dd/.j = W(j)
from FINSEQ_4:sch 2;
let j be Nat such that
A4: j in dom b2;
A5: j in dom dd by A4,A3,FINSEQ_3:29;
assume that
A6: len d = len b1 and
A7: for k st k in dom b1 holds d.k = (f.(b1/.k) |-- b2)/.j;
A8: len Col(M,j) = len M by MATRIX_0:def 8
.= len d by A6,MATRIX_0:def 2;
len M = len b1 by MATRIX_0:def 2; then
A9: dom M = dom b1 by FINSEQ_3:29;
A10: len b1 = len B3 by FINSEQ_2:33; then
A11: dom b1 = dom B3 by FINSEQ_3:29;
assume
A12: len b1 > 0; then
A13: width M = len b2 by MATRIX_0:23;
A14:
now
let i such that
A15: i in dom B3;
A16:
now
let j be Nat;
assume
A17: j in dom ((B3/.i) |-- b2);
then j in Seg len ((B3/.i) |-- b2) by FINSEQ_1:def 3;
then
A18: j in Seg width M by A13,Def7;
then
A19: [i,j] in Indices M by A9,A11,A15,ZFMISC_1:87;
thus Line(M,i).j = M*(i,j) by A18,MATRIX_0:def 7
.= ((B3/.i) |-- b2)/.j by A2,A19
.= ((B3/.i) |-- b2).j by A17,PARTFUN1:def 6;
end;
A20: len Line(M,i) = width M by MATRIX_0:def 7
.= len ((B3/.i) |-- b2) by A13,Def7;
thus B3/.i = Sum lmlt((B3/.i) |-- b2,b2) by Th35
.= Sum lmlt(Line(M,i),b2) by A20,A16,FINSEQ_2:9;
end;
Seg len b2 = dom b2 by FINSEQ_1:def 3;
then
A21: j in Seg width M by A4,A12,MATRIX_0:23;
A22:
now
let i be Nat;
assume i in dom d;
then
A23: i in dom b1 by A6,FINSEQ_3:29;
then
A24: B3/.i = B3.i by A11,PARTFUN1:def 6
.= f.(b1.i) by A23,FUNCT_1:13
.= f.(b1/.i) by A23,PARTFUN1:def 6;
A25: [i,j] in Indices M by A9,A21,A23,ZFMISC_1:87;
thus Col(M,j).i = M*(i,j) by A9,A23,MATRIX_0:def 8
.= (f.((b1/.i)) |-- b2)/.j by A2,A24,A25
.= d.i by A7,A23;
end;
len b2 > 0 by A4,Lm2;
hence (Sum(lmlt(a,f*b1)) |-- b2)/.j = (Sum(lmlt(dd,b2)) |-- b2)/.j
by A1,A12,A3,A10,A14,Th33
.= dd/.j by A3,Th36
.= Sum(mlt(a,Col(M,j))) by A3,A5
.= Sum(mlt(a,d)) by A8,A22,FINSEQ_2:9;
end;
begin :: Matrices of Linear Transformations
definition
let V1, V2 be finite-rank free Z_Module;
let f be Function of V1, V2;
let b1 be FinSequence of V1;
let b2 be OrdBasis of V2;
func AutMt(f,b1,b2) -> Matrix of INT.Ring means :Def8:
len it = len b1 & for k st k in dom b1 holds it/.k = f.(b1/.k) |-- b2;
existence
proof
deffunc V(Nat) = f.(b1/.$1) |-- b2;
consider M be FinSequence such that
A1: len M = len b1 and
A2: for k being Nat st k in dom M holds M.k = V(k) from FINSEQ_1:sch 2;
A3: dom M = Seg len b1 by A1,FINSEQ_1:def 3;
ex n being Nat st for x st x in rng M ex s st s = x & len s = n
proof
take n = len(f.(b1/.1) |-- b2);
let x be object;
assume x in rng M;
then consider y be object such that
A4: y in dom M and
A5: x = M.y by FUNCT_1:def 3;
reconsider y as Nat by A4;
M.y = f.(b1/.y) |-- b2 by A2,A4;
then reconsider s = M.y as FinSequence;
take s;
thus s = x by A5;
thus len s = len (f.(b1/.y) |-- b2) by A2,A4
.= len b2 by Def7
.= n by Def7;
end;
then reconsider M as tabular FinSequence by MATRIX_0:def 1;
now
let x be object;
assume x in rng M;
then consider y be object such that
A6: y in dom M and
A7: x = M.y by FUNCT_1:def 3;
reconsider y as Nat by A6;
M.y = f.(b1/.y) |-- b2 by A2,A6;
then reconsider s = M.y as FinSequence of INT;
s = x by A7;
hence x in (INT)* by FINSEQ_1:def 11;
end;
then rng M c= (the carrier of INT.Ring)*;
then reconsider M as Matrix of INT.Ring by FINSEQ_1:def 4;
take M1 = M;
for k st k in dom b1 holds M1/.k = f.(b1/.k) |-- b2
proof
let k be Nat;
assume
A8: k in dom b1;
then
A9: k in Seg len b1 by FINSEQ_1:def 3;
dom M1 = dom b1 by A1,FINSEQ_3:29;
hence M1/.k = M1.k by A8,PARTFUN1:def 6
.= f.(b1/.k) |-- b2 by A2,A3,A9;
end;
hence thesis by A1;
end;
uniqueness
proof
let K1, K2 be Matrix of INT.Ring such that
A10: len K1 = len b1 and
A11: for k st k in dom b1 holds K1/.k = f.(b1/.k) |-- b2 and
A12: len K2 = len b1 and
A13: for k st k in dom b1 holds K2/.k = f.(b1/.k) |-- b2;
for k be Nat st 1 <= k & k <= len K1 holds K1.k = K2.k
proof
let k be Nat;
assume
A14: 1 <= k & k <= len K1;
A16: k in dom K2 by A10,A12,A14,FINSEQ_3:25;
k in dom K1 by A14,FINSEQ_3:25;
hence K1.k = K1/.k by PARTFUN1:def 6
.= f.(b1/.k) |-- b2 by A10,A11,A14,FINSEQ_3:25
.= K2/.k by A10,A13,A14,FINSEQ_3:25
.= K2.k by A16,PARTFUN1:def 6;
end;
hence thesis by A10,A12,FINSEQ_1:14;
end;
end;
Lm3: dom AutMt(f,b1,b2) = dom b1
proof
len AutMt(f,b1,b2) = len b1 by Def8;
hence thesis by FINSEQ_3:29;
end;
theorem Th38:
len b1 = 0 implies AutMt(f,b1,b2) = {}
proof
assume len b1 = 0;
then len AutMt(f,b1,b2) = 0 by Def8;
hence thesis;
end;
theorem Th39:
len b1 > 0 implies width AutMt(f,b1,b2) = len b2
proof
assume len b1 > 0;
then len AutMt(f,b1,b2) > 0 by Def8;
then consider s be FinSequence such that
A1: s in rng AutMt(f,b1,b2) and
A2: len s = width AutMt(f,b1,b2) by MATRIX_0:def 3;
consider i be Nat such that
A3: i in dom AutMt(f,b1,b2) and
A4: AutMt(f,b1,b2).i = s by A1,FINSEQ_2:10;
len AutMt(f,b1,b2) = len b1 by Def8;
then
A5: i in dom b1 by A3,FINSEQ_3:29;
s = (AutMt(f,b1,b2))/.i by A3,A4,PARTFUN1:def 6
.= f.(b1/.i) |-- b2 by A5,Def8;
hence thesis by A2,Def7;
end;
theorem
f1 is additive homogeneous & f2 is additive homogeneous &
AutMt(f1,b1,b2) = AutMt(f2,b1,b2) & len b1 > 0 implies f1 = f2
proof
assume that
A1: f1 is additive homogeneous & f2 is additive homogeneous and
A2: AutMt(f1,b1,b2) = AutMt(f2,b1,b2) and
A3: len b1 > 0;
A4: rng b1 c= the carrier of V1;
then
A5: rng b1 c= dom f2 by FUNCT_2:def 1;
rng b1 c= dom f1 by A4,FUNCT_2:def 1;
then
A6: dom (f1*b1) = dom b1 by RELAT_1:27
.= dom (f2*b1) by A5,RELAT_1:27;
now
let x be object;
assume
A7: x in dom (f1*b1);
then reconsider k = x as Nat;
A8: dom (f1*b1) c= dom b1 by RELAT_1:25;
then
A9: f1.(b1/.k) |-- b2 = (AutMt(f2,b1,b2))/.k by A2,A7,Def8
.= f2.(b1/.k) |-- b2 by A7,A8,Def8;
thus (f1*b1).x = f1.(b1.x) by A7,FUNCT_1:12
.= f1.(b1/.x) by A7,A8,PARTFUN1:def 6
.= f2.(b1/.x) by A9,Th34
.= f2.(b1.x) by A7,A8,PARTFUN1:def 6
.= (f2*b1).x by A6,A7,FUNCT_1:12;
end;
hence thesis by A1,A3,A6,Th22,FUNCT_1:2;
end;
theorem LmSign1X:
for F being FinSequence of F_Real,
G being FinSequence of INT.Ring
st F = G
holds Sum F = Sum G
proof
defpred P[Nat] means
for F being FinSequence of F_Real,
G being FinSequence of INT.Ring
st len F = $1 & F = G holds Sum F = Sum G;
P1: P[0]
proof
let F be FinSequence of F_Real,
G be FinSequence of INT.Ring;
assume AS1: len F = 0 & F = G;
then F = <*> the carrier of F_Real;
then
P1: Sum F = 0.F_Real by RLVECT_1:43
.= 0;
G = <*> REAL by AS1; then
G = <*>the carrier of INT.Ring; then
Sum G = 0.INT.Ring by RLVECT_1:43;
hence thesis by P1;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
let F be FinSequence of F_Real,
G be FinSequence of INT.Ring;
assume AS2: len F = n+1 & F = G;
reconsider F0 = F| n as FinSequence of F_Real;
n+1 in Seg (n+1) by FINSEQ_1:4;
then n+1 in dom F by AS2,FINSEQ_1:def 3;
then F.(n+1) in rng F by FUNCT_1:3;
then reconsider af = F.(n+1) as Element of F_Real;
P1: len F0 = n by AS2,FINSEQ_1:59,NAT_1:11; then
P4: dom F0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by AS2,FINSEQ_1:59,NAT_1:11;
F0 = F | dom F0 by P4,FINSEQ_1:def 16; then
P3: Sum F = Sum F0 + af by AS2,A9,RLVECT_1:38;
reconsider G0 = G| n as FinSequence of INT.Ring;
n+1 in Seg (n+1) by FINSEQ_1:4;
then n+1 in dom G by AS2,FINSEQ_1:def 3;
then G.(n+1) in rng G by FUNCT_1:3;
then reconsider bf = G.(n+1) as Element of INT.Ring;
len G = n + 1 & G0 = G | (Seg n) by AS2,FINSEQ_1:def 16; then
G = G0^<*bf*> by FINSEQ_3:55;
then Sum G = Sum G0 + bf by FVSUM_1:71;
hence Sum F = Sum G by AS1,AS2,P1,P3;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
let F be FinSequence of F_Real,
G be FinSequence of INT.Ring;
assume X2: F = G;
len F is Nat;
hence thesis by X1,X2;
end;
LMEQ5:
for f, g, h being Function st f| (dom g) = g & rng h c= dom g & rng h c= dom f
holds f*h = g*h
proof
let f, g, h be Function;
assume AS: f| (dom g) = g & rng h c= dom g & rng h c= dom f;
P1: dom (f*h) = dom h by AS,RELAT_1:27;
P2: dom (g*h) = dom h by AS,RELAT_1:27;
for x being object st x in dom (f*h) holds (f*h).x = (g*h).x
proof
let x be object;
assume AS1: x in dom (f*h);
then x in dom h by AS,RELAT_1:27;
then P3: h.x in rng h by FUNCT_1:3;
thus (f*h).x =f.(h.x) by AS1,FUNCT_1:12
.= (f | (dom g)) .(h.x) by AS,P3,FUNCT_1:49
.= (g*h).x by AS,AS1,P1,P2,FUNCT_1:12;
end;
hence thesis by AS,P1,RELAT_1:27;
end;
LMLT12:
multint = multreal | [:INT,INT:]
proof
set ad = multreal | [:INT,INT:];
[:INT,INT:] c= [:REAL,REAL:] by NUMBERS:15,ZFMISC_1:96;
then A1: [:INT,INT:] c= dom (multreal) by FUNCT_2:def 1;
then A2: dom ad = [:INT,INT:] by RELAT_1:62;
A3: dom (multint) = [:INT,INT:] by FUNCT_2:def 1;
for z being object st z in dom ad holds ad.z = multint.z
proof
let z be object;
assume A4: z in dom ad;
then consider x, y be object such that
A5: x in INT & y in INT & z = [x,y] by A2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Integer by A5;
thus ad.z = multreal.(x1,y1) by A4,A5,A2,FUNCT_1:49
.= x1*y1 by BINOP_2:def 11
.= multint.(x1,y1) by BINOP_2:def 22
.= multint.z by A5;
end;
hence thesis by A1,A3,FUNCT_1:2,RELAT_1:62;
end;
theorem
for p, q being FinSequence of INT.Ring,
p1,q1 being FinSequence of F_Real
st p = p1 & q = q1
holds p "*" q = p1 "*" q1
proof
let p, q be FinSequence of INT.Ring,
p1, q1 be FinSequence of F_Real;
assume AS: p = p1 & q = q1;
A2: [:rng p,rng q:] c= [:INT,INT:] by ZFMISC_1:96;
A3: rng <:p,q:> c= [:rng p,rng q:] by FUNCT_3:51;
B1: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
[:INT,INT:] c= [:REAL,REAL:] by NUMBERS:15,ZFMISC_1:96; then
B2: rng <:p,q:> c= dom multreal by A2,A3,B1;
[:INT,INT:] = dom (multint) by FUNCT_2:def 1; then
B3: rng <:p,q:> c= dom (multint) by A2,A3;
multreal | dom (multint) = multint by LMLT12,FUNCT_2:def 1; then
A6: multint* <:p,q:> = multreal* <:p,q:> by LMEQ5,B3,B2;
mlt (p,q) = multint* <:p1,q1:> by AS,FUNCOP_1:def 3
.= mlt (p1,q1) by AS,A6,FUNCOP_1:def 3;
hence thesis by LmSign1X;
end;
theorem ThComp1:
g is additive homogeneous & len b1 > 0 & len b2 > 0 implies
AutMt(g*f,b1,b3) = AutMt(f,b1,b2) * AutMt(g,b2,b3)
proof
assume
A1: g is additive homogeneous;
assume that
A2: len b1 > 0 and
A3: len b2 > 0;
A4:width AutMt(f,b1,b2) = len b2 by A2,Th39
.= len (AutMt(g,b2,b3)) by Def8;
A5: width (AutMt(g*f,b1,b3)) = len b3 by A2,Th39
.= width (AutMt(g,b2,b3)) by A3,Th39;
A6: width (AutMt(g*f,b1,b3))
= width ((AutMt(f,b1,b2)) * (AutMt(g,b2,b3)))
by A5,A4,MATRIX_3:def 4;
A7: len (AutMt(g*f,b1,b3)) = len b1 by Def8
.= len AutMt(f,b1,b2) by Def8
.= len (AutMt(f,b1,b2)
* (AutMt(g,b2,b3))) by A4,MATRIX_3:def 4;
for i, j st [i,j] in Indices (AutMt(g*f,b1,b3)) holds
(AutMt(g*f,b1,b3))*(i,j) = ((AutMt(f,b1,b2))
* (AutMt(g,b2,b3)))*(i,j)
proof
let i, j;
deffunc V(Nat) = (g.((b2/.$1)) |-- b3)/.j;
consider d be FinSequence of INT.Ring such that
A9: len d = len b2 & for k being Nat st k in dom d holds d.k = V(k)
from FINSEQ_2:sch 1;
assume
A10: [i,j] in Indices (AutMt(g*f,b1,b3)); then
A12: j in Seg width AutMt(g*f,b1,b3) by ZFMISC_1:87;
A13: len Col(AutMt(g,b2,b3),j) = len AutMt(g,b2,b3) by MATRIX_0:def 8
.= len d by A9,Def8;
A14: dom d = Seg len b2 by A9,FINSEQ_1:def 3;
A15: [i,j] in Indices
((AutMt(f,b1,b2)) * (AutMt(g,b2,b3))) by A6,A7,A10,FINSEQ_3:29;
A16: i in dom AutMt(g*f,b1,b3) by A10,ZFMISC_1:87;
A17: width AutMt(g*f,b1,b3) <> {} by A10;
len b1 = len AutMt(g*f,b1,b3) by Def8;
then len b1 > 0 by A17,MATRIX_0:def 3; then
A18: j in Seg len b3 by A12,Th39; then
A19: j in dom b3 by FINSEQ_1:def 3;
A20:
now
let k be Nat;
assume
A21: 1 <= k & k <= len d;
A23: k in dom b2 by A9,A21,FINSEQ_3:25;
A24: len AutMt(g,b2,b3) = len b2 by Def8;
then
A25: k in dom AutMt(g,b2,b3) by A9,A21,FINSEQ_3:25;
j in Seg width AutMt(g,b2,b3) by A5,A10,ZFMISC_1:87;
then [k,j] in Indices AutMt(g,b2,b3) by A25,ZFMISC_1:87;
then consider p2 be FinSequence of INT such that
A26: p2 = AutMt(g,b2,b3).k and
A27: AutMt(g,b2,b3)*(k,j) = p2.j by MATRIX_0:def 5;
A28: p2 = (AutMt(g,b2,b3))/.k by A25,A26,PARTFUN1:def 6
.= g.(b2/.k) |-- b3 by A23,Def8;
then j in Seg len p2 by A18,Def7;
then
A29: j in dom p2 by FINSEQ_1:def 3;
k in dom AutMt(g,b2,b3) by A9,A21,A24,FINSEQ_3:25;
hence Col(AutMt(g,b2,b3),j).k = p2.j by A27,MATRIX_0:def 8
.= (g.(b2/.k) |-- b3)/.j by A28,A29,PARTFUN1:def 6
.= d.k by A9,A21,FINSEQ_3:25;
end;
b1/.i in the carrier of V1;
then
A30: b1/.i in dom f by FUNCT_2:def 1;
consider p1 be FinSequence of INT such that
A31: p1 = AutMt(g*f,b1,b3).i and
A32: AutMt(g*f,b1,b3)*(i,j) = p1.j by A10,MATRIX_0:def 5;
A33: len (f.(b1/.i) |-- b2) = len b2 by Def7;
A34: len AutMt(g*f,b1,b3) = len b1 by Def8;
then
A35: i in dom b1 by A16,FINSEQ_3:29;
A36: p1 = (AutMt(g*f,b1,b3))/.i by A16,A31,PARTFUN1:def 6
.= (g*f).(b1/.i) |-- b3 by A35,Def8;
len AutMt(f,b1,b2) = len b1 by Def8;
then
A37: i in dom AutMt(f,b1,b2) by A16,A34,FINSEQ_3:29;
then
A38: Line(AutMt(f,b1,b2),i) = AutMt(f,b1,b2).i by MATRIX_0:60
.= (AutMt(f,b1,b2))/.i by A37,PARTFUN1:def 6
.= f.(b1/.i) |-- b2 by A35,Def8;
A39: Seg len b2 = dom b2 by FINSEQ_1:def 3;
j in Seg len ((g*f).(b1/.i) |-- b3) by A18,Def7;
then A40:j in dom p1 by A36,FINSEQ_1:def 3;
thus (AutMt(g*f,b1,b3))*(i,j)
= ((g*f).(b1/.i) |-- b3)/.j by A32,A36,A40,PARTFUN1:def 6
.= (g.(f.(b1/.i)) |-- b3)/.j by A30,FUNCT_1:13
.= (g.Sum(lmlt(f.(b1/.i) |-- b2,b2)) |-- b3)/.j by Th35
.= (Sum(lmlt(f.(b1/.i) |-- b2,g*b2)) |-- b3)/.j by A1,A33,Th18
.= Sum(mlt(f.(b1/.i) |-- b2,d)) by A3,A19,A9,A14,A39,A33,Th37
.= Line(AutMt(f,b1,b2),i) "*" Col(AutMt(g,b2,b3),j)
by A38,A13,A20,FINSEQ_1:14
.= ((AutMt(f,b1,b2))
* (AutMt(g,b2,b3)))*(i,j) by A4,A15,MATRIX_3:def 4;
end;
hence thesis by A7,A6,MATRIX_0:21;
end;
theorem
AutMt(f1+f2,b1,b2) = (AutMt(f1,b1,b2)) + (AutMt(f2,b1,b2))
proof
A1: len AutMt(f1+f2,b1,b2) = len b1 by Def8
.= len AutMt(f1,b1,b2) by Def8;
A3: width AutMt(f1,b1,b2) = width AutMt(f2,b1,b2)
proof
per cases;
suppose A4: len b1 = 0;
then AutMt(f1,b1,b2) = {} by Th38
.= AutMt(f2,b1,b2) by A4,Th38;
hence thesis;
end;
suppose A5: len b1 > 0;
hence width AutMt(f1,b1,b2) = len b2 by Th39
.= width AutMt(f2,b1,b2) by A5,Th39;
end;
end;
A6: width AutMt(f1+f2,b1,b2) = width AutMt(f1,b1,b2)
proof
per cases;
suppose A7: len b1 = 0;
then AutMt(f1+f2,b1,b2) = {} by Th38
.= AutMt(f1,b1,b2) by A7,Th38;
hence thesis;
end;
suppose A8: len b1 > 0;
hence width AutMt(f1+f2,b1,b2) = len b2 by Th39
.= width AutMt(f1,b1,b2) by A8,Th39;
end;
end; then
A9: width AutMt(f1+f2,b1,b2) = width ((AutMt(f1,b1,b2))
+ (AutMt(f2,b1,b2)) ) by MATRIX_1:def 6;
AX10: len AutMt(f1,b1,b2) = len b1 by Def8
.= len AutMt(f2,b1,b2) by Def8;
A11: for i, j st [i,j] in Indices (AutMt(f1+f2,b1,b2)) holds
(AutMt(f1+f2,b1,b2))*(i,j) = ((AutMt(f1,b1,b2))
+ (AutMt(f2,b1,b2)))*(i,j)
proof
let i, j;
assume A12: [i,j] in Indices (AutMt(f1+f2,b1,b2)); then
A14: [i,j] in Indices AutMt(f1,b1,b2) by A1,A6,FINSEQ_3:29;
A15: [i,j] in Indices AutMt(f2,b1,b2) by A1,A3,A6,AX10,A12,FINSEQ_3:29;
A15A: AutMt(f1+f2,b1,b2)*(i,j)
= AutMt(f1,b1,b2)*(i,j)+AutMt(f2,b1,b2)*(i,j)
proof
consider KL3 be Linear_Combination of V2 such that
A16: f2.(b1/.i) = Sum(KL3) & Carrier KL3 c= rng b2 and
A17: for t st 1<=t & t<=len (f2.(b1/.i) |-- b2) holds
(f2.(b1/.i) |-- b2)/.t=KL3.(b2/.t) by Def7;
consider KL2 be Linear_Combination of V2 such that
A18: f1.(b1/.i) = Sum(KL2) & Carrier KL2 c= rng b2 and
A19: for t st 1<=t & t<=len (f1.(b1/.i) |-- b2) holds
(f1.(b1/.i) |-- b2)/.t=KL2.(b2/.t) by Def7;
A20: i in dom AutMt(f1+f2,b1,b2) by A12,ZFMISC_1:87;
then
A21: i in dom b1 by Lm3;
reconsider b4 = rng b2 as Basis of V2 by defOrdBasis;
consider p1 be FinSequence of INT.Ring such that
A22: p1 = AutMt(f1+f2,b1,b2).i and
A23: AutMt(f1+f2,b1,b2)*(i,j) = p1.j by A12,MATRIX_0:def 5;
consider KL1 be Linear_Combination of V2 such that
A24: (f1+f2).(b1/.i) = Sum(KL1) & Carrier KL1 c= rng b2 and
A25: for t st 1<=t & t<=len ((f1+f2).(b1/.i) |-- b2) holds
((f1+f2).(b1/.i) |-- b2)/.t=KL1.(b2/.t) by Def7;
Z: b4 is linearly-independent by VECTSP_7:def 3;
(f1+f2).(b1/.i) = f1.(b1/.i) + f2.(b1/.i) by MATRLIN:def 3;
then
A26: KL1.(b2/.j) = (KL2 + KL3).(b2/.j) by A24,A18,A16,Th6,Z
.= KL2.(b2/.j) + KL3.(b2/.j) by VECTSP_6:22;
A27: p1 = (AutMt(f1+f2,b1,b2))/.i by A22,A20,PARTFUN1:def 6
.= (f1+f2).(b1/.i) |-- b2 by A21,Def8;
consider p3 be FinSequence of INT.Ring such that
A28: p3 = (AutMt(f2,b1,b2)).i and
A29: AutMt(f2,b1,b2)*(i,j) = p3.j by A15,MATRIX_0:def 5;
consider p2 be FinSequence of INT.Ring such that
A30: p2 = (AutMt(f1,b1,b2)).i and
A31: AutMt(f1,b1,b2)*(i,j) = p2.j by A14,MATRIX_0:def 5;
A32: j in Seg width AutMt(f1+f2,b1,b2) by A12,ZFMISC_1:87;
then A33: 1 <= j by FINSEQ_1:1;
len b1 = len AutMt(f1+f2,b1,b2) by Def8;
then dom b1 = dom AutMt(f1+f2,b1,b2) by FINSEQ_3:29;
then dom b1 <> {} by A12;
then Seg len b1 <> {} by FINSEQ_1:def 3;
then len b1 > 0; then
A34: j in Seg len b2 by A32,Th39; then
A35: j <= len b2 by FINSEQ_1:1;
then j <= len ((f1+f2).(b1/.i) |-- b2) by Def7; then
A36: p1/.j = KL1.(b2/.j) by A33,A27,A25;
A37: j in dom b2 by A34,FINSEQ_1:def 3;
i in dom AutMt(f2,b1,b2) by A21,Lm3; then
A38: p3 = AutMt(f2,b1,b2)/.i by A28,PARTFUN1:def 6
.= f2.(b1/.i) |-- b2 by A21,Def8;
then j in dom p3 by A37,Lm1; then
A39: AutMt(f2,b1,b2)*(i,j) = p3/.j by A29,PARTFUN1:def 6;
i in dom AutMt(f1,b1,b2) by A21,Lm3; then
A40: p2 = (AutMt(f1,b1,b2))/.i by A30,PARTFUN1:def 6
.= f1.(b1/.i) |-- b2 by A21,Def8;
then j in dom p2 by A37,Lm1; then
A41: AutMt(f1,b1,b2)*(i,j) = p2/.j by A31,PARTFUN1:def 6;
j <= len (f2.(b1/.i) |-- b2) by A35,Def7; then
A42: p3/.j = KL3.(b2/.j) by A33,A38,A17;
j <= len (f1.(b1/.i) |-- b2) by A35,Def7; then
A43: p2/.j = KL2.(b2/.j) by A33,A40,A19;
j in dom p1 by A37,A27,Lm1;
hence thesis by A23,A41,A39,A36,A43,A42,A26,PARTFUN1:def 6;
end;
thus (AutMt(f1+f2,b1,b2))*(i,j)
= ((AutMt(f1,b1,b2)))*(i,j)
+ ((AutMt(f2,b1,b2)))*(i,j) by A15A
.= ((AutMt(f1,b1,b2)) + (AutMt(f2,b1,b2)))*(i,j) by A14,MATRIX_1:def 6;
end;
len (AutMt(f1+f2,b1,b2)) = len ((AutMt(f1,b1,b2))
+ (AutMt(f2,b1,b2))) by A1,MATRIX_1:def 6;
hence thesis by A9,A11,MATRIX_0:21;
end;
theorem
a <> 0.INT.Ring implies AutMt(a*f,b1,b2) = a * (AutMt(f,b1,b2))
proof
assume
A1: a <> 0.INT.Ring;
A2: width AutMt(a*f,b1,b2) = width AutMt(f,b1,b2)
proof
per cases;
suppose A3: len b1 = 0;
then AutMt(a*f,b1,b2) = {} by Th38
.= AutMt(f,b1,b2) by A3,Th38;
hence thesis;
end;
suppose A4: len b1 > 0;
hence width AutMt(a*f,b1,b2) = len b2 by Th39
.= width AutMt(f,b1,b2) by A4,Th39;
end;
end;
A5: width AutMt(a*f,b1,b2) = width (a * (AutMt(f,b1,b2)))
by A2,MATRIX_3:def 5;
A6: len AutMt(a*f,b1,b2) = len b1 by Def8
.= len AutMt(f,b1,b2) by Def8;
A8: for i, j st [i,j] in Indices (AutMt(a*f,b1,b2))
holds (AutMt(a*f,b1,b2))*(i,j) = (a * (AutMt(f,b1,b2)))*(i,j)
proof
let i, j;
assume A9: [i,j] in Indices (AutMt(a*f,b1,b2));
then
A11: [i,j] in Indices AutMt(f,b1,b2) by A2,A6,FINSEQ_3:29;
A11A: AutMt(a*f,b1,b2)*(i,j) = a * (AutMt(f,b1,b2)*(i,j))
proof
consider p2 be FinSequence of INT such that
A12: p2 = (AutMt(f,b1,b2)).i and
A13: AutMt(f,b1,b2)*(i,j) = p2.j by A11,MATRIX_0:def 5;
A14: i in dom AutMt(a*f,b1,b2) by A9,ZFMISC_1:87; then
A15: i in dom b1 by Lm3;
then i in dom AutMt(f,b1,b2) by Lm3; then
A16: p2 = (AutMt(f,b1,b2))/.i by A12,PARTFUN1:def 6
.= f.(b1/.i) |-- b2 by A15,Def8;
reconsider b4 = rng b2 as Basis of V2 by defOrdBasis;
consider p1 be FinSequence of INT such that
A17: p1 = AutMt(a*f,b1,b2).i and
A18: AutMt(a*f,b1,b2)*(i,j) = p1.j by A9,MATRIX_0:def 5;
consider KL1 be Linear_Combination of V2 such that
A19: (a*f).(b1/.i) = Sum(KL1) & Carrier KL1 c= rng b2 and
A20: for t st 1<=t & t<=len ((a*f).(b1/.i) |-- b2) holds
((a*f).(b1/.i) |-- b2)/.t=KL1.(b2/.t) by Def7;
consider KL2 be Linear_Combination of V2 such that
A21: f.(b1/.i) = Sum(KL2) & Carrier KL2 c= rng b2 and
A22: for t st 1<=t & t<=len (f.(b1/.i) |-- b2) holds
(f.(b1/.i) |-- b2)/.t= KL2.(b2/.t) by Def7;
b4 is linearly-independent & (a*f).(b1/.i) = a * (f.(b1/.i))
by MATRLIN:def 4,VECTSP_7:def 3; then
A23: KL1.(b2/.j) = (a * KL2).(b2/.j) by A1,A19,A21,Th7
.= a * KL2.(b2/.j) by VECTSP_6:def 9;
A24: j in Seg width AutMt(a*f,b1,b2) by A9,ZFMISC_1:87; then
A25: 1 <= j by FINSEQ_1:1;
len b1 = len AutMt(a*f,b1,b2) by Def8;
then dom b1 = dom AutMt(a*f,b1,b2) by FINSEQ_3:29;
then dom b1 <> {} by A9;
then Seg len b1 <> {} by FINSEQ_1:def 3;
then len b1 > 0; then
A26: j in Seg len b2 by A24,Th39; then
A27: j <= len b2 by FINSEQ_1:1;
then j <= len (f.(b1/.i) |-- b2) by Def7; then
A28: p2/.j = KL2.(b2/.j) by A25,A16,A22;
A29: j in dom b2 by A26,FINSEQ_1:def 3;
then j in dom (f.(b1/.i) |-- b2) by Lm1; then
A30: AutMt(f,b1,b2)*(i,j) = p2/.j by A13,A16,PARTFUN1:def 6;
A31: p1 = (AutMt(a*f,b1,b2))/.i by A17,A14,PARTFUN1:def 6
.= (a*f).(b1/.i) |-- b2 by A15,Def8;
then
A32: j in dom p1 by A29,Lm1;
j <= len ((a*f).(b1/.i) |-- b2) by A27,Def7;
then p1/.j = KL1.(b2/.j) by A25,A31,A20;
hence thesis by A18,A32,A30,A28,A23,PARTFUN1:def 6;
end;
A110: [i,j] in Indices (AutMt(f,b1,b2))
by A2,A6,A9,FINSEQ_3:29;
(AutMt(a*f,b1,b2))*(i,j)
= (a * (AutMt(f,b1,b2)))*(i,j) by A11A,A110,MATRIX_3:def 5;
hence thesis;
end;
len (AutMt(a*f,b1,b2)) = len (AutMt(a*f,b1,b2))
= len (a * (AutMt(f,b1,b2))) by A6,MATRIX_3:def 5;
hence thesis by A5,A8,MATRIX_0:21;
end;
theorem LmSign1B:
for D, E being non empty set, n, m, i, j being Nat, M being Matrix of n,m,D
st 0 < n & M is Matrix of n,m,E & [i, j] in Indices M
holds M*(i,j) is Element of E
proof
let D, E be non empty set, n, m, i, j be Nat,
M be Matrix of n,m,D;
assume that
A1: 0 < n and
A2: M is Matrix of n, m, E and
A3: [i, j] in Indices M;
consider m1 be Nat such that
A4: for x being object st x in rng M
ex q being FinSequence of E st x = q & len q = m1 by A2,MATRIX_0:9;
consider p be FinSequence of D such that
A5: p = M.i & M*(i,j) = p.j by A3,MATRIX_0:def 5;
A6: i in dom M & j in Seg width M by A3,ZFMISC_1:87;
then
A7: p in rng M by A5,FUNCT_1:3;
ex q being FinSequence of E st p = q & len q = m1 by A4,A5,A6,FUNCT_1:3;
then
A50: rng p c= E by FINSEQ_1:def 4;
len p = m by A7,MATRIX_0:def 2;
then len p = width M by A1,MATRIX_0:23;
then j in dom p by A6,FINSEQ_1:def 3;
hence thesis by A5,A50,FUNCT_1:3;
end;
theorem LmSign1C:
for F be FinSequence of F_Real
st for i being Nat st i in dom F holds F.i in INT
holds Sum F in INT
proof
defpred P[Nat] means
for F being FinSequence of F_Real
st len F = $1 &
for i being Nat st i in dom F holds F.i in INT
holds Sum F in INT;
P1: P[0]
proof
let F be FinSequence of F_Real;
assume AS1: len F = 0 &
for i being Nat st i in dom F holds F.i in INT;
F = <*> the carrier of F_Real by AS1;
then Sum F = 0.F_Real by RLVECT_1:43
.= 0;
hence Sum F in INT by INT_1:def 2;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
let F be FinSequence of F_Real;
assume AS2: len F = n+1 &
for i being Nat st i in dom F holds F.i in INT;
reconsider F0 = F| n as FinSequence of F_Real;
n+1 in Seg (n+1) by FINSEQ_1:4;
then
A70: n+1 in dom F by AS2,FINSEQ_1:def 3;
then F.(n+1) in rng F by FUNCT_1:3;
then reconsider af = F.(n+1) as Element of F_Real;
P1: len F0 = n by AS2,FINSEQ_1:59,NAT_1:11;
then
P4: dom F0 = Seg n by FINSEQ_1:def 3;
A9: len F = (len F0) + 1 by AS2,FINSEQ_1:59,NAT_1:11;
A11: F0 = F | dom F0 by P4,FINSEQ_1:def 16;
then
P3: Sum F = Sum F0 + af by AS2,A9,RLVECT_1:38;
for i being Nat st i in dom F0 holds F0.i in INT
proof
let i be Nat;
assume P40: i in dom F0;
dom F = Seg (n+1) by AS2,FINSEQ_1:def 3;
then dom F0 c= dom F by P4,FINSEQ_1:5,NAT_1:11;
then F.i in INT by AS2,P40;
hence thesis by A11,P40,FUNCT_1:47;
end;
then Sum F0 in INT by P1,AS1;
then reconsider i1 = Sum F0 as Integer;
F.(n+1) in INT by A70,AS2;
then reconsider i2 = af as Integer;
Sum F = i1 + i2 by P3;
hence Sum F in INT by INT_1:def 2;
end;
X1: for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
let F be FinSequence of F_Real;
assume X2: for i being Nat st i in dom F holds F.i in INT;
len F is Nat;
hence Sum F in INT by X1,X2;
end;
theorem LmSign1D:
for i be Nat, j be Element of F_Real st j in INT
holds power(F_Real).(-1_F_Real,i)*j in INT
proof
let i be Nat,j be Element of F_Real;
assume AS: j in INT;
defpred P[Nat] means
power(F_Real).(-1_F_Real,$1 )*j in INT;
P1: P[0]
proof
power(F_Real).(-1_F_Real,0 )*j = 1_(F_Real) *j by GROUP_1:def 7
.= j;
hence thesis by AS;
end;
P2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume AS1: P[n];
P3: power(F_Real).(-1_F_Real,n+1 )*j
= ((power(F_Real).(-1_F_Real,n)) * (-1_F_Real)) *j by GROUP_1:def 7
.= (-1_F_Real) * (( power(F_Real).(-1_F_Real,n)) * j);
reconsider mi = -1_F_Real as Integer;
reconsider m0 = (power(F_Real).(-1_F_Real,n)) * j as Integer by AS1;
power(F_Real).(-1_F_Real,n+1 )*j = -m0 by P3;
hence power(F_Real).(-1_F_Real,n+1)*j in INT by INT_1:def 2;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
theorem LmSign1F:
for n, i, j, k, m being Nat, M being Matrix of n+1, F_Real
st 0 < n & M is Matrix of n+1, INT &
[i, j] in Indices M & [k, m] in Indices (Delete(M,i,j))
holds (Delete(M,i,j))*(k,m) is Element of INT
proof
let n, i, j, k, m be Nat, M be Matrix of n+1,F_Real;
assume that
0 < n and
A2: M is Matrix of n+1, INT and
A3: [i, j] in Indices M and
A4: [k, m] in Indices (Delete(M,i,j));
[i, j] in [:Seg (n+1),Seg (n+1):] by A3,MATRIX_0:24;
then
A5: i in Seg (n+1) & j in Seg (n+1) by ZFMISC_1:87;
set M0 = Delete(M,i,j);
(n+1)-'1 = n by NAT_D:34;
then len M0 = n & width M0 = n & Indices M0 = [:(Seg n),(Seg n):]
by MATRIX_0:24; then
D5: k in Seg n & m in Seg n by A4,ZFMISC_1:87;
then
D3: k in Seg ((n+1)-'1 ) & m in Seg ((n+1)-'1 ) by NAT_D:34;
FC0: 1<=k & k <= n & 1<=m & m <= n by D5,FINSEQ_1:1;
then 1<=k & k+0 <= n+1 & 1<=m & m+0 <= n+1 by XREAL_1:7;
then
FC1: k in Seg (n+1) & m in Seg (n+1) by FINSEQ_1:1;
1+0<=k+1 & k+1 <= n+1 & 1+0<=m+1 & m+1 <= n+1 by FC0,XREAL_1:6; then
FC3: k+1 in Seg (n+1) & m+1 in Seg (n+1) by FINSEQ_1:1;
per cases;
suppose k < i & m < j; then
F11: Delete(M,i,j)*(k,m) = M*(k,m) by A5,D3,LAPLACE:13;
[k, m] in [:Seg (n+1),Seg (n+1):] by FC1,ZFMISC_1:87;
then [k, m] in Indices M by MATRIX_0:24;
hence thesis by A2,F11,LmSign1B;
end;
suppose k < i & m >= j; then
F21: Delete(M,i,j)*(k,m) = M*(k,m+1) by A5,D3,LAPLACE:13;
[k, m+1] in [:Seg (n+1),Seg (n+1):] by FC1,FC3,ZFMISC_1:87;
then [k, m+1] in Indices M by MATRIX_0:24;
hence thesis by A2,F21,LmSign1B;
end;
suppose k >= i & m < j; then
F31: Delete(M,i,j)*(k,m) = M*(k+1,m) by A5,D3,LAPLACE:13;
[k+1, m] in [:Seg (n+1),Seg (n+1):] by FC1,FC3,ZFMISC_1:87;
then [k+1, m] in Indices M by MATRIX_0:24;
hence thesis by A2,F31,LmSign1B;
end;
suppose k >= i & m >= j; then
F41: Delete(M,i,j)*(k,m) = M*(k+1,m+1) by A5,D3,LAPLACE:13;
[k+1, m+1] in [:Seg (n+1),Seg (n+1):] by FC3,ZFMISC_1:87;
then [k+1, m+1] in Indices M by MATRIX_0:24;
hence thesis by A2,F41,LmSign1B;
end;
end;
theorem LmSign1E:
for n, i, j being Nat, M being Matrix of n+1, F_Real
st 0 < n & M is Matrix of n+1,INT & [i, j] in Indices M
holds Delete(M,i,j) is Matrix of n, INT
proof
let n, i, j be Nat, M be Matrix of n+1,F_Real;
assume that
A1: 0 < n and
A2:M is Matrix of n+1, INT and
A3: [i, j] in Indices M;
set M0 = Delete(M,i,j);
X39: (n+1)-'1 = n by NAT_D:34; then
D2: len M0 = n & width M0 = n & Indices M0 = [:(Seg n),(Seg n):]
by MATRIX_0:24;
for x being object st x in rng M0 holds
ex p being FinSequence of INT st x = p & len p = n
proof
let x be object;
assume S1: x in rng M0;
then reconsider p = x as FinSequence of the carrier of F_Real
by FINSEQ_2:def 3;
S3: len p = n by S1,X39,MATRIX_0:def 2;
for z being object st z in rng p holds z in INT
proof
let z be object;
assume z in rng p;
then consider j1 be object such that
S4: j1 in dom p & z = p.j1 by FUNCT_1:def 3;
S5: j1 in Seg n by S3,S4,FINSEQ_1:def 3;
reconsider j1 as Nat by S4;
consider i1 be object such that
S6: i1 in dom M0 & x = M0.i1 by S1,FUNCT_1:def 3;
reconsider i1 as Nat by S6;
S8: [i1,j1] in Indices M0 by D2,S5,S6,ZFMISC_1:87;
then consider q be FinSequence of F_Real such that
S9: q = M0.i1 & M0*(i1,j1) = q.j1 by MATRIX_0:def 5;
M0*(i1,j1) is Element of INT by A1,A2,A3,S8,LmSign1F;
hence z in INT by S4,S6,S9;
end; then
rng p c= INT;
then p is FinSequence of INT by FINSEQ_1:def 4;
hence thesis by S3;
end;
hence thesis by A1,D2,MATRIX_0:9,20;
end;
theorem LmSign1A:
for n being Nat, M being Matrix of n, F_Real
st M is Matrix of n, INT
holds Det M in INT
proof
defpred P[Nat] means
for M being Matrix of $1, F_Real st M is Matrix of $1, INT
holds Det M in INT;
P0: P[0]
proof
let M be Matrix of 0, F_Real;
assume M is Matrix of 0, INT;
Det M = 1.F_Real by MATRIXR2:41
.= 1;
hence Det M in INT by INT_1:def 2;
end;
P1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P10: P[n];
let M be Matrix of n+1, F_Real;
assume AS1: M is Matrix of n+1, INT;
reconsider j = 1 as Nat;
X0: 1 <= 1 & 1 <= n+1 by NAT_1:14;
then j in Seg (n+1) by FINSEQ_1:1; then
X1: Det M = Sum LaplaceExpC(M,j) by LAPLACE:27;
set L = LaplaceExpC(M,j);
X2: len L = n+1
& for i being Nat st i in dom L holds
L.i = M*(i,j)*Cofactor(M,i,j) by LAPLACE:def 8;
for i being Nat st i in dom L holds L.i in INT
proof
let i be Nat;
assume X30:i in dom L; then
X31: L.i = M*(i,j)*Cofactor(M,i,j) by LAPLACE:def 8;
i in Seg (n+1) & j in Seg (n+1) by X0,X2,X30,FINSEQ_1:1,def 3;
then [i,j] in [:Seg (n+1),Seg (n+1):] by ZFMISC_1:87; then
X41: [i, j] in Indices M by MATRIX_0:24; then
X32: M*(i,j) is Element of INT by AS1,LmSign1B;
(n+1)-'1 = n by NAT_D:34;
then reconsider DD= Delete(M,i,j) as Matrix of n,F_Real;
Det DD in INT
proof
per cases;
suppose 0 < n;
then DD is Matrix of n, INT by LmSign1E,AS1,X41;
hence Det DD in INT by P10;
end;
suppose not 0 < n;
then n = 0;
then Det DD = 1.F_Real by MATRIXR2:41
.= 1;
hence Det DD in INT by INT_1:def 2;
end;
end;
then Minor(M,i,j) in INT by NAT_D:34;
then Cofactor(M,i,j) in INT by LmSign1D;
hence L.i in INT by X32,X31,INT_1:def 2;
end;
hence thesis by X1,LmSign1C;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P0,P1);
hence thesis;
end;
theorem
for n being Nat, M being Matrix of n, F_Real
st M is Matrix of n, INT.Ring
holds Det M in INT by LmSign1A;
theorem
for V being finite-rank free Z_Module, I being Basis of V holds
ex J being OrdBasis of V st rng J = I
proof
let V be finite-rank free Z_Module, I be Basis of V;
consider p be FinSequence such that
A2: rng p = I and
A3: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of V by A2,FINSEQ_1:def 4;
take f = p;
thus f is one-to-one by A3;
thus thesis by A2;
end;
registration
let V be Z_Module;
cluster id V -> additive homogeneous;
correctness;
end;
theorem ThRank1:
for V being finite-rank free Z_Module, b being OrdBasis of V
holds len b = rank V
proof
let V be finite-rank free Z_Module, b be OrdBasis of V;
reconsider R = rng b as Basis of V by defOrdBasis;
A1: b is one-to-one by defOrdBasis;
thus len b = card Seg len b by FINSEQ_1:57
.= card dom b by FINSEQ_1:def 3
.= card R by A1,CARD_1:70
.= rank V by ZMODUL03:def 5;
end;
theorem LMThMBF3:
for V being finite-rank free Z_Module,
b1, b2 being OrdBasis of V holds
AutMt(id(V), b1, b2) is Matrix of rank V,INT.Ring
proof
let V be finite-rank free Z_Module,
b1, b2 be OrdBasis of V;
set n = rank V;
A1: len b1 = rank V by ThRank1;
A2: len b2 = rank V by ThRank1;
P0: len AutMt(id(V),b1,b2) = len b1 by Def8;
per cases;
suppose X1: len b1 = 0;
then len AutMt(id(V), b1, b2) = 0 by Def8;
then AutMt(id(V), b1, b2) = {};
hence thesis by A1,X1,MATRIX_0:13;
end;
suppose P1: 0 < len b1; then
width AutMt(id(V),b1,b2) = len b2 by Th39;
hence thesis by P0,P1,A1,A2,MATRIX_0:20;
end;
end;
theorem
for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V,
M being Matrix of rank(V),F_Real st M = AutMt(id(V), b1, b2)
holds Det M in INT
proof
let V be finite-rank free Z_Module,
b1, b2 be OrdBasis of V,
M be Matrix of rank(V),F_Real;
assume A2: M = AutMt(id(V), b1, b2);
per cases;
suppose not 0 < rank(V);
then rank(V) = 0;
then Det M = 1.F_Real by MATRIXR2:41;
hence Det M in INT;
end;
suppose A3: 0 < rank(V);
len M = rank(V) & width M = rank(V) by MATRIX_0:24;
then M is Matrix of rank(V),INT by A2,A3,MATRIX_0:20;
hence thesis by LmSign1A;
end;
end;
theorem LmSign31X:
for V1 being finite-rank free Z_Module,
b1 being OrdBasis of V1 holds
for i,j be Nat
st i in dom b1 & j in dom b1 holds
( i = j implies ((b1/.i) |-- b1).j = 1 )
& ( i <> j implies ((b1/.i) |-- b1).j = 0 )
proof
let V1 be finite-rank free Z_Module,
b1 be OrdBasis of V1;
let i, j be Nat;
assume that
A5: i in dom b1 and
A18: j in dom b1;
set bb= (b1/.i) |-- b1;
consider KL be Linear_Combination of V1 such that
A1: b1/.i = Sum(KL) & Carrier KL c= rng b1 and
A2: for k st 1<=k & k<=len bb holds bb/.k=KL.(b1/.k) by Def7;
reconsider rb1=rng b1 as Basis of V1 by defOrdBasis;
b1/.i in {b1/.i} by TARSKI:def 1;
then b1/.i in Lin{b1/.i} by ZMODUL02:65;
then consider Lb be Linear_Combination of {b1/.i} such that
A4: b1/.i=Sum Lb by ZMODUL02:64;
A6: b1.i=b1/.i by A5,PARTFUN1:def 6; then
A7: Carrier Lb c= {b1.i} by VECTSP_6:def 4;
A8: b1.i in rb1 by A5,FUNCT_1:def 3;
then {b1.i}c= rb1 by ZFMISC_1:31;
then Carrier Lb c= rb1 by A7; then
A9: Lb = KL by A4,A1,Th5,VECTSP_7:def 3;
A12: len b1=len bb by Def7;
A13: b1/.i<>0.V1 by A6,A8,VECTSP_7:def 3,ZMODUL02:57;
j in Seg len b1 by A18,FINSEQ_1:def 3; then
A15: 1<=j & j<=len bb by A12,FINSEQ_1:1;
A19: dom bb=dom b1 by A12,FINSEQ_3:29;
set One = 1.INT.Ring;
reconsider KLi = KL.(b1/.i) as Element of INT.Ring;
now
assume A20: i = j;
KLi *(b1/.i) = b1/.i by A4,A9,ZMODUL02:21
.= One *(b1/.i);
then KLi = One by A13,ZMODUL01:11;
hence 1 = bb/.j by A2,A15,A20
.= bb.j by A18,A19,PARTFUN1:def 6;
end;
hence i = j implies ((b1/.i) |-- b1).j = 1;
now
assume
A22: i <> j;
b1 is one-to-one by defOrdBasis;
then b1.i <> b1.j by A5,A18,A22; then
A23: not b1.j in Carrier Lb by A7,TARSKI:def 1;
b1.j = b1/.j by A18,PARTFUN1:def 6;
hence 0 = KL.(b1/.j) by A9,A23
.= bb/.j by A2,A15
.= bb.j by A18,A19,PARTFUN1:def 6;
end;
hence i <> j implies ((b1/.i) |-- b1).j = 0;
end;
theorem LmSign31:
for V being finite-rank free Z_Module, b1 being OrdBasis of V
st rank(V) > 0 holds
AutMt(id(V), b1, b1) = 1.(INT.Ring,rank(V))
proof
let V be finite-rank free Z_Module, b1 be OrdBasis of V;
assume AS:rank(V) > 0;
B0: len b1 = rank(V) by ThRank1;
B1: len AutMt(id(V), b1, b1) = rank(V) by B0,Def8;
B3: width AutMt(id(V),b1,b1) = rank(V) by AS,B0,Th39;
P1: len AutMt(id(V), b1, b1) = len 1.(INT.Ring,rank(V))
by B1,MATRIX_0:24;
P4: dom AutMt(id(V), b1, b1)
= Seg len AutMt(id(V), b1, b1) by FINSEQ_1:def 3
.= dom (1.(INT.Ring,rank(V))) by P1,FINSEQ_1:def 3;
P2: width AutMt(id(V), b1, b1) = width (1.(INT.Ring,rank(V)))
by B3,MATRIX_0:24;
P5: Indices AutMt(id(V), b1, b1) = Indices (1.(INT.Ring,rank(V)))
by B3,P4,MATRIX_0:24;
X2:
now
let i, j be Nat;
assume X20: [i,j] in Indices AutMt(id(V), b1, b1); then
X21: i in dom AutMt(id(V), b1, b1)
& j in Seg width AutMt(id(V), b1, b1) by ZFMISC_1:87;
dom AutMt(id(V), b1, b1) = Seg len AutMt(id(V), b1, b1)
by FINSEQ_1:def 3
.= Seg len b1 by Def8
.= dom b1 by FINSEQ_1:def 3;
then
X23: i in dom b1 by X20,ZFMISC_1:87;
width AutMt(id(V),b1,b1) = len b1 by Th39,AS,B0;
then
Y23: j in dom b1 by X21,FINSEQ_1:def 3;
X25: AutMt(id(V), b1, b1)/.i = id(V).(b1/.i) |-- b1 by Def8,X23;
consider q be FinSequence of INT such that
X26: q = AutMt(id(V), b1, b1).i
& AutMt(id(V), b1, b1)*(i,j) = q.j by X20,MATRIX_0:def 5;
X27: AutMt(id(V), b1, b1)*(i,j)
= ((b1/.i) |-- b1).j by X21,X25,X26,PARTFUN1:def 6;
thus i <> j implies AutMt(id(V), b1, b1)*(i,j) = 0
by X23,X27,Y23,LmSign31X;
thus i = j implies AutMt(id(V), b1, b1)*(i,j) = 1
by X23,X27,LmSign31X;
end;
for i, j being Nat st [i,j] in Indices AutMt(id(V), b1, b1)
holds AutMt(id(V), b1, b1)*(i,j) = 1.(INT.Ring,rank V)*(i,j)
proof
let i, j be Nat;
assume P6: [i,j] in Indices AutMt(id(V), b1, b1);
per cases;
suppose P8: i <> j;
then 1.(INT.Ring,rank(V))*(i,j) = 0.INT.Ring
by P5,P6,MATRIX_1:def 3;
hence AutMt(id(V), b1, b1)*(i,j) = 1.(INT.Ring,rank(V))*(i,j)
by P6,P8,X2;
end;
suppose P10: i = j;
then 1.(INT.Ring,rank(V))*(i,j) = 1.INT.Ring by P5,P6,MATRIX_1:def 3;
hence AutMt(id(V), b1, b1)*(i,j) = 1.(INT.Ring,rank(V))*(i,j)
by P6,P10,X2;
end;
end;
hence thesis by P1,P2,EQ40;
end;
theorem LmSign3:
for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V
st rank(V) > 0
holds (AutMt(id(V), b1, b2)) * (AutMt(id(V), b2, b1)) = 1.(INT.Ring,rank(V))
proof
let V be finite-rank free Z_Module, b1, b2 be OrdBasis of V;
assume AS: rank(V) > 0;
then A1: len b1 > 0 & len b2 > 0 by ThRank1;
thus (AutMt(id(V), b1, b2))
* (AutMt(id(V), b2, b1)) =
AutMt(id(V)*id(V), b1, b1) by A1,ThComp1
.= AutMt(id(V), b1, b1) by FUNCT_2:17
.= 1.(INT.Ring,rank(V)) by AS,LmSign31;
end;
theorem ThSign1:
for V being finite-rank free Z_Module, b1, b2 being OrdBasis of V,
M being Matrix of rank(V),INT.Ring st M = AutMt(id(V), b1, b2)
holds |. Det M .| = 1
proof
let V be finite-rank free Z_Module, b1, b2 be OrdBasis of V,
M be Matrix of rank(V),INT.Ring;
assume AS1: M = AutMt(id(V), b1, b2);
per cases;
suppose rank(V) = 0;
then Det M = 1.INT.Ring by MATRIXR2:41;
hence thesis by ABSVALUE:def 1;
end;
suppose AS2: rank(V) > 0; then
as2: rank V >= 1+0 by NAT_1:13;
B0: len b1 = rank(V) by ThRank1;
B1: len AutMt(id(V), b2, b1) = len b2 by Def8
.= rank(V) by ThRank1;
len b2 = rank(V) by ThRank1;
then width AutMt(id(V), b2, b1) = len b1 by AS2,Th39;
then reconsider M2 = AutMt(id(V), b2, b1) as Matrix of rank(V),INT.Ring
by AS2,B0,B1,MATRIX_0:20;
M = AutMt(id(V), b1, b2) by AS1; then
A1: M * M2 = 1.(INT.Ring,rank(V)) by AS2,LmSign3;
reconsider MM2 = M*M2 as Matrix of rank(V),INT.Ring;
A2: (Det M) * (Det M2) = Det (MM2) by AS2,MATRIX11:62
.= 1_INT.Ring by A1,as2,MATRIX_7:16
.= 1.INT.Ring;
reconsider i = Det M as Integer;
reconsider j = Det M2 as Integer;
i * j = 1 by A2;
then i = 1 & j = 1 or i = -1 & j = -1 by INT_1:9;
then |. i .| = 1 or |. i .| = -(-1) by ABSVALUE:def 1;
hence thesis;
end;
end;
begin :: Real-valued Function of Z_Module
registration
let V be non empty ModuleStr over INT.Ring;
cluster additive homogeneous 0-preserving for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
definition
let V be non empty ModuleStr over INT.Ring;
mode linear-Functional of V is additive homogeneous Functional of V;
end;
theorem VS10Th1:
for a being Element of INT.Ring, V being add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over INT.Ring,
v being Vector of V
holds (0.INT.Ring)*v = 0.V & a*(0.V) = 0.V
proof
let x be Element of INT.Ring;
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, v be Vector of V;
A1: v+(0.INT.Ring)*v = 1.INT.Ring*v + (0.INT.Ring)*v by VECTSP_1:def 17
.= (1.INT.Ring+0.INT.Ring)*v by VECTSP_1:def 15
.= v + 0.V by VECTSP_1:def 17;
hence (0.INT.Ring)*v = 0.V by RLVECT_1:8;
hence x*(0.V) = (x*0.INT.Ring)*v by VECTSP_1:def 16
.= 0.V by A1,RLVECT_1:8;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster additive 0-preserving for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
registration
let V be right_zeroed non empty ModuleStr over INT.Ring;
cluster additive -> 0-preserving for Functional of V;
coherence
proof
let f be Functional of V;
assume
A1: f is additive;
f.(0.V) = f.(0.V+0.V) by RLVECT_1:def 4
.= f.(0.V) + f.(0.V) by A1;
hence f.(0.V) = 0.INT.Ring;
end;
end;
registration
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring;
cluster homogeneous -> 0-preserving for Functional of V;
coherence
proof
let f be Functional of V;
assume
A1: f is homogeneous;
thus f.(0.V) = f.(0.INT.Ring * 0.V) by VS10Th1
.= 0.INT.Ring * f.(0.V) by A1
.= 0.INT.Ring;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster 0Functional(V) -> constant;
coherence;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster constant for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
definition
let V be right_zeroed non empty ModuleStr over INT.Ring;
let f be 0-preserving Functional of V;
redefine attr f is constant means :: redefines constant (FUNCT_1, definition)
f = 0Functional(V);
compatibility
proof
A1: f.(0.V) = 0.INT.Ring &
the carrier of V = dom f by FUNCT_2:def 1,HAHNBAN1:def 9;
hereby
assume f is constant;
then for v be Vector of V holds f.v = (0Functional(V)).v by A1;
hence f = 0Functional(V) by FUNCT_2:63;
end;
assume
A3: f = 0Functional(V);
now
let x, y be object;
assume x in dom f & y in dom f;
then reconsider v = x, w = y as Vector of V;
thus f.x = (0Functional(V)).v by A3
.= 0
.= (0Functional(V)).w
.= f.y by A3;
end;
hence thesis;
end;
end;
registration
let V be right_zeroed non empty ModuleStr over INT.Ring;
cluster constant additive 0-preserving for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
LMPROJ1:
for V being free Z_Module, A,B being Subset of V
st A c= B & B is Basis of V holds
ex F being linear-transformation of V, V
st ( for v being Vector of V holds
ex vA, vB being Vector of V st vA in Lin A
& vB in Lin (B \ A) & v = vA+vB & F.v = vA ) &
for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A)
& v = vA + vB holds F.v =vA
proof
let V be free Z_Module,
A, B be Subset of V;
assume A c= B & B is Basis of V; then
P0: V is_the_direct_sum_of Lin A, Lin (B \ A) by ZMODUL05:50;
defpred P[Element of V, object ] means
ex vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A)
& $1 =vA+vB & $2 = vA;
A1: for v being Element of V holds ex vA being Element of V st P[v,vA]
proof
let v be Element of V;
consider vA, vB be Vector of V such that
A2: vA in Lin A & vB in Lin (B \ A) & v = vA+vB by P0,ZMODUL01:133;
take vA;
thus thesis by A2;
end;
consider f be Function of V, V such that
A9: for v being Vector of V holds P[v,f.v] from FUNCT_2:sch 3(A1);
A10:for v, vA, vB being Vector of V
st vA in Lin A & vB in Lin (B \ A) & v = vA + vB
holds f.v = vA
proof
let v, vA, vB be Vector of V;
assume A11:
vA in Lin A & vB in Lin (B \ A) & v = vA + vB;
consider vA1, vB1 be Vector of V such that
A12: vA1 in Lin A & vB1 in Lin (B \ A) & v = vA1 + vB1 & f.v = vA1 by A9;
thus thesis by A11,A12,P0,ZMODUL01:134;
end;
A13: f is additive
proof
let x, y be Element of V;
consider xA, xB be Vector of V such that
A14: xA in Lin A & xB in Lin (B \ A) & x = xA+xB & f.x = xA by A9;
consider yA, yB be Vector of V such that
A15: yA in Lin A & yB in Lin (B \ A) & y = yA+yB & f.y = yA by A9;
consider xyA, xyB be Vector of V such that
A16: xyA in Lin A & xyB in Lin (B \ A) & x+y = xyA+xyB & f.(x+y) = xyA
by A9;
A17: xyA+xyB = (xA+xB+yA)+yB by A14,A15,A16,RLVECT_1:def 3
.= (xB+(xA+yA))+yB by RLVECT_1:def 3
.= (xA+yA)+(xB+yB) by RLVECT_1:def 3;
A18: xA+yA in Lin A by A14,A15,ZMODUL01:36;
xB+yB in Lin (B \ A) by A14,A15,ZMODUL01:36;
hence f.(x+y) = f.x + f.y by A14,A15,A16,A17,A18,P0,ZMODUL01:134;
end;
for r being Element of INT.Ring, x being Element of V holds
f.(r*x) = r*f.x
proof
let r be Element of INT.Ring, x be Element of V;
consider xA, xB be Vector of V such that
A14: xA in Lin A & xB in Lin (B \ A) & x = xA+xB & f.x = xA by A9;
consider rxA, rxB be Vector of V such that
A15: rxA in Lin A & rxB in Lin (B \ A) & r*x = rxA+rxB
& f.(r*x) = rxA by A9;
A16: rxA+rxB = r*xA + r*xB by A14,A15,VECTSP_1:def 14;
A18: r*xA in Lin A by A14,ZMODUL01:37;
r*xB in Lin (B \ A) by A14,ZMODUL01:37;
hence f.(r*x) = r*f.x by A14,A15,A16,A18,P0,ZMODUL01:134;
end;
then f is homogeneous;
then reconsider f as linear-transformation of V, V by A13;
take f;
thus thesis by A10,A9;
end;
definition
let V be free Z_Module,
A,B be Subset of V;
assume AS: A c= B & B is Basis of V;
func Proj(A,B) -> linear-transformation of V, V means
( for v being Vector of V holds
ex vA, vB being Vector of V st
vA in Lin A & vB in Lin (B \ A) & v = vA+vB & it.v = vA )
& for v, vA, vB being Vector of V
st vA in Lin A & vB in Lin (B \ A) & v = vA + vB
holds it.v = vA;
existence by LMPROJ1,AS;
uniqueness
proof
let F1, F2 be linear-transformation of V, V;
assume
A1: ( for v being Vector of V holds
ex vA, vB being Vector of V
st vA in Lin A & vB in Lin (B \ A) & v = vA+vB & F1.v = vA ) &
for v,vA,vB be Vector of V
st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds F1.v = vA;
assume
A2: ( for v being Vector of V holds
ex vA, vB being Vector of V
st vA in Lin A & vB in Lin (B \ A) & v = vA+vB & F2.v = vA ) &
for v, vA, vB being Vector of V
st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds F2.v = vA;
now
let v be Vector of V;
consider vA, vB be Vector of V such that
A3: vA in Lin A & vB in Lin (B \ A) & v = vA+vB & F1.v = vA by A1;
thus F1.v = F2.v by A2,A3;
end;
hence F1 = F2 by FUNCT_2:def 7;
end;
end;
definition
let V be free Z_Module,
B be Basis of V,
u be Vector of V;
func Coordinate(u,B) -> Function of V, INT.Ring means
:defCoord:
( for v being Vector of V holds
ex Lu being Linear_Combination of B st v = Sum Lu & it.v = Lu.u )
& (for v being Vector of V, Lv being Linear_Combination of B
st v = Sum Lv holds it.v = Lv.u )
& ( for v1, v2 being Vector of V holds it.(v1+v2) = it.v1 + it.v2 )
& ( for v being Vector of V, r being Element of INT.Ring holds
it.(r*v) = r*it.v );
existence
proof
X1: B is linearly-independent & Lin (B) = the ModuleStr of V
by VECTSP_7:def 3;
defpred P[Element of V, object] means
ex L being Linear_Combination of B st $1=Sum L & $2=L.u;
A1: for v being Element of V holds
ex r being Element of INT.Ring st P[v,r]
proof
let v be Element of V;
v in Lin(B) by X1;
then consider Lv be Linear_Combination of B such that
A4: v=Sum Lv by ZMODUL02:64;
reconsider r = Lv.u as Element of INT.Ring;
take r;
thus thesis by A4;
end;
consider f be Function of V, the carrier of INT.Ring such that
A9: for v being Vector of V holds P[v,f.v] from FUNCT_2:sch 3(A1);
A10: for v being Vector of V, Lv be Linear_Combination of B
st v = Sum Lv holds f.v = Lv.u
proof
let v be Vector of V, Lv be Linear_Combination of B;
assume A11: v = Sum Lv;
consider L be Linear_Combination of B such that
A12: v = Sum L & f.v = L.u by A9;
Carrier L c= B & Carrier Lv c= B by VECTSP_6:def 4;
hence f.v = Lv.u by A11,A12,Th5,VECTSP_7:def 3;
end;
A15: for v1,v2 being Vector of V holds f.(v1+v2) = f.v1 + f.v2
proof
let v1, v2 be Vector of V;
consider Lv1 be Linear_Combination of B such that
P1: v1 = Sum Lv1 & f.v1 = Lv1.u by A9;
consider Lv2 be Linear_Combination of B such that
P2: v2 = Sum Lv2 & f.v2 = Lv2.u by A9;
consider Lv12 be Linear_Combination of B such that
P3: v1+v2 = Sum Lv12 & f.(v1+v2) = Lv12.u by A9;
Carrier Lv1 c= B & Carrier Lv2 c= B
& Carrier Lv12 c= B by VECTSP_6:def 4;
then S: Lv12 = Lv1 + Lv2 by P1,P2,P3,Th6,VECTSP_7:def 3;
f.(v1 + v2) = Lv12.u by P3
.= Lv1.u + Lv2.u by S,VECTSP_6:22
.= f.v1 + f.v2 by P1,P2;
hence f.(v1+v2) = f.v1+f.v2;
end;
A15A: f.(0.V) = f.(0.V + 0.V)
.= f.(0.V) +f.(0.V) by A15;
A16: for v being Vector of V, r being Element of INT.Ring
holds f.(r*v) = r*f.v
proof
let v be Vector of V, r be Element of INT.Ring;
per cases;
suppose r = 0.INT.Ring;
hence f.(r*v) = r*f.v by A15A,ZMODUL01:1;
end;
suppose A162: r <> 0.INT.Ring;
consider Lv be Linear_Combination of B such that
P1: v = Sum Lv & f.v = Lv.u by A9;
consider rLv be Linear_Combination of B such that
P2: r*v = Sum rLv & f.(r*v) = rLv.u by A9;
Carrier Lv c= B & Carrier rLv c= B by VECTSP_6:def 4; then
r*Lv = rLv by A162,P1,P2,Th7,VECTSP_7:def 3;
hence f.(r*v) = r*f.v by P1,P2,VECTSP_6:def 9;
end;
end;
take f;
thus thesis by A9,A10,A15,A16;
end;
uniqueness
proof
let f1, f2 be Function of V,INT.Ring;
assume
A1: ( for v being Vector of V holds
ex Lu being Linear_Combination of B st v=Sum Lu & f1.v = Lu.u)
& (for v being Vector of V, Lv being Linear_Combination of B
st v = Sum Lv holds f1.v = Lv.u )
& ( for v1, v2 being Vector of V
holds f1.(v1+v2) = f1.v1 + f1.v2 )
& ( for v being Vector of V, r being Element of INT.Ring holds
f1.(r*v) = r*f1.v );
assume
A2: ( for v being Vector of V holds ex Lu being Linear_Combination of B
st v = Sum Lu & f2.v = Lu.u )
& (for v being Vector of V, Lv being Linear_Combination of B
st v = Sum Lv holds f2.v = Lv.u )
& ( for v1, v2 being Vector of V holds f2.(v1+v2) = f2.v1 + f2.v2 )
& ( for v being Vector of V, r being Element of INT.Ring
holds f2.(r*v) = r*f2.v );
now
let v be Vector of V;
consider Lu be Linear_Combination of B such that
A3: v = Sum Lu & f1.v = Lu.u by A1;
thus f1.v = f2.v by A2,A3;
end;
hence f1 = f2 by FUNCT_2:def 7;
end;
end;
theorem PROJ4:
for V being free Z_Module, B being Basis of V, u being Vector of V
holds Coordinate(u,B).(0.V) = 0
proof
let V be free Z_Module,
B be Basis of V,
u be Vector of V;
set f = Coordinate(u,B);
f.(0.V) = f.(0.V + 0.V)
.= f.(0.V) +f.(0.V) by defCoord;
hence f.(0.V) = 0;
end;
theorem PROJ5:
for V being free Z_Module, X being Basis of V, v being Vector of V
st v in X & v <> 0.V holds Coordinate(v,X).v = 1
proof
let V be free Z_Module,
X be Basis of V,
v be Vector of V;
assume AS: v in X & v <> 0.V;
set f = Coordinate(v,X);
consider KL be Linear_Combination of X such that
A1: v = Sum KL & f.v = KL.v by defCoord;
A3: Carrier KL c= X by VECTSP_6:def 4;
v in {v} by TARSKI:def 1;
then v in Lin{v} by ZMODUL02:65;
then consider Lb be Linear_Combination of {v} such that
A4: v = Sum Lb by ZMODUL02:64;
A7: Carrier Lb c= {v} by VECTSP_6:def 4;
{v} c= X by AS,ZFMISC_1:31;
then Carrier Lb c= X by A7;
then
A9: Lb = KL by A4,A1,A3,Th5,VECTSP_7:def 3;
Lb.v * v = v by A4,ZMODUL02:21
.= (1.INT.Ring)*v;
hence f.v = 1 by AS,A1,A9,ZMODUL01:11;
end;
registration
let V be non trivial free Z_Module;
cluster additive homogeneous non constant non trivial for Functional of V;
existence
proof
set X = the Basis of V;
X1: X is linearly-independent & Lin (X) = the ModuleStr of V
by VECTSP_7:def 3;
X <> {}
proof
assume X = {};
then X = {}(the carrier of V); then
X3: the ModuleStr of V = (0).V by X1,ZMODUL02:67;
for x, y being object
st x in the carrier of V & y in the carrier of V holds x = y
proof
let x, y be object;
assume x in the carrier of V & y in the carrier of V; then
reconsider x1 = x, y1 = y as Vector of V;
x1 in (0).V & y1 in (0).V by X3;
then x1 = 0.V & y1 = 0.V by ZMODUL02:66;
hence thesis;
end;
then V is trivial;
hence contradiction;
end;
then consider v be object such that
X2: v in X by XBOOLE_0:def 1;
reconsider v as Vector of V by X2;
X20: v <> 0.V by X2,VECTSP_7:def 3,ZMODUL02:57;
reconsider f = Coordinate(v,X)
as Function of V, INT.Ring;
DM1: dom f = the carrier of V by FUNCT_2:def 1;
J1: f.(0.V) = 0 by PROJ4;
A16: f.v = 1 by X2,X20,PROJ5;
take f;
thus thesis by A16,DM1,J1,defCoord;
end;
end;
theorem VS10Th28:
for V being non trivial free Z_Module,
f being non constant 0-preserving Functional of V
ex v being Vector of V st v <> 0.V & f.v <> 0.INT.Ring
proof
let V be non trivial free Z_Module,
f be non constant 0-preserving Functional of V;
A1: f.(0.V) = 0.INT.Ring by HAHNBAN1:def 9;
assume
A2: for v being Vector of V st v <> 0.V holds f.v = 0.INT.Ring;
now
let x, y be object;
assume x in dom f & y in dom f;
then reconsider v = x, w = y as Vector of V;
thus f.x = f.v
.= 0 by A2,A1
.= f.w by A2,A1
.= f.y;
end;
hence contradiction by FUNCT_1:def 10;
end;
begin :: Bilinear form of Z_Module
definition
let V,W be ModuleStr over INT.Ring;
func NulForm(V,W) -> Form of V,W equals
[:the carrier of V,the carrier of W:] --> 0.INT.Ring;
coherence;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f, g be Form of V,W;
func f+g -> Form of V,W means
:BLDef2:
for v being Vector of V, w being Vector of W holds
it.(v,w) = f.(v,w)+g.(v,w);
existence
proof
set X = the carrier of V, Y = the carrier of W;
deffunc F(Element of X, Element of Y) = f.($1,$2)+g.($1,$2);
consider ff be Function of [:X,Y:],INT.Ring such that
A1: for x being Element of X for y being Element of Y holds ff.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider ff as Form of V,W;
take ff;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Form of V, W such that
A2: for v being Vector of V, w being Vector of W holds
F.(v,w) = f.(v,w)+g.(v,w)
and
A3: for v being Vector of V, w being Vector of W holds
G.(v,w) = f.(v,w)+g.(v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = f.(v,w)+g.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W;
let a be Element of INT.Ring;
func a*f -> Form of V,W means
:BLDef3:
for v being Vector of V, w being Vector of W holds it.(v,w) = a*f.(v,w);
existence
proof
reconsider aa = a as Element of INT.Ring;
set X = the carrier of V, Y = the carrier of W;
deffunc F(Element of X, Element of Y) = In(aa*f.($1,$2),
the carrier of INT.Ring);
consider ff be Function of [:X,Y:],INT.Ring such that
A1: for x being Element of X for y being Element of Y holds ff.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider ff as Form of V,W;
take ff;
let v be Vector of V, w be Vector of W;
ff.(v,w) = F(v,w) by A1; then
ff.(v,w) = a*f.(v,w);
hence thesis;
end;
uniqueness
proof
let F,G be Form of V, W such that
A2: for v being Vector of V, w be Vector of W holds F.(v,w) = a*f.(v,w) and
A3: for v being Vector of V, w be Vector of W holds G.(v,w) = a*f.(v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = a*f.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W;
func -f -> Form of V,W means
:BLDef4:
for v being Vector of V, w being Vector of W holds it.(v,w) = -f.(v,w);
existence
proof
set X = the carrier of V, Y = the carrier of W;
deffunc F(Element of X,Element of Y) = In(-f.($1,$2),the carrier of
INT.Ring);
consider ff be Function of [:X,Y:],INT.Ring such that
A1: for x being Element of X for y being Element of Y holds ff.(x,y)=F(x,y)
from BINOP_1:sch 4;
reconsider ff as Form of V,W;
take ff;
let v be Vector of V, w be Vector of W;
ff.(v,w) = F(v,w) by A1; then
ff.(v,w) = -f.(v,w);
hence thesis;
end;
uniqueness
proof
let F,G be Form of V, W such that
A2: for v being Vector of V, w being Vector of W holds
F.(v,w) = -f.(v,w) and
A3: for v being Vector of V, w being Vector of W holds
G.(v,w) = -f.(v,w);
now
let v be Vector of V, w be Vector of W;
thus F.(v,w) = -f.(v,w) by A2
.= G.(v,w) by A3;
end;
hence thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W;
redefine func -f equals :: redefines - (ZMATRLIN, definition)
(- 1.INT.Ring) * f;
compatibility
proof
let g be Form of V,W;
thus g= -f implies g = (- 1.INT.Ring) *f
proof
assume
A1: g =-f;
now
let v be Vector of V, w be Vector of W;
thus g.(v,w)= -f.(v,w) by A1,BLDef4
.= (-1.INT.Ring) * f.(v,w)
.=((-1.INT.Ring) *f).(v,w) by BLDef3;
end;
hence thesis;
end;
assume
A2: g = (-1.INT.Ring) *f;
now
let v be Vector of V, w be Vector of W;
thus g.(v,w)= (-1.INT.Ring)* f.(v,w) by A2,BLDef3
.=- f.(v,w)
.= (-f).(v,w) by BLDef4;
end;
hence thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f, g be Form of V,W;
func f-g -> Form of V,W equals
f + -g;
correctness;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f, g be Form of V,W;
redefine func f - g means :BLDef7: :: redefines - (ZMATRLIN, definition)
for v being Vector of V, w being Vector of W holds
it.(v,w) = f.(v,w) - g.(v,w);
compatibility
proof
let h be Form of V,W;
thus h = f - g implies for v being Vector of V, w being Vector of W holds
h.(v,w) = f.(v,w) - g.(v,w)
proof
assume
A1: h = f-g;
let v be Vector of V, w be Vector of W;
thus h.(v,w) = f.(v,w) + (-g).(v,w) by A1,BLDef2
.= f.(v,w) -g.(v,w) by BLDef4;
end;
assume
A2: for v being Vector of V, w being Vector of W holds
h.(v,w) = f.(v,w) - g .(v,w);
now
let v be Vector of V, w be Vector of W;
thus h.(v,w) = f.(v,w) - g.(v,w) by A2
.= f.(v,w) + (-g).(v,w) by BLDef4
.= (f-g).(v,w) by BLDef2;
end;
hence thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f, g be Form of V,W;
redefine func f+g; :: redefines + (ZMATRLIN, definition)
commutativity
proof
let f,g be Form of V,W;
now
let v be Vector of V,w be Vector of W;
thus (f+g).(v,w) = f.(v,w) + g.(v,w) by BLDef2
.= (g+f).(v,w) by BLDef2;
end;
hence f+g = g+f;
end;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W
holds f + NulForm(V,W) = f
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V,W;
set g = NulForm(V,W);
now
let v be Vector of V, w be Vector of W;
thus (f+g).(v,w) = f.(v,w) + g.(v,w) by BLDef2
.= f.(v,w) + 0 by FUNCOP_1:70
.= f.(v,w);
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f, g, h being Form of V,W
holds f+g+h = f+(g+h)
proof
let V, W be non empty ModuleStr over INT.Ring, f, g, h be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus (f+g+h).(v,w) = (f+g).(v,w) + h.(v,w) by BLDef2
.= f.(v,w) + g.(v,w)+ h.(v,w) by BLDef2
.= f.(v,w) + (g.(v,w)+ h.(v,w))
.= f.(v,w) + (g+h).(v,w) by BLDef2
.= (f+ (g+h)).(v,w) by BLDef2;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W
holds f - f = NulForm(V,W)
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus (f-f).(v,w) = f.(v,w) - f.(v,w) by BLDef7
.= (NulForm(V,W)).(v,w) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring,
a being Element of INT.Ring,
f, g being Form of V,W holds a*(f+g) = a*f+a*g
proof
let V, W be non empty ModuleStr over INT.Ring, r be Element of INT.Ring,
f,g be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus (r*(f+g)).(v,w) = r * (f+g).(v,w) by BLDef3
.= r*(f.(v,w) + g.(v,w)) by BLDef2
.= r*f.(v,w) + r*g.(v,w)
.= (r*f).(v,w) + r*g.(v,w) by BLDef3
.= (r*f).(v,w) + (r*g).(v,w) by BLDef3
.= (r*f + r*g).(v,w) by BLDef2;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring,
a, b being Element of INT.Ring,
f being Form of V,W holds (a+b)*f = a*f+b*f
proof
let V, W be non empty ModuleStr over INT.Ring,
r,s be Element of INT.Ring,
f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((r+s)*f).(v,w) = (r+s) * f.(v,w) by BLDef3
.= r*f.(v,w) + s*f.(v,w)
.= (r*f).(v,w) + s*f.(v,w) by BLDef3
.= (r*f).(v,w) + (s*f).(v,w) by BLDef3
.= (r*f + s*f).(v,w) by BLDef2;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring,
a, b being Element of INT.Ring,
f being Form of V,W holds (a*b)*f = a*(b*f)
proof
let V, W be non empty ModuleStr over INT.Ring,
r, s be Element of INT.Ring,
f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((r*s)*f).(v,w) = (r*s) * f.(v,w) by BLDef3
.= r*(s*f.(v,w))
.= r*(s*f).(v,w) by BLDef3
.= (r*(s*f)).(v,w) by BLDef3;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W holds
(1.INT.Ring)*f = f
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V,W;
now
let v be Vector of V, w be Vector of W;
thus ((1.INT.Ring)*f).(v,w) = (1.INT.Ring) * f.(v,w) by BLDef3
.= f.(v,w);
end;
hence thesis;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W, v be Vector of V;
func FunctionalFAF(f,v) -> Functional of W equals
(curry f).v;
correctness;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W, w be Vector of W;
func FunctionalSAF(f,w) -> Functional of V equals
(curry' f).w;
correctness;
end;
theorem BLTh8:
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W,
v being Vector of V
holds dom (FunctionalFAF(f,v)) = the carrier of W &
rng (FunctionalFAF(f,v)) c= the carrier of INT.Ring &
for w be Vector of W holds (FunctionalFAF(f,v)).w = f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W, v be Vector of V;
set F = FunctionalFAF(f,v);
dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
then
A1: ex g being Function st (curry f).v = g & dom g = the carrier of W &
rng g c= rng f & for y being object st y in the carrier of W holds
g.y = f.(v,y) by FUNCT_5:29;
hence dom F = the carrier of W & rng F c= the carrier of INT.Ring;
let y be Vector of W;
thus thesis by A1;
end;
theorem BLTh9:
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W,
w being Vector of W holds
dom (FunctionalSAF(f,w)) = the carrier of V &
rng (FunctionalSAF(f,w)) c= the carrier of INT.Ring & for v be Vector of V
holds (FunctionalSAF(f,w)).v = f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V, W,
w be Vector of W;
set F = FunctionalSAF(f,w);
dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
then
A1: ex g being Function st (curry' f).w = g & dom g = the carrier of V &
rng g c= rng f & for y being object st y in the carrier of V holds
g .y = f.(y,w) by FUNCT_5:32;
hence dom F = the carrier of V & rng F c= the carrier of INT.Ring;
let v be Vector of V;
thus thesis by A1;
end;
theorem BLTh10:
for V, W being non empty ModuleStr over INT.Ring, v being Vector of V holds
FunctionalFAF(NulForm(V,W),v) = 0Functional(W)
proof
let V, W be non empty ModuleStr over INT.Ring, v be Vector of V;
set N = NulForm(V,W);
now
let y be Vector of W;
thus FunctionalFAF(N,v).y = N.(v,y) by BLTh8
.= 0.INT.Ring by FUNCOP_1:70
.= (0Functional(W)).y;
end;
hence thesis by FUNCT_2:63;
end;
theorem BLTh11:
for V, W being non empty ModuleStr over INT.Ring, w being Vector of W holds
FunctionalSAF(NulForm(V,W),w) = 0Functional(V)
proof
let V, W be non empty ModuleStr over INT.Ring, y be Vector of W;
set N = NulForm(V,W);
now
let v be Vector of V;
thus FunctionalSAF(N,y).v = N.(v,y) by BLTh9
.= 0.INT.Ring by FUNCOP_1:70
.= (0Functional(V)).v;
end;
hence thesis by FUNCT_2:63;
end;
theorem BLTh12:
for V, W being non empty ModuleStr over INT.Ring, f, g being Form of V,W,
w being Vector of W holds
FunctionalSAF(f+g,w) = FunctionalSAF(f,w) + FunctionalSAF(g,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f,g be Form of V,W,
w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(f+g,w)).v = (f+g).(v,w) by BLTh9
.= f.(v,w) + g.(v,w) by BLDef2
.= (FunctionalSAF(f,w)).v + g.(v,w) by BLTh9
.= (FunctionalSAF(f,w)).v + (FunctionalSAF(g,w)).v by BLTh9
.= (FunctionalSAF(f,w) +FunctionalSAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem BLTh13:
for V, W being non empty ModuleStr over INT.Ring, f,g being Form of V,W,
v being Vector of V holds
FunctionalFAF(f+g,v) = FunctionalFAF(f,v) + FunctionalFAF(g,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f,g be Form of V,W,
w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(f+g,w)).v = (f+g).(w,v) by BLTh8
.= f.(w,v) + g.(w,v) by BLDef2
.= (FunctionalFAF(f,w)).v + g.(w,v) by BLTh8
.= (FunctionalFAF(f,w)).v + (FunctionalFAF(g,w)).v by BLTh8
.= (FunctionalFAF(f,w) + FunctionalFAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem BLTh14:
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W,
a being Element of INT.Ring, w be Vector of W
holds FunctionalSAF(a*f,w) = a*FunctionalSAF(f,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V,W,
a be Element of INT.Ring,
w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(a*f,w)).v = (a*f).(v,w) by BLTh9
.= a*f.(v,w) by BLDef3
.= a*(FunctionalSAF(f,w)).v by BLTh9
.= (a*(FunctionalSAF(f,w))).v by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem BLTh15:
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W,
a being Element of INT.Ring, v being Vector of V holds
FunctionalFAF(a*f,v) = a*FunctionalFAF(f,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V,W,
a be Element of INT.Ring,
w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(a*f,w)).v = (a*f).(w,v) by BLTh8
.= a*f.(w,v) by BLDef3
.= a*(FunctionalFAF(f,w)).v by BLTh8
.= (a* FunctionalFAF(f,w)).v by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W,
w being Vector of W
holds FunctionalSAF(-f,w) = -FunctionalSAF(f,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V,W,
w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(-f,w)).v = (-f).(v,w) by BLTh9
.= -f.(v,w) by BLDef4
.= -(FunctionalSAF(f,w)).v by BLTh9
.= (- FunctionalSAF(f,w)).v by HAHNBAN1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being Form of V,W,
v being Vector of V
holds FunctionalFAF(-f,v) = -FunctionalFAF(f,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f be Form of V,W,
w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(-f,w)).v = (-f).(w,v) by BLTh8
.= -f.(w,v) by BLDef4
.= -(FunctionalFAF(f,w)).v by BLTh8
.= (- FunctionalFAF(f,w)).v by HAHNBAN1:def 4;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f, g being Form of V,W,
w being Vector of W
holds FunctionalSAF(f-g,w) = FunctionalSAF(f,w) - FunctionalSAF(g,w)
proof
let V, W be non empty ModuleStr over INT.Ring, f,g be Form of V,W,
w be Vector of W;
now
let v be Vector of V;
thus (FunctionalSAF(f-g,w)).v = (f-g).(v,w) by BLTh9
.= f.(v,w) - g.(v,w) by BLDef7
.= (FunctionalSAF(f,w)).v - g.(v,w) by BLTh9
.= (FunctionalSAF(f,w)).v - (FunctionalSAF(g,w)).v by BLTh9
.= (FunctionalSAF(f,w)).v + (-FunctionalSAF(g,w)).v by HAHNBAN1:def 4
.= (FunctionalSAF(f,w) -FunctionalSAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f,g being Form of V,W,
v being Vector of V
holds FunctionalFAF(f-g,v) = FunctionalFAF(f,v) - FunctionalFAF(g,v)
proof
let V, W be non empty ModuleStr over INT.Ring, f,g be Form of V,W,
w be Vector of V;
now
let v be Vector of W;
thus (FunctionalFAF(f-g,w)).v = (f-g).(w,v) by BLTh8
.= f.(w,v) - g.(w,v) by BLDef7
.= (FunctionalFAF(f,w)).v - g.(w,v) by BLTh8
.= (FunctionalFAF(f,w)).v - (FunctionalFAF(g,w)).v by BLTh8
.= (FunctionalFAF(f,w)).v + (-FunctionalFAF(g,w)).v by HAHNBAN1:def 4
.= (FunctionalFAF(f,w) -FunctionalFAF(g,w)).v by HAHNBAN1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
:: Two Form generated by Functionals
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Functional of V;
let g be Functional of W;
func FormFunctional(f,g) -> Form of V,W means
:BLDef10:
for v being Vector of V, w being Vector of W holds it.(v,w)= f.v * g.w;
existence
proof
deffunc F(Vector of V, Vector of W) = (f.$1) * (g.$2);
set c1 = the carrier of V, c2 = the carrier of W;
consider i be Function of [:c1,c2:],the carrier of INT.Ring such that
A1: for x being Element of c1 for y being Element of c2 holds
i.(x,y) = F(x,y) from BINOP_1:sch 4;
reconsider i as Form of V,W;
take i;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be Form of V,W such that
A2: for v being Vector of V, y being Vector of W holds
F1.(v,y)= f.v * g.y and
A3: for v being Vector of V, y being Vector of W holds F2.(v,y)= f.v * g.y;
now
let v be Vector of V, y be Vector of W;
thus F1.(v,y) = f.v * g.y by A2
.= F2.(v,y) by A3;
end;
hence thesis;
end;
end;
theorem BLTh20:
for V, W being non empty ModuleStr over INT.Ring, f being Functional of V,
v being Vector of V, w being Vector of W holds
FormFunctional(f,0Functional(W)).(v,w) = 0
proof
let V, W be non empty ModuleStr over INT.Ring;
let f be Functional of V, v be Vector of V, y be Vector of W;
set 0F = 0Functional(W), F = FormFunctional(f,0F);
thus F.(v,y) = f.v * 0F.y by BLDef10
.= f.v * 0
.= 0;
end;
theorem BLTh21:
for V, W being non empty ModuleStr over INT.Ring, g being Functional of W,
v being Vector of V, w be Vector of W holds
FormFunctional(0Functional(V),g).(v,w) = 0
proof
let V, W be non empty ModuleStr over INT.Ring;
let h be Functional of W, v be Vector of V, y be Vector of W;
set 0F = 0Functional(V), F = FormFunctional(0F,h);
thus F.(v,y) = 0F.v * h.y by BLDef10
.= 0 * h.y
.= 0;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, f being Functional of V
holds
FormFunctional(f,0Functional(W)) = NulForm(V,W)
proof
let V, W be non empty ModuleStr over INT.Ring, f be Functional of V;
now
let v be Vector of V, y be Vector of W;
thus FormFunctional(f,0Functional(W)).(v,y) = 0 by BLTh20
.= NulForm(V,W).(v,y) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem
for V, W being non empty ModuleStr over INT.Ring, g being Functional of W
holds
FormFunctional(0Functional(V),g) = NulForm(V,W)
proof
let V, W be non empty ModuleStr over INT.Ring, h be Functional of W;
now
let v be Vector of V, y be Vector of W;
thus FormFunctional(0Functional(V),h).(v,y) = 0 by BLTh21
.= NulForm(V,W).(v,y) by FUNCOP_1:70;
end;
hence thesis;
end;
theorem BLTh24:
for V, W being non empty ModuleStr over INT.Ring,
f being Functional of V,
g being Functional of W, v being Vector of V
holds FunctionalFAF(FormFunctional(f,g),v) = f.v * g
proof
let V, W be non empty ModuleStr over INT.Ring;
let f be Functional of V,
h be Functional of W, v be Vector of V;
set F = FormFunctional(f,h), FF = FunctionalFAF(F,v);
now
let y be Vector of W;
thus FF.y = F.(v,y) by BLTh8
.= f.v * h.y by BLDef10
.= (f.v * h).y by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
theorem BLTh25:
for V, W being non empty ModuleStr over INT.Ring, f being Functional of V,
g being Functional of W, w being Vector of W
holds FunctionalSAF(FormFunctional(f,g),w) = g.w * f
proof
let V, W be non empty ModuleStr over INT.Ring;
let f be Functional of V, h be Functional of W, y be Vector of W;
set F = FormFunctional(f,h), FF = FunctionalSAF(F,y);
now
let v be Vector of V;
thus FF.v = F.(v,y) by BLTh9
.= f.v * h.y by BLDef10
.= (h.y * f).v by HAHNBAN1:def 6;
end;
hence thesis by FUNCT_2:63;
end;
:: Bilinear Forms and Their Properties
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W;
attr f is additiveFAF means
:BLDef11:
for v being Vector of V holds FunctionalFAF (f,v) is additive;
attr f is additiveSAF means
:BLDef12:
for w being Vector of W holds FunctionalSAF (f,w) is additive;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
let f be Form of V,W;
attr f is homogeneousFAF means
:BLDef13:
for v being Vector of V holds FunctionalFAF(f,v) is homogeneous;
attr f is homogeneousSAF means
:BLDef14:
for w being Vector of W holds FunctionalSAF(f,w) is homogeneous;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
cluster NulForm(V,W) -> additiveFAF;
coherence
proof
let v be Vector of V;
FunctionalFAF(NulForm(V,W),v)= 0Functional(W) by BLTh10;
hence thesis;
end;
cluster NulForm(V,W) -> additiveSAF;
coherence
proof
let y be Vector of W;
FunctionalSAF(NulForm(V,W),y)= 0Functional(V) by BLTh11;
hence thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
cluster NulForm(V,W) -> homogeneousFAF;
coherence
proof
let v be Vector of V;
FunctionalFAF(NulForm(V,W),v)= 0Functional(W) by BLTh10;
hence thesis;
end;
cluster NulForm(V,W) -> homogeneousSAF;
coherence
proof
let y be Vector of W;
FunctionalSAF(NulForm(V,W),y)= 0Functional(V) by BLTh11;
hence thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF
for Form of V,W;
existence
proof
take NulForm(V,W);
thus thesis;
end;
end;
definition
let V, W be non empty ModuleStr over INT.Ring;
mode bilinear-Form of V,W is additiveSAF homogeneousSAF additiveFAF
homogeneousFAF Form of V,W;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveFAF Form of V,W, v be Vector of V;
cluster FunctionalFAF(f,v) -> additive;
coherence by BLDef11;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveSAF Form of V,W, w be Vector of W;
cluster FunctionalSAF(f,w) -> additive;
coherence by BLDef12;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousFAF Form of V,W, v be Vector of V;
cluster FunctionalFAF(f,v) -> homogeneous;
coherence by BLDef13;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousSAF Form of V,W, w be Vector of W;
cluster FunctionalSAF(f,w) -> homogeneous;
coherence by BLDef14;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be Functional of V, g be additive Functional of W;
cluster FormFunctional(f,g) -> additiveFAF;
coherence
proof
let v be Vector of V;
set fg = FormFunctional(f,g), F = FunctionalFAF(fg,v);
let y,y9 be Vector of W;
A1: F = f.v * g by BLTh24;
hence F.(y+y9) = f.v * g.(y+y9) by HAHNBAN1:def 6
.= f.v *(g.y +g.y9) by VECTSP_1:def 20
.= f.v * g.y + f.v * g.y9
.= f.v * g.y + F.y9 by A1,HAHNBAN1:def 6
.= F.y + F.y9 by A1,HAHNBAN1:def 6;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additive Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> additiveSAF;
coherence
proof
let y be Vector of W;
set fg = FormFunctional(f,g), F = FunctionalSAF(fg,y);
F = g.y * f by BLTh25;
hence thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be Functional of V, g be homogeneous Functional of W;
cluster FormFunctional(f,g) -> homogeneousFAF;
coherence
proof
let v be Vector of V;
set fg = FormFunctional(f,g), F = FunctionalFAF(fg,v);
let y be Vector of W,r be Element of INT.Ring;
A1: F = f.v * g by BLTh24;
hence F.(r* y) = f.v * g.(r*y) by HAHNBAN1:def 6
.= f.v *(r*g.y) by HAHNBAN1:def 8
.= r*(f.v * g.y)
.= r * F.y by A1,HAHNBAN1:def 6;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneous Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> homogeneousSAF;
coherence
proof
let y be Vector of W;
set fg = FormFunctional(f,g);
set F = FunctionalSAF(fg,y);
let v be Vector of V, r be Element of INT.Ring;
A1: F = g.y * f by BLTh25;
hence F.(r* v) = g.y * f.(r*v) by HAHNBAN1:def 6
.= g.y *(r*f.v) by HAHNBAN1:def 8
.= r*(g.y * f.v)
.= r * F.v by A1,HAHNBAN1:def 6;
end;
end;
registration
let V be non trivial ModuleStr over INT.Ring, W be Z_Module;
let f be Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> non trivial;
coherence
proof
set fg = FormFunctional(f,g);
set w = the Vector of W;
consider v be Vector of V such that
A1: v <> 0.V by STRUCT_0:def 18;
A2: [0.V,0.W] <> [v,w] by A1,XTUPLE_0:1;
dom fg = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then
A3: [[0.V,0.W],fg.(0.V,0.W)] in fg & [[v,w],fg.(v,w)] in fg by FUNCT_1:1;
assume
A4: fg is trivial;
per cases by A4,ZFMISC_1:131;
suppose
fg = {};
hence contradiction;
end;
suppose
ex x being object st fg = {x};
then consider x be object such that
A5: fg = {x};
[[0.V,0.W],fg.(0.V,0.W)] = x & x=[[v,w],fg.(v,w)] by A3,A5,TARSKI:def 1;
hence contradiction by A2,XTUPLE_0:1;
end;
end;
end;
registration
let V be non empty ModuleStr over INT.Ring, W be non trivial Z_Module;
let f be Functional of V, g be Functional of W;
cluster FormFunctional(f,g) -> non trivial;
coherence
proof
set fg = FormFunctional(f,g);
set v = the Vector of V;
consider w be Vector of W such that
A1: w <> 0.W by STRUCT_0:def 18;
A2: [0.V,0.W] <> [v,w] by A1,XTUPLE_0:1;
dom fg = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then
A3: [[0.V,0.W],fg.(0.V,0.W)] in fg & [[v,w],fg.(v,w)] in fg by FUNCT_1:1;
assume
A4: fg is trivial;
per cases by A4,ZFMISC_1:131;
suppose
fg = {};
hence contradiction;
end;
suppose
ex x being object st fg = {x};
then consider x be object such that
A5: fg={x};
[[0.V,0.W],fg.(0.V,0.W)] = x & x=[[v,w],fg.(v,w)] by A3,A5,TARSKI:def 1;
hence contradiction by A2,XTUPLE_0:1;
end;
end;
end;
registration
let V, W be non trivial free Z_Module;
let f be non constant 0-preserving Functional of V, g be non constant
0-preserving Functional of W;
cluster FormFunctional(f,g) -> non constant;
coherence
proof
set fg = FormFunctional(f,g);
consider v be Vector of V such that
v <> 0.V and
A1: f.v <> 0 by VS10Th28;
consider w be Vector of W such that
w <> 0.W and
A2: g.w <> 0 by VS10Th28;
fg.(v,w) = f.v * g.w by BLDef10;
then
A3: dom fg = [:the carrier of V, the carrier of W:] & fg.(v,w) <> 0
by A1,A2,FUNCT_2:def 1;
fg.(0.V,0.W) = f.(0.V)*g.(0.W) by BLDef10
.= (0.INT.Ring) * g.(0.W) by HAHNBAN1:def 9
.= 0.INT.Ring;
hence thesis by A3,BINOP_1:19;
end;
end;
registration
let V, W be non trivial free Z_Module;
cluster non trivial non constant additiveFAF homogeneousFAF additiveSAF
homogeneousSAF for Form of V,W;
existence
proof
set f = the non constant non trivial linear-Functional of V,
g = the non constant non trivial linear-Functional of W;
take FormFunctional(f,g);
thus thesis;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f,g be additiveSAF Form of V,W;
cluster f+g -> additiveSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(f+g,w), Ff = FunctionalSAF(f,w);
set Fg = FunctionalSAF(g,w);
let v, y be Vector of V;
A1: Ff is additive;
A2: Fg is additive;
thus Ffg.(v+y) = (Ff+Fg).(v+y) by BLTh12
.= Ff.(v+y) + Fg.(v+y) by HAHNBAN1:def 3
.= Ff.v+Ff.y + Fg.(v+y) by A1
.= Ff.v+Ff.y + (Fg.v+Fg.y) by A2
.= Ff.v+Fg.v + Ff.y+Fg.y
.= (Ff+Fg).v + Ff.y+Fg.y by HAHNBAN1:def 3
.= (Ff+Fg).v + (Ff.y+Fg.y)
.= (Ff+Fg).v + (Ff+Fg).y by HAHNBAN1:def 3
.= Ffg.v + (Ff+Fg).y by BLTh12
.= Ffg.v + Ffg.y by BLTh12;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be additiveFAF Form of V,W;
cluster f+g -> additiveFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(f+g,w), Ff = FunctionalFAF(f,w);
set Fg = FunctionalFAF(g,w);
let v,y be Vector of W;
A1: Ff is additive;
A2: Fg is additive;
thus Ffg.(v+y) = (Ff+Fg).(v+y) by BLTh13
.= Ff.(v+y) + Fg.(v+y) by HAHNBAN1:def 3
.= Ff.v+Ff.y + Fg.(v+y) by A1
.= Ff.v+Ff.y + (Fg.v+Fg.y) by A2
.= Ff.v+Fg.v + Ff.y+Fg.y
.= (Ff+Fg).v + Ff.y+Fg.y by HAHNBAN1:def 3
.= (Ff+Fg).v + (Ff.y+Fg.y)
.= (Ff+Fg).v + (Ff+Fg).y by HAHNBAN1:def 3
.= Ffg.v + (Ff+Fg).y by BLTh13
.= Ffg.v + Ffg.y by BLTh13;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveSAF Form of V,W;
let a be Element of INT.Ring;
cluster a*f -> additiveSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(a*f,w), Ff = FunctionalSAF(f,w);
let v,y be Vector of V;
A1: Ff is additive;
thus Ffg.(v+y) = (a*Ff).(v+y) by BLTh14
.= a*Ff.(v+y) by HAHNBAN1:def 6
.= a*(Ff.v + Ff.y) by A1
.= a* Ff.v + a*Ff.y
.= (a*Ff).v +a* Ff.y by HAHNBAN1:def 6
.= (a*Ff).v + (a*Ff).y by HAHNBAN1:def 6
.= Ffg.v + (a*Ff).y by BLTh14
.= Ffg.v + Ffg.y by BLTh14;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveFAF Form of V,W;
let a be Element of INT.Ring;
cluster a*f -> additiveFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(a*f,w), Ff = FunctionalFAF(f,w);
let v,y be Vector of W;
A1: Ff is additive;
thus Ffg.(v+y) = (a*Ff).(v+y) by BLTh15
.= a*Ff.(v+y) by HAHNBAN1:def 6
.= a*(Ff.v + Ff.y) by A1
.= a* Ff.v +a* Ff.y
.= (a*Ff).v +a* Ff.y by HAHNBAN1:def 6
.= (a*Ff).v + (a*Ff).y by HAHNBAN1:def 6
.= Ffg.v + (a*Ff).y by BLTh15
.= Ffg.v + Ffg.y by BLTh15;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveSAF Form of V,W;
cluster -f -> additiveSAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be additiveFAF Form of V,W;
cluster -f -> additiveFAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be additiveSAF Form of V,W;
cluster f-g -> additiveSAF;
correctness;
end;
registration
let V,W be non empty ModuleStr over INT.Ring;
let f, g be additiveFAF Form of V,W;
cluster f-g -> additiveFAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be homogeneousSAF Form of V,W;
cluster f+g -> homogeneousSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(f+g,w), Ff = FunctionalSAF(f,w);
set Fg = FunctionalSAF(g,w);
let v be Vector of V, a be Element of INT.Ring;
thus Ffg.(a*v) = (Ff+Fg).(a*v) by BLTh12
.= Ff.(a*v) + Fg.(a*v) by HAHNBAN1:def 3
.= a*Ff.v + Fg.(a*v) by HAHNBAN1:def 8
.= a*Ff.v + a*Fg.v by HAHNBAN1:def 8
.= a*(Ff.v + Fg.v)
.= a*(Ff + Fg).v by HAHNBAN1:def 3
.= a* Ffg.v by BLTh12;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f, g be homogeneousFAF Form of V,W;
cluster f+g -> homogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(f+g,w), Ff = FunctionalFAF(f,w);
set Fg = FunctionalFAF(g,w);
let v be Vector of W, a be Element of INT.Ring;
thus Ffg.(a*v) = (Ff+Fg).(a*v) by BLTh13
.= Ff.(a*v) + Fg.(a*v) by HAHNBAN1:def 3
.= a*Ff.v + Fg.(a*v) by HAHNBAN1:def 8
.= a*Ff.v + a*Fg.v by HAHNBAN1:def 8
.= a*(Ff.v + Fg.v)
.= a*(Ff + Fg).v by HAHNBAN1:def 3
.= a* Ffg.v by BLTh13;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousSAF Form of V,W;
let a be Element of INT.Ring;
cluster a*f -> homogeneousSAF;
correctness
proof
let w be Vector of W;
set Ffg = FunctionalSAF(a*f,w), Ff = FunctionalSAF(f,w);
let v be Vector of V, b be Element of INT.Ring;
thus Ffg.(b*v) = (a*Ff).(b*v) by BLTh14
.= a*Ff.(b*v) by HAHNBAN1:def 6
.= a*(b*Ff.v) by HAHNBAN1:def 8
.= b*(a*Ff.v)
.= b*(a*Ff).v by HAHNBAN1:def 6
.= b* Ffg.v by BLTh14;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousFAF Form of V,W;
let a be Element of INT.Ring;
cluster a*f -> homogeneousFAF;
correctness
proof
let w be Vector of V;
set Ffg = FunctionalFAF(a*f,w), Ff = FunctionalFAF(f,w);
let v be Vector of W, b be Element of INT.Ring;
thus Ffg.(b*v) = (a*Ff).(b*v) by BLTh15
.= a*Ff.(b*v) by HAHNBAN1:def 6
.= a*(b*Ff.v) by HAHNBAN1:def 8
.= b*(a*Ff.v)
.= b*(a*Ff).v by HAHNBAN1:def 6
.= b* Ffg.v by BLTh15;
end;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousSAF Form of V,W;
cluster -f -> homogeneousSAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f be homogeneousFAF Form of V,W;
cluster -f -> homogeneousFAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f,g be homogeneousSAF Form of V,W;
cluster f-g -> homogeneousSAF;
correctness;
end;
registration
let V, W be non empty ModuleStr over INT.Ring;
let f,g be homogeneousFAF Form of V,W;
cluster f-g -> homogeneousFAF;
correctness;
end;
theorem BLTh26:
for V, W being non empty ModuleStr over INT.Ring, v, u being Vector of V,
w being Vector of W, f being Form of V,W st f is additiveSAF
holds f.(v+u,w) = f.(v,w) + f.(u,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v, w be Vector of V, y be Vector of W, f be Form of V,W;
set F = FunctionalSAF(f,y);
assume f is additiveSAF;
then
A1: F is additive;
thus f.(v+w,y) = F.(v+w) by BLTh9
.= F.v+F.w by A1
.= f.(v,y) + F.w by BLTh9
.= f.(v,y) + f.(w,y) by BLTh9;
end;
theorem BLTh27:
for V, W being non empty ModuleStr over INT.Ring, v being Vector of V,
u, w being Vector of W, f being Form of V,W st f is additiveFAF
holds f.(v,u+w) = f.(v,u) + f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v be Vector of V, y, z be Vector of W, f be Form of V,W;
set F = FunctionalFAF(f,v);
assume f is additiveFAF; then
A1: F is additive;
thus f.(v,y+z) = F.(y+z) by BLTh8
.= F.y+F.z by A1
.= f.(v,y) + F.z by BLTh8
.= f.(v,y) + f.(v,z) by BLTh8;
end;
theorem BLTh28:
for V, W being non empty ModuleStr over INT.Ring, v, u being Vector of V,
w, t being Vector of W, f being additiveSAF additiveFAF Form of V,W
holds f.(v+u,w+t) = f.(v,w) + f.(v,t) + (f.(u,w) + f.(u,t))
proof
let V, W be non empty ModuleStr over INT.Ring;
let v, w be Vector of V, y, z be Vector of W, f be additiveSAF additiveFAF
Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v+w,y+z) = f.(v,y+z) + f.(w,y+z) by BLTh26
.= (v1 + v3) + f.(w,y+z) by BLTh27
.= v1 +v3 + (v4 + v5) by BLTh27;
end;
theorem BLTh29:
for V, W being right_zeroed non empty ModuleStr over INT.Ring,
f being additiveFAF Form of V,W,
v being Vector of V holds f.(v,0.W) = 0
proof
let V, W be right_zeroed non empty ModuleStr over INT.Ring;
let f be additiveFAF Form of V,W, v be Vector of V;
f.(v,0.W) = f.(v,0.W+0.W) by RLVECT_1:def 4
.= f.(v,0.W) + f.(v,0.W) by BLTh27;
hence thesis;
end;
theorem BLTh30:
for V, W being right_zeroed non empty ModuleStr over INT.Ring,
f being additiveSAF Form of V,W,
w being Vector of W holds f.(0.V,w) = 0
proof
let V, W be right_zeroed non empty ModuleStr over INT.Ring;
let f be additiveSAF Form of V,W, v be Vector of W;
f.(0.V,v) = f.(0.V+0.V,v) by RLVECT_1:def 4
.= f.(0.V,v) + f.(0.V,v) by BLTh26;
hence thesis;
end;
theorem BLTh31:
for V, W being non empty ModuleStr over INT.Ring, v being Vector of V,
w being Vector of W, a being Element of INT.Ring, f being Form of V,W
st f is homogeneousSAF
holds f.(a*v,w) = a*f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v be Vector of V, y be Vector of W, r be Element of INT.Ring,
f be Form of V,W;
set F = FunctionalSAF(f,y);
assume f is homogeneousSAF;
then
A1: F is homogeneous;
thus f.(r*v,y) = F.(r*v) by BLTh9
.= r*F.v by A1
.= r*f.(v,y) by BLTh9;
end;
theorem BLTh32:
for V, W being non empty ModuleStr over INT.Ring, v being Vector of V,
w being Vector of W, a being Element of INT.Ring, f being Form of V,W
st f is homogeneousFAF
holds f.(v,a*w) = a*f.(v,w)
proof
let V, W be non empty ModuleStr over INT.Ring;
let v be Vector of V, y be Vector of W, r be Element of INT.Ring,
f be Form of V,W;
set F = FunctionalFAF(f,v);
assume f is homogeneousFAF;
then
A1: F is homogeneous;
thus f.(v,r*y) = F.(r*y) by BLTh8
.= r*F.y by A1
.= r*f.(v,y) by BLTh8;
end;
theorem
for V, W being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, f being homogeneousSAF Form of V,W,
w being Vector of W holds f.(0.V,w) = 0.INT.Ring
proof
let V, W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring;
let f be homogeneousSAF Form of V,W, v be Vector of W;
(0.INT.Ring)*(0.V) = 0.V by VS10Th1;
hence f.(0.V,v) = (0.INT.Ring) * f.(0.V,v) by BLTh31
.= 0.INT.Ring;
end;
theorem
for V, W being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, f being homogeneousFAF Form of V,W,
v being Vector of V holds f.(v,0.W) = 0.INT.Ring
proof
let V, W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring;
let f be homogeneousFAF Form of V,W, v be Vector of V;
(0.INT.Ring)*(0.W) = 0.W by VS10Th1;
hence f.(v,0.W) = (0.INT.Ring) * f.(v,0.W) by BLTh32
.= 0.INT.Ring;
end;
theorem BLTh35:
for V, W being Z_Module, v, u being Vector of V, w being Vector of W,
f being additiveSAF homogeneousSAF Form of V,W
holds f.(v-u,w) = f.(v,w) - f.(u,w)
proof
let V, W be Z_Module, v, w be Vector of V, y be Vector of W;
let f be additiveSAF homogeneousSAF Form of V,W;
thus f.(v-w,y) = f.(v,y) +f.(-w,y) by BLTh26
.= f.(v,y) +f.((-1.INT.Ring)* w,y) by ZMODUL01:2
.= f.(v,y) +(-1.INT.Ring)*f.(w,y) by BLTh31
.= f.(v,y) - f.( w,y);
end;
theorem BLTh36:
for V, W being Z_Module, v being Vector of V, w, t being Vector of W,
f being additiveFAF homogeneousFAF Form of V,W
holds f.(v,w-t) = f.(v,w) - f.(v,t)
proof
let V, W be Z_Module, v be Vector of V, y, z be Vector of W,
f be additiveFAF homogeneousFAF Form of V,W;
thus f.(v,y-z) = f.(v,y) + f.(v,-z) by BLTh27
.= f.(v,y) + f.(v,(-1.INT.Ring)* z) by ZMODUL01:2
.= f.(v,y) + (-1.INT.Ring)*f.(v,z) by BLTh32
.= f.(v,y) - f.(v,z);
end;
theorem BLTh37:
for V, W being Z_Module, v, u being Vector of V, w, t being Vector of W,
f being bilinear-Form of V,W
holds f.(v-u,w-t) = f.(v,w) - f.(v,t) -(f.(u,w) - f.(u,t))
proof
let V, W be Z_Module;
let v, w be Vector of V, y, z be Vector of W, f be bilinear-Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v-w,y-z) = f.(v,y-z) - f.(w,y-z) by BLTh35
.= v1 - v3 - f.(w,y-z) by BLTh36
.= v1 - v3 - (v4 - v5) by BLTh36;
end;
theorem
for V, W being add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, v, u being Vector of V,
w, t being Vector of W,
a, b being Element of INT.Ring, f being bilinear-Form of V,W
holds f.(v+a*u,w+b*t) = f.(v,w) + b*f.(v,t) + (a*f.(u,w) + a*(b*f.(u,t)))
proof
let V, W be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over INT.Ring, v, w be Vector of V,
y, z be Vector of W,
a, b be Element of INT.Ring;
let f be bilinear-Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v+a*w,y+b*z) = v1 +f.(v,b*z) + (f.(a*w,y) +f.(a*w,b*z)) by BLTh28
.= v1 +b*v3 + (f.(a*w,y) +f.(a*w,b*z)) by BLTh32
.= v1 + b*v3 + (a*v4 + f.(a*w,b*z)) by BLTh31
.= v1 + b*v3 + (a*v4 + a*f.(w,b*z)) by BLTh31
.= v1 + b*v3 + (a*v4 + a*(b*v5)) by BLTh32;
end;
theorem
for V, W being Z_Module, v, u being Vector of V, w, t being Vector of W,
a, b being Element of INT.Ring, f being bilinear-Form of V,W
holds f.(v-a*u,w-b*t) = f.(v,w) - b*f.(v,t) - (a*f.(u,w) - a*(b*f.(u,t)))
proof
let V, W be Z_Module, v, w be Vector of V, y, z be Vector of W,
a, b be Element of INT.Ring, f be bilinear-Form of V,W;
set v1 = f.(v,y), v3 = f.(v,z), v4 = f.(w,y), v5 = f.(w,z);
thus f.(v-a*w,y-b*z) = v1 -f.(v,b*z) - (f.(a*w,y) -f.(a*w,b*z)) by BLTh37
.= v1 -b*v3 - (f.(a*w,y) -f.(a*w,b*z)) by BLTh32
.= v1 - b*v3 - (a*v4 - f.(a*w,b*z)) by BLTh31
.= v1 - b*v3 - (a*v4 - a*f.(w,b*z)) by BLTh31
.= v1 - b*v3 - (a*v4 - a*(b*v5)) by BLTh32;
end;
theorem
for V, W being right_zeroed non empty ModuleStr over INT.Ring,
f being Form of V,W
st f is additiveFAF or f is additiveSAF
holds f is constant iff
for v be Vector of V, w be Vector of W holds f.(v,w)=0
proof
let V, W be right_zeroed non empty ModuleStr over INT.Ring,
f be Form of V,W;
A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
assume
A2: f is additiveFAF or f is additiveSAF;
hereby
assume
A3: f is constant;
let v be Vector of V, w be Vector of W;
per cases by A2;
suppose
A4: f is additiveFAF;
thus f.(v,w) = f.(v,0.W) by A1,A3,BINOP_1:19
.= 0 by A4,BLTh29;
end;
suppose
A5: f is additiveSAF;
thus f.(v,w) = f.(0.V,w) by A1,A3,BINOP_1:19
.= 0 by A5,BLTh30;
end;
end;
hereby
assume
A6: for v being Vector of V, w being Vector of W holds f.(v,w) = 0;
now
let x, y be object such that
A7: x in dom f and
A8: y in dom f;
consider v be Vector of V, w be Vector of W such that
A9: x = [v,w] by A7,DOMAIN_1:1;
consider s be Vector of V, t be Vector of W such that
A10: y = [s,t] by A8,DOMAIN_1:1;
thus f.x = f.(v,w) by A9
.= 0 by A6
.=f.(s,t) by A6
.=f.y by A10;
end;
hence f is constant;
end;
end;
begin :: Matrix of bilinear-form
definition
let V1, V2 be finite-rank free Z_Module;
let b1 be OrdBasis of V1, b2 be OrdBasis of V2;
let f be bilinear-Form of V1,V2;
func BilinearM(f, b1, b2) -> Matrix of len b1, len b2, INT.Ring means
:defBilinearM:
for i, j being Nat st i in dom b1 & j in dom b2
holds it*(i,j) = f.(b1/.i, b2/.j);
existence
proof
deffunc F(Nat,Nat) = In(f.(b1/.$1, b2/.$2),the carrier of INT.Ring);
consider M being Matrix of len b1, len b2, INT.Ring such that
A20: for i, j st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MATRIX_0:sch 1;
take M;
thus for i, j being Nat st i in dom b1 & j in dom b2
holds M*(i,j) = f.(b1/.i, b2/.j)
proof
let i, j be Nat;
assume A21: i in dom b1 & j in dom b2;
len b1 <> 0
proof
assume len b1 = 0;
then Seg len b1 = {};
hence contradiction by A21,FINSEQ_1:def 3;
end;
then Indices M = [:Seg len b1, Seg len b2:] by MATRIX_0:23
.= [: dom b1, Seg len b2:] by FINSEQ_1:def 3
.= [: dom b1, dom b2:] by FINSEQ_1:def 3;
then [i, j] in Indices M by A21,ZFMISC_1:87; then
M*(i,j) = F(i,j) by A20;
hence M*(i,j) = f.(b1/.i, b2/.j);
end;
end;
uniqueness
proof
let M1, M2 be Matrix of len b1, len b2, INT.Ring;
assume that
A22: for i, j being Nat st i in dom b1 & j in dom b2
holds M1*(i,j) = f.(b1/.i, b2/.j) and
A23: for i, j being Nat st i in dom b1 & j in dom b2
holds M2*(i,j) = f.(b1/.i, b2/.j);
now
let i, j;
assume
A25: [i,j] in Indices M1;
then len b1 <> 0 by MATRIX_0:22;
then Indices M1 = [:Seg len b1, Seg len b2:] by MATRIX_0:23
.= [: dom b1, Seg len b2:] by FINSEQ_1:def 3
.= [: dom b1, dom b2:] by FINSEQ_1:def 3;
then
A26: i in dom b1 & j in dom b2 by A25,ZFMISC_1:87;
thus M1*(i,j) = f.(b1/.i, b2/.j) by A22,A26
.= M2*(i,j) by A26,A23;
end;
hence thesis by MATRIX_0:27;
end;
end;
theorem
for V being finite-rank free Z_Module,
i being Nat,
a1 being Element of INT.Ring,
a2 being Element of V,
p1 being FinSequence of INT.Ring,
p2 being FinSequence of V
st i in dom (lmlt (p1,p2)) & a1 = p1 . i & a2 = p2 . i holds
(lmlt (p1,p2)).i = a1 * a2 by FUNCOP_1:22;
theorem LMThMBF1X0:
for V being finite-rank free Z_Module,
F being linear-Functional of V,
y being FinSequence of V,
x being FinSequence of INT.Ring,
X, Y being FinSequence of INT.Ring
st X = x & len y = len x & len X = len Y &
(for k being Nat st k in Seg len x holds Y.k = F.(y/.k))
holds X "*" Y = F.(Sum lmlt (x,y))
proof
let V be finite-rank free Z_Module,
F be linear-Functional of V;
defpred P[FinSequence of V] means
for x being FinSequence of INT.Ring,
X, Y being FinSequence of INT.Ring
st X = x & len $1 = len x & len X = len Y &
(for k being Nat st k in Seg len x holds Y.k = F.($1/.k))
holds X "*" Y = F.(Sum lmlt (x,$1));
A2: for y being FinSequence of V
for w being Element of V st P[y] holds P[y^<*w*>]
proof
let y be FinSequence of V;
let w be Element of V such that
P1: for x being FinSequence of INT.Ring,
X, Y being FinSequence of INT.Ring
st X = x & len y = len x & len X = len Y &
(for k being Nat st k in Seg len x holds Y.k = F.(y/.k))
holds X "*" Y = F.(Sum lmlt (x,y));
thus for x being FinSequence of INT.Ring,
X, Y being FinSequence of INT.Ring
st X = x & len (y^<*w*>) = len x & len X = len Y &
(for k being Nat st k in Seg len x holds Y.k = F.((y^<*w*>)/.k))
holds X "*" Y = F.(Sum lmlt (x,y^<*w*>))
proof
let x be FinSequence of INT.Ring,
X, Y be FinSequence of INT.Ring;
assume that
R1: X = x and
R2: len (y^<*w*>) = len x and
R3: len X = len Y and
R4: for k being Nat st k in Seg len x holds Y.k = F.((y^<*w*>)/.k);
X1: F is additive;
X2: F is homogeneous;
set n = len y;
set X0 = X | n;
set Y0 = Y | n;
set x0 = x | n;
Q0: len (y^<*w*>) = len y + len <*w*> by FINSEQ_1:22
.= n + 1 by FINSEQ_1:39;
LN4: len x0 = n by Q0,R2,FINSEQ_1:59,NAT_1:11;
LN5: len X0 = n by Q0,R1,R2,FINSEQ_1:59,NAT_1:11;
LN6: len Y0 = n by Q0,R1,R2,R3,FINSEQ_1:59,NAT_1:11;
LN7: n+1 in Seg (n+1) by FINSEQ_1:4;
W1: X0 = X | Seg n by FINSEQ_1:def 16;
W2: Y0 = Y | Seg n by FINSEQ_1:def 16;
W3: x0 = x | Seg n by FINSEQ_1:def 16;
Q2: len y = len x0 by Q0,R2,FINSEQ_1:59,NAT_1:11;
Q3: len X0 = len Y0 by LN5,Q0,R1,R2,R3,FINSEQ_1:59,NAT_1:11;
for k being Nat st k in Seg len x0 holds Y0.k = F.(y/.k)
proof
let k be Nat;
assume Q31: k in Seg len x0;
then
Q34: k in dom y by LN4,FINSEQ_1:def 3;
Q32: Seg len x0 c= Seg len x by Q0,R2,LN4,FINSEQ_3:18;
then k in Seg len x by Q31;
then
Q33: k in dom (y^<*w*>) by R2,FINSEQ_1:def 3;
Q35: (y^<*w*>)/.k = (y^<*w*>).k by Q33,PARTFUN1:def 6
.= y.k by Q34,FINSEQ_1:def 7
.= y/.k by Q34,PARTFUN1:def 6;
thus Y0.k = Y.k by W2,LN4,Q31,FUNCT_1:49
.= F.(y/.k) by R4,Q31,Q32,Q35;
end; then
Q4: X0 "*" Y0 = F.(Sum lmlt (x0,y)) by R1,Q2,Q3,P1;
Q51: n+1 in dom X by LN7,Q0,R1,R2,FINSEQ_1:def 3;
Q61: n+1 in dom Y by LN7,Q0,R1,R2,R3,FINSEQ_1:def 3;
Q71: n+1 in dom x by LN7,Q0,R2,FINSEQ_1:def 3;
Q9: X/.(n+1) = X.(n+1) by Q51,PARTFUN1:def 6
.= x/.(n+1) by R1,Q71,PARTFUN1:def 6;
Q103: n+1 in dom (y^<*w*>) by LN7,Q0,FINSEQ_1:def 3;
Q102: (y^<*w*>)/.(n+1) = (y^<*w*>).(n+1) by Q103,PARTFUN1:def 6
.= w by FINSEQ_1:42;
Y/.(n+1) = Y.(n+1) by Q61,PARTFUN1:def 6
.= F.w by Q0,Q102,R2,R4,FINSEQ_1:4; then
Q11: X/.(n+1)* Y/.(n+1) = x/.(n+1) * F.w by Q9
.= F.((x/.(n+1))*w) by X2;
len mlt (X,Y) = n+1 by Q0,R1,R2,R3,MATRIX_3:6;
then
Q85: dom (mlt (X,Y)) = Seg (n+1) by FINSEQ_1:def 3;
Q82: len mlt (X0,Y0) = n by LN5,LN6,MATRIX_3:6;
Q88: len ((mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *> )
= len (mlt (X0,Y0)) + len ( <* X/.(n+1)* Y/.(n+1) *> ) by FINSEQ_1:22
.= n+1 by Q82,FINSEQ_1:39;
for k being Nat st k in dom (mlt (X,Y))
holds (mlt (X,Y)).k = ((mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *>).k
proof
let k be Nat;
assume V1: k in dom mlt (X,Y); then
V2: 1<=k & k <= n + 1 by Q85,FINSEQ_1:1;
set f=((mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *>);
AA: rng X0 c= the carrier of INT.Ring by RELAT_1:def 19;
AB: rng Y0 c= the carrier of INT.Ring by RELAT_1:def 19;
per cases;
suppose k <= n; then
V3: k in Seg n by V2,FINSEQ_1:1; then
V4: k in dom (mlt (X0,Y0)) by Q82,FINSEQ_1:def 3;
V5: k in dom X0 by LN5,V3,FINSEQ_1:def 3;
V6: k in dom Y0 by LN6,V3,FINSEQ_1:def 3;
X0.k in rng X0 by V5,FUNCT_1:3;
then reconsider X0k = X0.k as Element of INT.Ring by AA;
Y0.k in rng Y0 by V6,FUNCT_1:3;
then reconsider Y0k = Y0.k as Element of INT.Ring by AB;
k in dom X by V1,Q0,Q85,R1,R2,FINSEQ_1:def 3;
then X.k in rng X by FUNCT_1:3;
then reconsider Xk = X.k as Element of INT.Ring;
k in dom Y by V1,Q0,Q85,R1,R2,R3,FINSEQ_1:def 3;
then Y.k in rng Y by FUNCT_1:3;
then reconsider Yk = Y.k as Element of INT.Ring;
f.k = (mlt (X0,Y0)).k by V4,FINSEQ_1:def 7
.= X0k*Y0k by V4,FVSUM_1:60
.= (X.k)*(Y0.k) by W1,V5,FUNCT_1:47
.= Xk*Yk by W2,V6,FUNCT_1:47
.= (mlt (X,Y)).k by V1,FVSUM_1:60;
hence thesis;
end;
suppose not k <= n;
then n+1 <= k by NAT_1:13;
then V8: k=n+1 by V2,XXREAL_0:1;
Seg 1 = dom (<* X/.(n+1)* Y/.(n+1) *>) by FINSEQ_1:38;
then
V10: 1 in dom (<* X/.(n+1)* Y/.(n+1) *>) by FINSEQ_1:3;
Q9: X/.(n+1) = X.(n+1) by Q51,PARTFUN1:def 6;
then reconsider Xn = X.(n+1) as Element of INT.Ring;
Q10: Y/.(n+1) = Y.(n+1) by Q61,PARTFUN1:def 6;
then reconsider Yn = Y.(n+1) as Element of INT.Ring;
f.k = (<* X/.(n+1)* Y/.(n+1) *>).1
by Q82,V8,V10,FINSEQ_1:def 7
.= X/.(n+1)* Y/.(n+1)
.= (mlt (X,Y)).k by Q9,Q10,V1,V8,FVSUM_1:60;
hence thesis;
end;
end;
then
Q8: mlt (X,Y) =(mlt (X0,Y0)) ^<* X/.(n+1)* Y/.(n+1) *>
by Q85,Q88,FINSEQ_1:def 3;
QX121: dom x = Seg (n+1) by Q0,R2,FINSEQ_1:def 3
.= dom (y^<*w*>) by Q0,FINSEQ_1:def 3;
then
Q121: dom (lmlt (x,y^<*w*>)) = dom x by Th12;
dom x0 = Seg n by LN4,FINSEQ_1:def 3
.= dom y by FINSEQ_1:def 3;
then
dom (lmlt (x0,y)) = dom x0 by Th12;
then
Q124: dom (lmlt (x0,y)) = Seg n by LN4,FINSEQ_1:def 3;
then
Q125: len lmlt (x0,y) = n by FINSEQ_1:def 3;
len ((lmlt (x0,y)) ^ <* (x/.(n+1))*w *> )
= len (lmlt (x0,y)) + len ( <* (x/.(n+1))*w *> ) by FINSEQ_1:22
.= n+1 by Q125,FINSEQ_1:39;
then
Q126: dom ((lmlt (x0,y)) ^ <* (x/.(n+1))*w *> )
= Seg (n+1) by FINSEQ_1:def 3;
for k being Nat st k in dom (lmlt (x,y^<*w*>))
holds (lmlt (x,y^<*w*> )).k
= ((lmlt (x0,y)) ^ <* (x/.(n+1))*w *> ).k
proof
let k be Nat;
assume V1: k in dom (lmlt (x,y^<*w*>));
then
V0: k in Seg (n+1) by Q121,Q0,R2,FINSEQ_1:def 3;
then
V2: 1<=k & k <= n + 1 by FINSEQ_1:1;
set f = (lmlt (x0,y)) ^<* (x/.(n+1))*w *>;
per cases;
suppose VX3: k <= n; then
V3: k in Seg n by V2,FINSEQ_1:1;
V5: k in dom x0 by V3,LN4,FINSEQ_1:def 3;
V6: k in dom y by V3,FINSEQ_1:def 3;
XX1: x0.k in rng x0 by V5,FUNCT_1:3;
rng x0 c= the carrier of INT.Ring by RELAT_1:def 19;
then reconsider x0k = x0.k as Element of INT.Ring by XX1;
y.k in rng y by V6,FUNCT_1:3;
then reconsider y0k = y.k as Element of V;
k in dom x by V1,QX121,Th12; then
XX2: x.k in rng x by FUNCT_1:3;
reconsider xk = x.k as Element of INT.Ring by XX2;
k in dom (y^<*w*>) by V0,Q0,FINSEQ_1:def 3;
then (y^<*w*>).k in rng (y^<*w*>) by FUNCT_1:3;
then reconsider yk = (y^<*w*>).k as Element of V;
W: y0k = (y^<*w*>).k by V6,FINSEQ_1:def 7 .= yk;
f.k = (lmlt (x0,y)).k by V3,Q124,FINSEQ_1:def 7
.= x0k*y0k by V2,VX3,Q124,FINSEQ_1:1,FUNCOP_1:22
.= (xk)*y0k by V5,W3,FUNCT_1:47
.= (lmlt (x,y^<*w*>)).k by W,V1,FUNCOP_1:22;
hence thesis;
end;
suppose not k <= n;
then n+1 <= k by NAT_1:13;
then
V8: k=n+1 by V2,XXREAL_0:1;
Seg 1 = dom (<* (x/.(n+1))*w *>) by FINSEQ_1:38;
then V10: 1 in dom (<* (x/.(n+1))*w *>) by FINSEQ_1:3;
Seg 1 = dom ( <*w*> ) by FINSEQ_1:38;
then
V11: 1 in dom ( <*w*> ) by FINSEQ_1:3;
Q9: x/.(n+1) = x.(n+1) by Q71,PARTFUN1:def 6;
then reconsider xn = x.(n+1) as Element of INT.Ring;
(y^<*w*>)/.(n+1) = (y^<*w*>).(n+1) by Q103,PARTFUN1:def 6;
then reconsider yn = (y^<*w*>).(n+1) as Element of V;
Q11: (y^<*w*>).(n+1) = (<*w*>).1 by V11,FINSEQ_1:def 7
.= w;
f.k = (<* (x/.(n+1))*w *>).1 by Q125,V8,V10,FINSEQ_1:def 7
.= xn*w by Q9
.= (lmlt (x,y^<*w*>)).k by Q11,V1,V8,FUNCOP_1:22;
hence thesis;
end;
end;
then
Q12: lmlt (x,y^<*w*>) = (lmlt (x0,y)) ^ <* (x/.(n+1))*w *>
by Q0,Q121,Q126,R2,FINSEQ_1:def 3;
thus X "*" Y = Sum (mlt (X0,Y0)) + X/.(n+1)* Y/.(n+1) by Q8,FVSUM_1:71
.= F.(Sum lmlt (x0,y) + (x/.(n+1))*w) by Q4,Q11,X1
.= F.(Sum lmlt (x,y^<*w*>)) by Q12,FVSUM_1:71;
end;
end;
A4: P[<*>(the carrier of V)]
proof
let x be FinSequence of INT.Ring,
X, Y be FinSequence of INT.Ring;
assume that
R1: X = x and
R2: len (<*>(the carrier of V)) = len x and
len X = len Y and
for k being Nat st k in Seg len x
holds Y.k = F.((<*>(the carrier of V))/.k);
set y = <*>(the carrier of V);
Q2: X = <*>(the carrier of INT.Ring) by R1,R2;
Q4: mlt (X,Y) = (the multF of INT.Ring) * <:X,Y:> by FUNCOP_1:def 3
.= <*>(the carrier of INT.Ring) by Q2;
Q5: lmlt (x,y) = (the lmult of V) * <:x,y:> by FUNCOP_1:def 3
.= <*>(the carrier of V);
reconsider I0 = 0 as Element of INT.Ring;
X1: F is additive;
X2: F.(0.V) = F.(0.V+0.V)
.= F.(0.V) + F.(0.V) by X1;
thus X "*" Y = 0.INT.Ring by Q4,RLVECT_1:43
.= F.(Sum lmlt (x,y)) by Q5,X2,RLVECT_1:43;
end;
for p being FinSequence of V holds P[p] from FINSEQ_2:sch 2(A4,A2);
hence thesis;
end;
theorem LMThMBF1X:
for V1, V2 being finite-rank free Z_Module,
b2 being OrdBasis of V2, b3 being OrdBasis of V2,
f being bilinear-Form of V1, V2,
v1 being Vector of V1,
v2 being Vector of V2,
X, Y being FinSequence of INT.Ring
st len X = len b2 & len Y = len b2 &
( for k being Nat st k in Seg len b2 holds Y.k = f.(v1, b2/.k)) &
X = (v2|-- b2)
holds Y "*" X = f.(v1, v2)
proof
let V1, V2 be finite-rank free Z_Module,
b2 be OrdBasis of V2, b3 be OrdBasis of V2,
f be bilinear-Form of V1, V2,
v1 be Vector of V1,
v2 be Vector of V2,
X, Y be FinSequence of INT.Ring;
assume that
A1: len X = len b2 and
A2: len Y = len b2 and
A3:( for k being Nat st k in Seg len b2 holds Y.k = f.(v1, b2/.k)) and
A4: X = (v2|-- b2);
set x = (v2|-- b2);
P2: for k being Nat st k in Seg len x
holds Y.k = (FunctionalFAF(f,v1)).(b2/.k)
proof
let k be Nat;
assume k in Seg len x;
then Y.k = f.(v1, b2/.k) by A1,A3,A4;
hence Y.k = (FunctionalFAF(f,v1)).(b2/.k) by BLTh8;
end;
thus Y "*" X = X "*" Y by FVSUM_1:90
.= (FunctionalFAF(f,v1)).(Sum lmlt(v2|--b2,b2)) by LMThMBF1X0,A1,A2,A4,P2
.= f.(v1, Sum lmlt(v2|--b2,b2)) by BLTh8
.= f.(v1, v2) by Th35;
end;
theorem LMThMBF1Y:
for V1, V2 being finite-rank free Z_Module,
b1 being OrdBasis of V1,
f being bilinear-Form of V1, V2,
v1 being Vector of V1,
v2 being Vector of V2,
X,Y being FinSequence of INT.Ring
st len X = len b1 & len Y = len b1 &
( for k being Nat st k in Seg len b1 holds Y.k = f.(b1/.k, v2) ) &
X = (v1 |-- b1)
holds X "*" Y = f.(v1, v2)
proof
let V1, V2 be finite-rank free Z_Module,
b1 be OrdBasis of V1,
f be bilinear-Form of V1, V2,
v1 be Vector of V1,
v2 be Vector of V2,
X,Y be FinSequence of INT.Ring;
assume that
A1: len X = len b1 and
A2: len Y = len b1 and
A3: for k being Nat st k in Seg len b1 holds Y.k = f.(b1/.k, v2) and
A4: X = v1|-- b1;
set x = v1|-- b1;
P2: for k being Nat st k in Seg len x
holds Y.k = (FunctionalSAF(f,v2)).(b1/.k)
proof
let k be Nat;
assume k in Seg len x;
then Y.k = f.(b1/.k,v2) by A1,A3,A4;
hence Y.k = (FunctionalSAF(f,v2)).(b1/.k) by BLTh9;
end;
thus X "*" Y = (FunctionalSAF(f,v2)).(Sum lmlt(v1|--b1,b1))
by LMThMBF1X0,A1,A2,A4,P2
.= f.(Sum lmlt(v1|--b1,b1),v2) by BLTh9
.= f.(v1, v2) by Th35;
end;
theorem ThMBF1:
for V1, V2 being finite-rank free Z_Module,
b1 being OrdBasis of V1, b2 being OrdBasis of V2, b3 being OrdBasis of V2,
f being bilinear-Form of V1, V2
st 0 < rank V1 holds
BilinearM(f, b1, b3) =
BilinearM(f, b1, b2) * (AutMt(id(V2), b3, b2)@)
proof
let V1, V2 be finite-rank free Z_Module,
b1 be OrdBasis of V1,
b2 be OrdBasis of V2,
b3 be OrdBasis of V2,
f be bilinear-Form of V1, V2;
assume AS: 0 < rank V1;
set n = len b2;
A2: len b2 = rank V2 by ThRank1;
A3: len b3 = rank V2 by ThRank1;
reconsider IM1 = AutMt(id(V2), b3, b2) as Matrix of n,INT.Ring
by LMThMBF3,A2;
reconsider M1 = IM1@ as Matrix of n,INT.Ring;
set M2 = BilinearM(f, b1, b2) * M1;
B1: len M1 = n & width M1 = n
& Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
F1: len IM1 = n & width IM1 = n
& Indices IM1 = [:Seg n, Seg n:] by MATRIX_0:24;
B2: 0 < len b1 by AS,ThRank1; then
B3: len BilinearM(f, b1, b2) = len b1
& width BilinearM(f, b1, b2) = len b2 by MATRIX_0:23;
C1: width BilinearM(f, b1, b2) = len M1 by B1,B2,MATRIX_0:23;
len M2 = len b1 & width M2 = n by B1,B3,MATRIX_3:def 4;
then reconsider M2 as Matrix of len b1,n,INT.Ring by B2,MATRIX_0:20;
set FM1 = M1;
set FBM = BilinearM(f, b1, b2);
for i, j being Nat st [i,j] in Indices BilinearM(f, b1, b3)
holds BilinearM(f, b1, b3)*(i,j) = M2*(i,j)
proof
let i, j be Nat;
assume [i,j] in Indices BilinearM(f, b1, b3); then
B6: [i,j] in [:Seg len b1,Seg len b3 :] by B2,MATRIX_0:23; then
B7: i in Seg len b1 & j in Seg len b3 by ZFMISC_1:87; then
B8:i in dom b1 & j in dom b3 by FINSEQ_1:def 3; then
B9: (BilinearM(f, b1, b3))*(i,j) = f.(b1/.i, b3/.j) by defBilinearM;
[i,j] in Indices M2 by B2,B6,A2,A3,MATRIX_0:23; then
B11: M2*(i,j) = Line(FBM,i) "*" Col(FM1,j) by C1,MATRIX_3:def 4;
B12: len Line(FBM,i) = len b2 by B3,MATRIX_0:def 7;
B13:
now
let k be Nat;
assume B131: k in Seg len b2; then
B132: k in Seg width FBM by B2,MATRIX_0:23;
B81: k in dom b2 by B131,FINSEQ_1:def 3;
thus Line(FBM,i).k = FBM*(i,k) by B132,MATRIX_0:def 7
.= f.(b1/.i, b2/.k) by B8,B81,defBilinearM;
end;
B14: len Col(FM1,j) = len b2 by B1,MATRIX_0:def 8;
B135: j in Seg n by B6,A2,A3,ZFMISC_1:87;
B15:
now
let k be Nat;
assume 1 <= k & k <= len Col(FM1,j); then
B131:k in Seg len b2 by B14,FINSEQ_1:1; then
B132: k in dom FM1 by B1,FINSEQ_1:def 3;
B132A: j in dom IM1 by B135,F1,FINSEQ_1:def 3;
Y1: [j,k] in Indices IM1 by F1,B131,B135,ZFMISC_1:87;
then consider p be FinSequence of INT such that
B133: p = IM1.j & IM1*(j,k) = p.k by MATRIX_0:def 5;
B81A: j in dom b3 by B7,FINSEQ_1:def 3;
X0: Col(FM1,j).k = FM1*(k,j) by B132,MATRIX_0:def 8
.= (AutMt(id(V2),b3,b2))*(j,k) by Y1,MATRIX_0:def 6;
IM1.j = (AutMt(id(V2), b3, b2)) /.j by B132A,PARTFUN1:def 6
.= (id(V2)).(b3/.j) |-- b2 by B81A,Def8;
hence Col(FM1,j).k = ((b3/.j) |-- b2).k by B133,X0;
end;
len Col(FM1,j) = len ((b3/.j) |-- b2) by B14,Def7;
hence thesis by B9,B11,B12,B13,B14,B15,LMThMBF1X,FINSEQ_1:def 18;
end;
hence thesis by A2,A3,MATRIX_0:27;
end;
theorem ThMBF2:
for V1, V2 being finite-rank free Z_Module,
b1 being OrdBasis of V1, b2 being OrdBasis of V2, b3 being OrdBasis of V1,
f being bilinear-Form of V1, V2 st 0 < rank V1 holds
BilinearM(f, b3, b2) =
(AutMt(id(V1), b3, b1)) * BilinearM(f, b1, b2)
proof
let V1, V2 be finite-rank free Z_Module,
b1 be OrdBasis of V1,
b2 be OrdBasis of V2,
b3 be OrdBasis of V1,
f be bilinear-Form of V1, V2;
assume AS: 0 < rank V1;
set n = len b3;
A1: len b1 = rank V1 by ThRank1;
A3: len b3 = rank V1 by ThRank1;
reconsider IM1 = AutMt(id(V1), b3, b1) as Matrix of n,INT.Ring
by LMThMBF3,A3;
reconsider M1 = IM1 as Matrix of n,INT.Ring;
set M2 = M1 * BilinearM(f, b1, b2);
B1: len M1 = n & width M1 = n
& Indices M1 = [:Seg n, Seg n:] by MATRIX_0:24;
0 < len b1 by AS,ThRank1; then
B3: len BilinearM(f, b1, b2) = len b1
& width BilinearM(f, b1, b2) = len b2 by MATRIX_0:23;
then len M2 = n & width M2 = len b2 by A1,A3,B1,MATRIX_3:def 4;
then reconsider M2 as Matrix of n,len b2, INT.Ring by A3,AS,MATRIX_0:20;
set FM1 = M1;
set FBM = BilinearM(f, b1, b2);
for i, j being Nat st [i,j] in Indices BilinearM(f, b3, b2)
holds BilinearM(f, b3, b2)*(i,j) = M2*(i,j)
proof
let i, j be Nat;
assume [i,j] in Indices BilinearM(f, b3, b2); then
B6: [i,j] in [:Seg len b3,Seg len b2 :] by AS,A3,MATRIX_0:23; then
i in Seg len b3 & j in Seg len b2 by ZFMISC_1:87;
then B8: i in dom b3 & j in dom b2 by FINSEQ_1:def 3; then
B9: (BilinearM(f, b3, b2))*(i,j) = f.(b3/.i, b2/.j) by defBilinearM;
[i,j] in Indices M2 by AS,A3,B6,MATRIX_0:23; then
B11: M2*(i,j) = Line(FM1,i) "*" Col(FBM,j) by A1,A3,B1,B3,MATRIX_3:def 4;
B12: len Line(FM1,i) = len b3 by B1,MATRIX_0:def 7;
B14: len Col(FBM,j) = len b3 by B3,A1,A3,MATRIX_0:def 8;
B13:
now
let k be Nat;
assume B131: k in Seg len b1; then
B132: k in dom FBM by B3,FINSEQ_1:def 3;
B81: k in dom b1 by B131,FINSEQ_1:def 3;
thus Col(FBM,j).k = FBM*(k,j) by B132,MATRIX_0:def 8
.= f.(b1/.k, b2/.j) by B8,B81,defBilinearM;
end;
B135: i in Seg n by B6,ZFMISC_1:87; then
B135A: i in dom M1 by B1,FINSEQ_1:def 3;
B136: i in dom b3 by B135,FINSEQ_1:def 3;
B15:
now
let k be Nat;
assume BX131: 1 <= k & k <= len Line(FM1,i); then
B131: k in Seg len b1 by B12,A1,A3,FINSEQ_1:1;
[i,k] in Indices M1 by A1,A3,B1,B131,B135,ZFMISC_1:87;
then consider p be FinSequence of INT.Ring such that
B133: p = M1.i & M1*(i,k) = p.k by MATRIX_0:def 5;
X0: Line(FM1,i).k = FM1*(i,k)
by B1,B12,BX131,FINSEQ_1:1,MATRIX_0:def 7
.= (AutMt(id(V1),b3,b1))*(i,k);
M1.i = AutMt(id(V1), b3, b1)/.i by B135A,PARTFUN1:def 6
.= (id(V1)).(b3/.i) |-- b1 by B136,Def8;
hence Line(FM1,i).k = ((b3/.i) |-- b1).k by B133,X0;
end;
len Line(FM1,i) = len ((b3/.i) |-- b1) by A1,A3,B12,Def7;
hence thesis by A1,A3,B9,B11,B12,B13,B14,B15,LMThMBF1Y,FINSEQ_1:def 18;
end;
hence thesis by MATRIX_0:27;
end;
theorem ThMBF3:
for V being finite-rank free Z_Module,
b1, b2 being OrdBasis of V, f being bilinear-Form of V, V
st 0 < rank V holds
BilinearM(f, b2, b2) = (AutMt(id(V), b2, b1))
* BilinearM(f, b1, b1) * (AutMt(id(V), b2, b1)@)
proof
let V be finite-rank free Z_Module,
b1, b2 be OrdBasis of V, f be bilinear-Form of V, V;
assume AS: 0 < rank V;
set n = len b1;
A1: len b1 = rank V by ThRank1;
reconsider IM1 = AutMt(id(V), b2, b1) as Matrix of
n,INT.Ring by LMThMBF3,A1;
reconsider IM2 = AutMt(id(V), b2, b1) as Matrix of n,INT.Ring
by LMThMBF3,A1;
reconsider M1 = IM1@ as Matrix of n,INT.Ring;
reconsider M2 = IM2 as Matrix of n,INT.Ring;
Y1: width IM1=n by MATRIX_0:24;
Yb: width BilinearM(f, b1, b1)=len b1 by MATRIX_0:24;
X1: width (AutMt(id(V), b2, b1))=len BilinearM(f, b1, b1) &
width BilinearM(f, b1, b1)=len (AutMt(id(V), b2, b1)@)
by Y1,Yb,MATRIX_0:def 2;
thus BilinearM(f, b2, b2)
= (AutMt(id(V), b2, b1)) * BilinearM(f, b1, b2) by ThMBF2,AS
.= (AutMt(id(V), b2, b1))
* (BilinearM(f, b1, b1) * (AutMt(id(V), b2, b1)@)) by ThMBF1,AS
.= (AutMt(id(V), b2, b1)) * BilinearM(f, b1, b1) *
((AutMt(id(V), b2, b1)@)) by X1,MATRIX_3:33;
end;
theorem
for V being finite-rank free Z_Module,
b1, b2 being OrdBasis of V, f being bilinear-Form of V, V
holds |. Det BilinearM(f, b2, b2) .| = |. Det BilinearM(f, b1, b1) .|
proof
let V be finite-rank free Z_Module,
b1, b2 be OrdBasis of V, f be bilinear-Form of V, V;
set n = len b1;
A1: len b1 = rank V by ThRank1;
A2: len b2 = rank V by ThRank1;
reconsider B1 = BilinearM(f, b1, b1) as Matrix of n,INT.Ring;
reconsider B2 = BilinearM(f, b2, b2) as Matrix of n,INT.Ring by A1,A2;
per cases;
suppose rank V = 0;
hence |. Det BilinearM(f, b2, b2) .| = |. Det BilinearM(f, b1, b1) .|
by A1,A2,MATRIX_0:45;
end;
suppose ZZ: rank V > 0;
then B2: BilinearM(f, b2, b2) = ((AutMt(id(V), b2, b1))
* BilinearM(f, b1, b1)) * (AutMt(id(V), b2, b1)@) by ThMBF3;
reconsider IM1 = AutMt(id(V), b2, b1) as Matrix of n,INT.Ring
by A1,LMThMBF3;
reconsider IM2 = AutMt(id(V), b2, b1) as Matrix of n,INT.Ring
by A1,LMThMBF3;
reconsider M1 = IM1@ as Matrix of n,INT.Ring;
reconsider M2 = IM2 as Matrix of n,INT.Ring;
n >= 1+0 by A1,ZZ,NAT_1:13; then
X1: Det IM1 = Det M1 by MATRIX_7:37;
reconsider M2B1 = M2 * B1 as Matrix of n, INT.Ring;
Det B2 = (Det(M2B1)) * (Det M1) by B2,ZZ,A1,MATRIX11:62
.= ((Det M2) * (Det B1)) * (Det M1) by ZZ,A1,MATRIX11:62;
hence |. Det BilinearM(f, b2, b2) .|
= |. (Det M2) * (Det B1) .| * |. Det M1 .| by A1,A2,COMPLEX1:65
.= |. (Det M2) * (Det B1) .| * 1 by A1,X1,ThSign1
.= |. Det M2 .| * |. Det B1 .| by COMPLEX1:65
.= |. Det B1 .| * 1 by A1,ThSign1
.= |. Det BilinearM(f, b1, b1) .|;
end;
end;