environ
vocabularies HIDDEN, RLVECT_1, ALGSTR_0, BINOP_1, VECTSP_1, LATTICES, XBOOLE_0, SUBSET_1, ARYTM_1, RELAT_1, ARYTM_3, RLSUB_1, SUPINF_2, GROUP_1, STRUCT_0, TARSKI, REALSET1, ZFMISC_1, FUNCT_1, MESFUNC1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, STRUCT_0, ALGSTR_0, DOMAIN_1, BINOP_1, RLVECT_1, GROUP_1, VECTSP_1;
definitions TARSKI, RLVECT_1, XBOOLE_0, ALGSTR_0, VECTSP_1;
theorems FUNCT_1, FUNCT_2, TARSKI, VECTSP_1, ZFMISC_1, RLVECT_1, RELAT_1, VECTSP_2, RELSET_1, XBOOLE_0, XBOOLE_1, ALGSTR_0;
schemes XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, REALSET1, STRUCT_0, VECTSP_1, RELAT_1, ALGSTR_0;
constructors HIDDEN, PARTFUN1, BINOP_1, REALSET1, VECTSP_1, RLVECT_1, RELSET_1, GROUP_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, VECTSP_1;
expansions TARSKI, XBOOLE_0, STRUCT_0;
Lm1:
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for a, b being Element of GF
for v being Element of V holds (a - b) * v = (a * v) - (b * v)
Lm2:
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W being Subspace of V
for V1 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
Lm3:
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W being Subspace of V holds (0. V) + W = the carrier of W
Lm4:
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v being Element of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
:: Auxiliary theorems.
::