:: Quotient Vector Spaces and Functionals
:: by Jaros{\l}aw Kotowicz
::
:: Received November 5, 2002
:: Copyright (c) 2002 Association of Mizar Users
:: deftheorem defines StructVectSp VECTSP10:def 1 :
theorem :: VECTSP10:1
canceled;
theorem Th2: :: VECTSP10:2
theorem :: VECTSP10:3
theorem Th4: :: VECTSP10:4
theorem Th5: :: VECTSP10:5
theorem Th6: :: VECTSP10:6
theorem Th7: :: VECTSP10:7
theorem Th8: :: VECTSP10:8
theorem Th9: :: VECTSP10:9
theorem Th10: :: VECTSP10:10
theorem Th11: :: VECTSP10:11
theorem Th12: :: VECTSP10:12
theorem Th13: :: VECTSP10:13
theorem Th14: :: VECTSP10:14
theorem Th15: :: VECTSP10:15
theorem Th16: :: VECTSP10:16
theorem Th17: :: VECTSP10:17
theorem Th18: :: VECTSP10:18
theorem Th19: :: VECTSP10:19
theorem Th20: :: VECTSP10:20
theorem Th21: :: VECTSP10:21
:: deftheorem defines CosetSet VECTSP10:def 2 :
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:
:: VECTSP10:def 3
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 :
:: deftheorem defines zeroCoset VECTSP10:def 4 :
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:
:: VECTSP10:def 5
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 :
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 VectSp-like VectSpStr of
K means :
Def6:
:: VECTSP10:def 6
( 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 VectSp-like 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 VectSp-like 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 :
theorem Th22: :: VECTSP10:22
theorem Th23: :: VECTSP10:23
theorem Th24: :: VECTSP10:24
theorem :: VECTSP10:25
theorem :: VECTSP10:26
theorem :: VECTSP10:27
theorem Th28: :: VECTSP10:28
:: deftheorem Def7 defines constant VECTSP10:def 7 :
:: deftheorem Def8 defines coeffFunctional VECTSP10:def 8 :
theorem Th29: :: VECTSP10:29
theorem Th30: :: VECTSP10:30
theorem Th31: :: VECTSP10:31
theorem :: VECTSP10:32
theorem :: VECTSP10:33
:: deftheorem defines ker VECTSP10:def 9 :
theorem Th34: :: VECTSP10:34
:: deftheorem Def10 defines degenerated VECTSP10:def 10 :
:: deftheorem Def11 defines Ker VECTSP10:def 11 :
:: deftheorem Def12 defines QFunctional VECTSP10:def 12 :
theorem Th35: :: VECTSP10:35
:: deftheorem defines CQFunctional VECTSP10:def 13 :
theorem Th36: :: VECTSP10:36