environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, VECTSP_7, VECTSP_1, HAHNBAN, VECTSP_5, RLVECT_2, MOD_2, HAHNBAN1, MATRLIN, VECTSP_6;
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;
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, VECTSP_2, INT_1, XBOOLE_0, ORDINAL1, FUNCOP_1, XXREAL_0, NAT_1, RELAT_1, VECTSP_1, ZFMISC_1, PRE_POLY, FUNCT_3, XCMPLX_0, ZMODUL01, ZMODUL03, MATRIX_0, VECTSP_7, INT_3, MATRIX_6, HAHNBAN1;
constructors HIDDEN, 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;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, VECTSP_1, FVSUM_1, SUBSET_1, LAPLACE, MATRIX_0, VECTSP_6, PARTFUN1, ZMODUL01, ZMODUL03, MATRLIN, INT_3, HAHNBAN1;
expansions TARSKI, BINOP_1, STRUCT_0, VECTSP_1, FUNCT_1, VECTSP_5, VECTSP_7, HAHNBAN, VECTSP_6, ZMODUL01, ZMODUL03, MATRLIN, ZMODUL05, RLVECT_2, MOD_2, HAHNBAN1;
Th5:
for V being free Z_Module
for KL1, KL2 being Linear_Combination of V
for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds
KL1 = KL2
by ZMODUL03:3;
theorem Th33:
for
m,
n being
Nat for
V1 being
free finite-rank Z_Module for
M being
Matrix of
n,
m,
INT.Ring st
n > 0 &
m > 0 holds
for
p,
d being
FinSequence of
INT.Ring st
len p = n &
len d = m & ( for
j being
Nat st
j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for
b,
c being
FinSequence of
V1 st
len b = m &
len c = n & ( for
i being
Nat st
i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
Lm1:
for V being free finite-rank Z_Module
for b being OrdBasis of V
for W being Element of V holds dom (W |-- b) = dom b
Lm2:
for p being FinSequence
for k being set st k in dom p holds
len p > 0
Lm3:
for V1, V2 being free finite-rank Z_Module
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1
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
LMLT12:
multint = multreal | [:INT,INT:]
theorem ThComp1:
for
V1,
V2,
V3 being
free finite-rank Z_Module for
f being
Function of
V1,
V2 for
g being
Function of
V2,
V3 for
b1 being
OrdBasis of
V1 for
b2 being
OrdBasis of
V2 for
b3 being
OrdBasis of
V3 st
g is
additive &
g is
homogeneous &
len b1 > 0 &
len b2 > 0 holds
AutMt (
(g * f),
b1,
b3)
= (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))
theorem LmSign1B:
for
D,
E being non
empty set for
n,
m,
i,
j being
Nat for
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
theorem LmSign1F:
for
n,
i,
j,
k,
m being
Nat for
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
LMPROJ1:
for V being free Z_Module
for 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 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 ) )
definition
let V be
free Z_Module;
let A,
B be
Subset of
V;
assume AS:
(
A c= B &
B is
Basis of
V )
;
existence
ex b1 being linear-transformation of V,V st
( ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b1 . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
b1 . v = vA ) )
by LMPROJ1, AS;
uniqueness
for b1, b2 being linear-transformation of V,V st ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b1 . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
b1 . v = vA ) & ( for v being Vector of V ex vA, vB being Vector of V st
( vA in Lin A & vB in Lin (B \ A) & v = vA + vB & b2 . v = vA ) ) & ( for v, vA, vB being Vector of V st vA in Lin A & vB in Lin (B \ A) & v = vA + vB holds
b2 . v = vA ) holds
b1 = b2
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 for
w being
Vector of
W holds
it . (
v,
w)
= (f . (v,w)) + (g . (v,w));
existence
ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w))
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds
b1 = b2
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;
existence
ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w))
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = a * (f . (v,w)) ) holds
b1 = b2
end;
definition
let V,
W be non
empty ModuleStr over
INT.Ring ;
let f be
Form of
V,
W;
existence
ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w))
uniqueness
for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = - (f . (v,w)) ) holds
b1 = b2
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:
for
v being
Vector of
V for
w being
Vector of
W holds
it . (
v,
w)
= (f . (v,w)) - (g . (v,w));
compatibility
for b1 being Form of V,W holds
( b1 = f - g iff for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) - (g . (v,w)) )
end;
theorem
for
V,
W being non
empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over
INT.Ring for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
INT.Ring for
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)))))
theorem
for
V,
W being
Z_Module for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
INT.Ring for
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)))))
definition
let V1,
V2 be
free finite-rank Z_Module;
let b1 be
OrdBasis of
V1;
let b2 be
OrdBasis of
V2;
let f be
bilinear-Form of
V1,
V2;
existence
ex b1 being Matrix of len b1, len b2,INT.Ring st
for i, j being Nat st i in dom b1 & j in dom b2 holds
b1 * (i,j) = f . ((b1 /. i),(b2 /. j))
uniqueness
for b1, b2 being Matrix of len b1, len b2,INT.Ring st ( for i, j being Nat st i in dom b1 & j in dom b2 holds
b1 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) & ( for i, j being Nat st i in dom b1 & j in dom b2 holds
b2 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) holds
b1 = b2
end;
theorem ThMBF3:
for
V being
free finite-rank Z_Module for
b1,
b2 being
OrdBasis of
V for
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)) @)