environ
vocabularies HIDDEN, ALGSTR_0, STRUCT_0, VECTSP_1, SUPINF_2, XBOOLE_0, RLVECT_1, SUBSET_1, ARYTM_3, BINOP_1, LATTICES, FUNCT_1, RELAT_1, MESFUNC1, ZFMISC_1, RLSUB_1, RLVECT_3, RLVECT_2, CARD_3, FUNCT_2, TARSKI, ARYTM_1, RLSUB_2, FINSEQ_4, MCART_1, GROUP_1, SETFAM_1, HAHNBAN, MSSUBFAM, UNIALG_1, HAHNBAN1, GROUP_6, VECTSP10;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, DOMAIN_1, RELSET_1, FUNCT_2, STRUCT_0, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, GRCAT_1, HAHNBAN1;
definitions HAHNBAN1, TARSKI, XBOOLE_0, VECTSP_4, VECTSP_5, RLVECT_1, FUNCT_1, ALGSTR_0, VECTSP_1;
theorems XBOOLE_1, FUNCT_2, HAHNBAN1, VECTSP_1, RLVECT_1, MCART_1, VECTSP_5, VECTSP_4, VECTSP_6, VECTSP_7, TARSKI, FUNCT_1, XBOOLE_0, ZFMISC_1, BINOP_1, GROUP_1, STRUCT_0, ALGSTR_0, XTUPLE_0;
schemes FUNCT_2, BINOP_1;
registrations SUBSET_1, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_4, HAHNBAN1, ALGSTR_0, FUNCT_2, RELAT_1, ZFMISC_1, RELSET_1, XTUPLE_0;
constructors HIDDEN, REALSET2, VECTSP_5, VECTSP_6, VECTSP_7, HAHNBAN1, RELSET_1, GRCAT_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities HAHNBAN1, XBOOLE_0, VECTSP_4, STRUCT_0, ALGSTR_0, VECTSP_1;
expansions HAHNBAN1, TARSKI, XBOOLE_0, VECTSP_5, RLVECT_1, FUNCT_1, STRUCT_0, VECTSP_1;
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be
VectSp of
K;
let W be
Subspace of
V;
existence
ex b1 being BinOp of (CosetSet (V,W)) st
for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W
uniqueness
for b1, b2 being BinOp of (CosetSet (V,W)) st ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
b1 . (A,B) = (a + b) + W ) & ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W & B = b + W holds
b2 . (A,B) = (a + b) + W ) holds
b1 = b2
end;
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be
VectSp of
K;
let W be
Subspace of
V;
existence
ex b1 being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) st
for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b1 . (z,A) = (z * a) + W
uniqueness
for b1, b2 being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) st ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b1 . (z,A) = (z * a) + W ) & ( for z being Element of K
for A being Element of CosetSet (V,W)
for a being Vector of V st A = a + W holds
b2 . (z,A) = (z * a) + W ) holds
b1 = b2
end;
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;
let V be
VectSp of
K;
let W be
Subspace of
V;
existence
ex b1 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K st
( the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) )
uniqueness
for b1, b2 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K st the carrier of b1 = CosetSet (V,W) & the addF of b1 = addCoset (V,W) & 0. b1 = zeroCoset (V,W) & the lmult of b1 = lmultCoset (V,W) & the carrier of b2 = CosetSet (V,W) & the addF of b2 = addCoset (V,W) & 0. b2 = zeroCoset (V,W) & the lmult of b2 = lmultCoset (V,W) holds
b1 = b2
;
end;