begin
:: deftheorem defines StructVectSp VECTSP10:def 1 :
for K being doubleLoopStr holds StructVectSp K = VectSpStr(# the carrier of K,the addF of K,(0. K),the multF of K #);
theorem
canceled;
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
:: deftheorem defines CosetSet VECTSP10:def 2 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V holds CosetSet V,W = { A where A is Coset of W : verum } ;
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be
VectSp of
K;
let W be
Subspace of
V;
func addCoset V,
W -> BinOp of
(CosetSet V,W) means :
Def3:
for
A,
B being
Element of
CosetSet V,
W for
a,
b being
Vector of
V st
A = a + W &
B = b + W holds
it . A,
B = (a + b) + W;
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;
:: deftheorem Def3 defines addCoset VECTSP10:def 3 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b4 being BinOp of (CosetSet V,W) holds
( b4 = addCoset V,W iff for A, B being Element of CosetSet V,W
for a, b being Vector of V st A = a + W & B = b + W holds
b4 . A,B = (a + b) + W );
:: deftheorem defines zeroCoset VECTSP10:def 4 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V holds zeroCoset V,W = the carrier of W;
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be
VectSp of
K;
let W be
Subspace of
V;
func lmultCoset V,
W -> Function of
[:the carrier of K,(CosetSet V,W):],
(CosetSet V,W) means :
Def5:
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
it . z,
A = (z * a) + W;
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;
:: deftheorem Def5 defines lmultCoset VECTSP10:def 5 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b4 being Function of [:the carrier of K,(CosetSet V,W):],(CosetSet V,W) holds
( b4 = lmultCoset V,W iff 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
b4 . z,A = (z * a) + W );
definition
let K be non
empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be
VectSp of
K;
let W be
Subspace of
V;
func VectQuot V,
W -> non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of
K means :
Def6:
( the
carrier of
it = CosetSet V,
W & the
addF of
it = addCoset V,
W &
0. it = zeroCoset V,
W & the
lmult of
it = lmultCoset V,
W );
existence
ex b1 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of 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 VectSpStr of 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;
:: deftheorem Def6 defines VectQuot VECTSP10:def 6 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b4 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of K holds
( b4 = VectQuot V,W iff ( the carrier of b4 = CosetSet V,W & the addF of b4 = addCoset V,W & 0. b4 = zeroCoset V,W & the lmult of b4 = lmultCoset V,W ) );
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem
theorem
begin
theorem Th28:
:: deftheorem Def7 defines constant VECTSP10:def 7 :
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V being non empty right_zeroed VectSpStr of K
for f being 0-preserving Functional of V holds
( f is constant iff f = 0Functional V );
:: deftheorem Def8 defines coeffFunctional VECTSP10:def 8 :
for K being Field
for V being non trivial VectSp of K
for v being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V holds
for b5 being V8() non trivial linear-Functional of V holds
( b5 = coeffFunctional v,W iff ( b5 . v = 1_ K & b5 | the carrier of W = 0Functional W ) );
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem
begin
:: deftheorem defines ker VECTSP10:def 9 :
for K being non empty ZeroStr
for V being non empty VectSpStr of K
for f being Functional of V holds ker f = { v where v is Vector of V : f . v = 0. K } ;
theorem Th34:
:: deftheorem Def10 defines degenerated VECTSP10:def 10 :
for K being non empty ZeroStr
for V being non empty VectSpStr of K
for f being Functional of V holds
( f is degenerated iff ker f <> {(0. V)} );
:: deftheorem Def11 defines Ker VECTSP10:def 11 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V
for b4 being non empty strict Subspace of V holds
( b4 = Ker f iff the carrier of b4 = ker f );
:: deftheorem Def12 defines QFunctional VECTSP10:def 12 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for f being additive Functional of V st the carrier of W c= ker f holds
for b5 being additive Functional of (VectQuot V,W) holds
( b5 = QFunctional f,W iff for A being Vector of (VectQuot V,W)
for a being Vector of V st A = a + W holds
b5 . A = f . a );
theorem Th35:
:: deftheorem defines CQFunctional VECTSP10:def 13 :
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V holds CQFunctional f = QFunctional f,(Ker f);
theorem Th36: