:: Quotient Vector Spaces and Functionals
:: by Jaros{\l}aw Kotowicz
::
:: Received November 5, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

::Auxiliary Facts about Double Loops and Vector Spaces
definition
let K be doubleLoopStr ;
func StructVectSp K ->  strict VectSpStr over K equals :: VECTSP10:def 1
 VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #);
coherence
 VectSpStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is strict VectSpStr over K ;
end;

:: 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 #);

registration
let K be non empty doubleLoopStr ;
cluster StructVectSp K ->  non empty strict ;
coherence
 not StructVectSp K is empty ;
end;

registration
let K be non empty Abelian doubleLoopStr ;
cluster StructVectSp K ->  Abelian strict ;
coherence
 StructVectSp K is Abelian
proofend;
end;

registration
let K be non empty add-associative doubleLoopStr ;
cluster StructVectSp K ->  add-associative strict ;
coherence
 StructVectSp K is add-associative
proofend;
end;

registration
let K be non empty right_zeroed doubleLoopStr ;
cluster StructVectSp K ->  right_zeroed strict ;
coherence
 StructVectSp K is right_zeroed
proofend;
end;

registration
let K be non empty right_complementable doubleLoopStr ;
cluster StructVectSp K ->  right_complementable strict ;
coherence
 StructVectSp K is right_complementable
proofend;
end;

registration
let K be non empty associative distributive left_unital doubleLoopStr ;
cluster StructVectSp K ->  strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital )
proofend;
end;

registration
let K be non empty non degenerated doubleLoopStr ;
cluster StructVectSp K ->  non trivial strict ;
coherence
 not StructVectSp K is trivial ;
end;

registration
let K be non empty non degenerated doubleLoopStr ;
cluster non trivial for VectSpStr over K;
existence
 not for b1 being VectSpStr over K holds b1 is trivial
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
cluster non empty right_complementable add-associative right_zeroed strict for VectSpStr over K;
correctness
existence
ex b1 being non empty VectSpStr over K st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict );
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr ;
cluster non empty right_complementable add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for VectSpStr over K;
correctness
existence
ex b1 being non empty VectSpStr over K st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is strict );
proofend;
end;

registration
let K be non empty non degenerated right_complementable Abelian add-associative right_zeroed associative distributive left_unital doubleLoopStr ;
cluster non empty non trivial right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for VectSpStr over K;
existence
 ex b1 being non trivial VectSpStr over K st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is strict )
proofend;
end;

theorem Th1: :: VECTSP10:1
for K being non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr
for a being Element of K
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for v being Vector of V holds
( (0. K) * v = 0. V & a * (0. V) = 0. V )
proofend;

theorem :: VECTSP10: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 S, T being Subspace of V
for v being Vector of V st S /\ T = (0). V & v in S & v in T holds
v = 0. V
proofend;

theorem Th3: :: VECTSP10:3
for K being Field
for V being VectSp of K
for x being set
for v being Vector of V holds
( x in Lin {v} iff ex a being Element of K st x = a * v )
proofend;

theorem Th4: :: VECTSP10:4
for K being Field
for V being VectSp of K
for v being Vector of V
for a, b being Scalar of st v <> 0. V &amp; a * v = b * v holds
a = b
proofend;

theorem Th5: :: VECTSP10: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 W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v1 in W1 &amp; v2 in W2 &amp; v = v1 + v2 holds
v |-- (W1,W2) = [v1,v2]
proofend;

theorem Th6: :: VECTSP10: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 W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v = v1 + v2
proofend;

theorem Th7: :: VECTSP10:7
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
( v1 in W1 &amp; v2 in W2 )
proofend;

theorem Th8: :: VECTSP10:8
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v, v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2] holds
v |-- (W2,W1) = [v2,v1]
proofend;

theorem Th9: :: VECTSP10:9
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W1 holds
v |-- (W1,W2) = [v,(0. V)]
proofend;

theorem Th10: :: VECTSP10:10
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for v being Vector of V st v in W2 holds
v |-- (W1,W2) = [(0. V),v]
proofend;

theorem Th11: :: VECTSP10: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 V1 being Subspace of V
for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1
proofend;

theorem Th12: :: VECTSP10: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 V1, V2, W being Subspace of V
for W1, W2 being Subspace of W st W1 = V1 &amp; W2 = V2 holds
W1 + W2 = V1 + V2
proofend;

theorem Th13: :: VECTSP10:13
for K being Field
for V being VectSp of K
for W being Subspace of V
for v being Vector of V
for w being Vector of W st v = w holds
Lin {w} = Lin {v}
proofend;

theorem Th14: :: VECTSP10:14
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V st not v in X holds
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y &amp; W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
proofend;

theorem Th15: :: VECTSP10:15
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y &amp; X = W &amp; not v in X holds
y |-- (W,(Lin {y})) = [(0. W),y]
proofend;

theorem Th16: :: VECTSP10:16
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y &amp; X = W &amp; not v in X holds
for w being Vector of (X + (Lin {v})) st w in X holds
w |-- (W,(Lin {y})) = [w,(0. V)]
proofend;

theorem Th17: :: VECTSP10:17
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for v being Vector of V
for W1, W2 being Subspace of V ex v1, v2 being Vector of V st v |-- (W1,W2) = [v1,v2]
proofend;

theorem Th18: :: VECTSP10:18
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y &amp; X = W &amp; not v in X holds
for w being Vector of (X + (Lin {v})) ex x being Vector of X ex r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)]
proofend;

theorem Th19: :: VECTSP10:19
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y &amp; X = W &amp; not v in X holds
for w1, w2 being Vector of (X + (Lin {v}))
for x1, x2 being Vector of X
for r1, r2 being Element of K st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] &amp; w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds
(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]
proofend;

theorem Th20: :: VECTSP10:20
for K being Field
for V being VectSp of K
for v being Vector of V
for X being Subspace of V
for y being Vector of (X + (Lin {v}))
for W being Subspace of X + (Lin {v}) st v = y &amp; X = W &amp; not v in X holds
for w being Vector of (X + (Lin {v}))
for x being Vector of X
for t, r being Element of K st w |-- (W,(Lin {y})) = [x,(r * v)] holds
(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]
proofend;

begin

:: Quotient Vector Space for non commutative Double Loop
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 CosetSet (V,W) ->  non empty Subset-Family of V equals :: VECTSP10:def 2
 {  A where A is Coset of W : verum  }  ;
correctness
coherence
{  A where A is Coset of W : verum  }  is non empty Subset-Family of V;
proofend;
end;

:: 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: :: VECTSP10:def 3
 for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W &amp; 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 &amp; B = b + W holds
b1 . (A,B) = (a + b) + W
proofend;
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 &amp; B = b + W holds
b1 . (A,B) = (a + b) + W ) &amp; ( for A, B being Element of CosetSet (V,W)
for a, b being Vector of V st A = a + W &amp; B = b + W holds
b2 . (A,B) = (a + b) + W ) holds
b1 = b2
proofend;
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 &amp; B = b + W holds
b4 . (A,B) = (a + b) + 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 zeroCoset (V,W) ->  Element of CosetSet (V,W) equals :: VECTSP10:def 4
 the carrier of W;
coherence
 the carrier of W is Element of CosetSet (V,W)
proofend;
end;

:: 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: :: 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
proofend;
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 ) &amp; ( 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
proofend;
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 over K means :Def6: :: VECTSP10:def 6
( the carrier of it = CosetSet (V,W) &amp; the addF of it = addCoset (V,W) &amp; 0. it = zeroCoset (V,W) &amp; 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 over K st
( the carrier of b1 = CosetSet (V,W) &amp; the addF of b1 = addCoset (V,W) &amp; 0. b1 = zeroCoset (V,W) &amp; the lmult of b1 = lmultCoset (V,W) )
proofend;
uniqueness
 for b1, b2 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K st the carrier of b1 = CosetSet (V,W) &amp; the addF of b1 = addCoset (V,W) &amp; 0. b1 = zeroCoset (V,W) &amp; the lmult of b1 = lmultCoset (V,W) &amp; the carrier of b2 = CosetSet (V,W) &amp; the addF of b2 = addCoset (V,W) &amp; 0. b2 = zeroCoset (V,W) &amp; 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 over K holds
( b4 = VectQuot (V,W) iff ( the carrier of b4 = CosetSet (V,W) &amp; the addF of b4 = addCoset (V,W) &amp; 0. b4 = zeroCoset (V,W) &amp; the lmult of b4 = lmultCoset (V,W) ) );

theorem Th21: :: VECTSP10:21
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) = (0. V) + W &amp; 0. (VectQuot (V,W)) = zeroCoset (V,W) )
proofend;

theorem Th22: :: VECTSP10:22
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 w being Vector of (VectQuot (V,W)) holds
( w is Coset of W &amp; ex v being Vector of V st w = v + W )
proofend;

theorem Th23: :: VECTSP10:23
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 v being Vector of V holds
( v + W is Coset of W &amp; v + W is Vector of (VectQuot (V,W)) )
proofend;

theorem :: VECTSP10:24
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 A being Coset of W holds A is Vector of (VectQuot (V,W))
proofend;

theorem :: VECTSP10:25
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 A being Vector of (VectQuot (V,W))
for v being Vector of V
for a being Scalar of st A = v + W holds
a * A = (a * v) + W
proofend;

theorem :: VECTSP10:26
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 A1, A2 being Vector of (VectQuot (V,W))
for v1, v2 being Vector of V st A1 = v1 + W &amp; A2 = v2 + W holds
A1 + A2 = (v1 + v2) + W
proofend;

begin

:: Auxiliary Facts about Functionals
theorem Th27: :: VECTSP10:27
for K being Field
for V being VectSp of K
for X being Subspace of V
for fi being linear-Functional of X
for v being Vector of V
for y being Vector of (X + (Lin {v})) st v = y &amp; not v in X holds
for r being Element of K ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi &amp; psi . y = r )
proofend;

registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like non empty V14( the carrier of V) quasi_total additive 0-preserving for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st
( b1 is additive &amp; b1 is 0-preserving )
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
cluster Function-like quasi_total additive  ->  0-preserving for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st b1 is additive holds
b1 is 0-preserving
proofend;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
cluster Function-like quasi_total homogeneous  ->  0-preserving for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st b1 is homogeneous holds
b1 is 0-preserving
proofend;
end;

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
cluster 0Functional V ->  constant ;
coherence
 0Functional V is constant
proofend;
end;

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st b1 is constant
proofend;
end;

definition
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let f be 0-preserving Functional of V;
:: original:constant
redefine attrf is constant  means :Def7: :: VECTSP10:def 7
f = 0Functional V;
compatibility
 ( f is constant iff f = 0Functional V )
proofend;
end;

:: 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 over K
for f being 0-preserving Functional of V holds
( f is constant iff f = 0Functional V );

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like constant non empty V14( the carrier of V) quasi_total additive 0-preserving for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st
( b1 is constant &amp; b1 is additive &amp; b1 is 0-preserving )
proofend;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
clusterV1() V4( the carrier of V) V5( the carrier of K) Function-like non constant non empty non trivial V14( the carrier of V) quasi_total additive homogeneous for Element of bool [: the carrier of V, the carrier of K:];
existence
 ex b1 being Functional of V st
( b1 is additive &amp; b1 is homogeneous &amp; not b1 is constant &amp; not b1 is trivial )
proofend;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster Function-like trivial quasi_total  ->  constant for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st b1 is trivial holds
b1 is constant ;
end;

definition
let K be Field;
let V be non trivial VectSp of K;
let v be Vector of V;
let W be Linear_Compl of Lin {v};
assume A1: v <> 0. V ;
func coeffFunctional (v,W) ->  V8() non trivial linear-Functional of V means :Def8: :: VECTSP10:def 8
( it . v = 1_ K &amp; it | the carrier of W = 0Functional W );
existence
 ex b1 being V8() non trivial linear-Functional of V st
( b1 . v = 1_ K &amp; b1 | the carrier of W = 0Functional W )
proofend;
uniqueness
 for b1, b2 being V8() non trivial linear-Functional of V st b1 . v = 1_ K &amp; b1 | the carrier of W = 0Functional W &amp; b2 . v = 1_ K &amp; b2 | the carrier of W = 0Functional W holds
b1 = b2
proofend;
end;

:: 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 &amp; b5 | the carrier of W = 0Functional W ) );

theorem Th28: :: VECTSP10:28
for K being Field
for V being non trivial VectSp of K
for f being V8() 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V &amp; f . v <> 0. K )
proofend;

theorem Th29: :: VECTSP10:29
for K being Field
for V being non trivial VectSp of K
for v being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V holds
(coeffFunctional (v,W)) . (a * v) = a
proofend;

theorem Th30: :: VECTSP10:30
for K being Field
for V being non trivial VectSp of K
for v, w being Vector of V
for W being Linear_Compl of Lin {v} st v <> 0. V &amp; w in W holds
(coeffFunctional (v,W)) . w = 0. K
proofend;

theorem :: VECTSP10:31
for K being Field
for V being non trivial VectSp of K
for v, w being Vector of V
for a being Scalar of
for W being Linear_Compl of Lin {v} st v <> 0. V &amp; w in W holds
(coeffFunctional (v,W)) . ((a * v) + w) = a
proofend;

theorem :: VECTSP10:32
for K being non empty addLoopStr
for V being non empty VectSpStr over K
for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
proofend;

registration
let K be Field;
let V be non trivial VectSp of K;
clusterV *'  ->  non trivial ;
coherence
 not V *' is trivial
proofend;
end;

begin

:: Kernel of Additive Functional and Subspace Generated by Kernel of
:: Linear Functional. Linear Functionals in Quotient Vector Space
:: generated by Additive Functional
definition
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
let f be Functional of V;
func ker f ->  Subset of V equals :: VECTSP10:def 9
 {  v where v is Vector of V : f . v = 0. K  }  ;
coherence
  {  v where v is Vector of V : f . v = 0. K  }  is Subset of V
proofend;
end;

:: deftheorem  defines ker VECTSP10:def_9_:_
 for K being non empty ZeroStr
for V being non empty VectSpStr over K
for f being Functional of V holds ker f =  {  v where v is Vector of V : f . v = 0. K  }  ;

registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
let f be 0-preserving Functional of V;
cluster ker f ->  non empty ;
coherence
 not ker f is empty
proofend;
end;

theorem Th33: :: VECTSP10:33
for K being non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for f being linear-Functional of V holds ker f is linearly-closed
proofend;

definition
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
let f be Functional of V;
attrf is degenerated  means :Def10: :: VECTSP10:def 10
 ker f <> {(0. V)};
end;

:: deftheorem Def10 defines degenerated VECTSP10:def_10_:_
 for K being non empty ZeroStr
for V being non empty VectSpStr over K
for f being Functional of V holds
( f is degenerated iff ker f <> {(0. V)} );

registration
let K be non empty non degenerated doubleLoopStr ;
let V be non trivial VectSpStr over K;
cluster Function-like quasi_total 0-preserving non degenerated  ->  non constant for Element of bool [: the carrier of V, the carrier of K:];
coherence
 for b1 being Functional of V st not b1 is degenerated &amp; b1 is 0-preserving holds
not b1 is constant
proofend;
end;

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 f be linear-Functional of V;
func Ker f ->  non empty strict Subspace of V means :Def11: :: VECTSP10:def 11
 the carrier of it = ker f;
existence
 ex b1 being non empty strict Subspace of V st the carrier of b1 = ker f by Th33, VECTSP_4:34;
uniqueness
 for b1, b2 being non empty strict Subspace of V st the carrier of b1 = ker f &amp; the carrier of b2 = ker f holds
b1 = b2 by VECTSP_4:29;
end;

:: 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 );

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;
let f be additive Functional of V;
assume A1: the carrier of W c= ker f ;
func QFunctional (f,W) ->  additive Functional of (VectQuot (V,W)) means :Def12: :: VECTSP10:def 12
 for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
it . A = f . a;
existence
 ex b1 being additive Functional of (VectQuot (V,W)) st
for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b1 . A = f . a
proofend;
uniqueness
 for b1, b2 being additive Functional of (VectQuot (V,W)) st ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b1 . A = f . a ) &amp; ( for A being Vector of (VectQuot (V,W))
for a being Vector of V st A = a + W holds
b2 . A = f . a ) holds
b1 = b2
proofend;
end;

:: 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 Th34: :: VECTSP10:34
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 linear-Functional of V st the carrier of W c= ker f holds
QFunctional (f,W) is homogeneous
proofend;

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 f be linear-Functional of V;
func CQFunctional f ->  linear-Functional of (VectQuot (V,(Ker f))) equals :: VECTSP10:def 13
 QFunctional (f,(Ker f));
correctness
coherence
QFunctional (f,(Ker f)) is linear-Functional of (VectQuot (V,(Ker f)));
proofend;
end;

:: 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 Th35: :: VECTSP10:35
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 A being Vector of (VectQuot (V,(Ker f)))
for v being Vector of V st A = v + (Ker f) holds
(CQFunctional f) . A = f . v
proofend;

registration
let K be Field;
let V be non trivial VectSp of K;
let f be V8() linear-Functional of V;
cluster CQFunctional f -> V8() ;
coherence
 not CQFunctional f is constant
proofend;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let f be linear-Functional of V;
cluster CQFunctional f ->  non degenerated ;
coherence
 not CQFunctional f is degenerated
proofend;
end;