:: VECTSP10 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let K be doubleLoopStr ;
func StructVectSp K -> strict VectSpStr of K equals :: VECTSP10:def 1
VectSpStr(# the carrier of K,the add of K,the Zero of K,the mult of K #);
coherence
VectSpStr(# the carrier of K,the add of K,the Zero of K,the mult of K #) is strict VectSpStr of K
;
end;

:: deftheorem defines StructVectSp VECTSP10:def 1 :
for K being doubleLoopStr holds StructVectSp K = VectSpStr(# the carrier of K,the add of K,the Zero of K,the mult 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 -> non empty Abelian strict ;
coherence
StructVectSp K is Abelian
proof end;
end;

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

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

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

registration
let K be non empty associative distributive left_unital doubleLoopStr ;
cluster StructVectSp K -> non empty strict VectSp-like ;
coherence
StructVectSp K is VectSp-like
proof end;
end;

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

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

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

registration
let K be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
cluster non empty add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of K;
correctness
existence
ex b1 being non empty VectSpStr of K st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is VectSp-like & b1 is strict )
;
proof end;
end;

registration
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital non degenerated doubleLoopStr ;
cluster non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like non trivial VectSpStr of K;
existence
ex b1 being non empty VectSpStr of K st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is VectSp-like & b1 is strict & not b1 is trivial )
proof end;
end;

theorem :: VECTSP10:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: VECTSP10:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for a being Element of K
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of K
for v being Vector of V holds
( (0. K) * v = 0. V & a * (0. V) = 0. V )
proof end;

theorem :: VECTSP10:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;

theorem Th4: :: VECTSP10:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th5: :: VECTSP10:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & a * v = b * v holds
a = b
proof end;

theorem Th6: :: VECTSP10:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 & v2 in W2 & v = v1 + v2 holds
v |-- W1,W2 = [v1,v2]
proof end;

theorem Th7: :: VECTSP10:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;

theorem Th8: :: VECTSP10:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 & v2 in W2 )
proof end;

theorem Th9: :: VECTSP10:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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]
proof end;

theorem Th10: :: VECTSP10:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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)]
proof end;

theorem Th11: :: VECTSP10:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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]
proof end;

theorem Th12: :: VECTSP10:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;

theorem Th13: :: VECTSP10:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 & W2 = V2 holds
W1 + W2 = V1 + V2
proof end;

theorem Th14: :: VECTSP10:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th15: :: VECTSP10:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & W = X holds
X + (Lin {v}) is_the_direct_sum_of W, Lin {y}
proof end;

theorem Th16: :: VECTSP10:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & X = W & not v in X holds
y |-- W,(Lin {y}) = [(0. W),y]
proof end;

theorem Th17: :: VECTSP10:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & X = W & 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)]
proof end;

theorem Th18: :: VECTSP10:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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]
proof end;

theorem Th19: :: VECTSP10:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & X = W & 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)]
proof end;

theorem Th20: :: VECTSP10:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & X = W & 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)] & w2 |-- W,(Lin {y}) = [x2,(r2 * v)] holds
(w1 + w2) |-- W,(Lin {y}) = [(x1 + x2),((r1 + r2) * v)]
proof end;

theorem Th21: :: VECTSP10:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & X = W & 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)]
proof end;

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
;
proof end;
end;

:: deftheorem defines CosetSet VECTSP10:def 2 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;
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
proof end;
end;

:: deftheorem Def3 defines addCoset VECTSP10:def 3 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 );

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;
end;

:: deftheorem defines zeroCoset VECTSP10:def 4 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;
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
proof end;
end;

:: deftheorem Def5 defines lmultCoset VECTSP10:def 5 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be VectSp of K;
let W be Subspace of V;
func VectQuot V,W -> non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of K means :Def6: :: VECTSP10:def 6
( the carrier of it = CosetSet V,W & the add of it = addCoset V,W & the Zero of it = zeroCoset V,W & the lmult of it = lmultCoset V,W );
existence
ex b1 being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of K st
( the carrier of b1 = CosetSet V,W & the add of b1 = addCoset V,W & the Zero of b1 = zeroCoset V,W & the lmult of b1 = lmultCoset V,W )
proof end;
uniqueness
for b1, b2 being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of K st the carrier of b1 = CosetSet V,W & the add of b1 = addCoset V,W & the Zero of b1 = zeroCoset V,W & the lmult of b1 = lmultCoset V,W & the carrier of b2 = CosetSet V,W & the add of b2 = addCoset V,W & the Zero of 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being VectSp of K
for W being Subspace of V
for b4 being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of K holds
( b4 = VectQuot V,W iff ( the carrier of b4 = CosetSet V,W & the add of b4 = addCoset V,W & the Zero of b4 = zeroCoset V,W & the lmult of b4 = lmultCoset V,W ) );

theorem Th22: :: VECTSP10:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being VectSp of K
for W being Subspace of V holds
( zeroCoset V,W = (0. V) + W & 0. (VectQuot V,W) = zeroCoset V,W )
proof end;

theorem Th23: :: VECTSP10:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 & ex v being Vector of V st w = v + W )
proof end;

theorem Th24: :: VECTSP10:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 & v + W is Vector of (VectQuot V,W) )
proof end;

theorem :: VECTSP10:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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)
proof end;

theorem :: VECTSP10:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;

theorem :: VECTSP10:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 & A2 = v2 + W holds
A1 + A2 = (v1 + v2) + W
proof end;

theorem Th28: :: VECTSP10:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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 & psi . y = r )
proof end;

registration
let K be non empty right_zeroed LoopStr ;
let V be non empty VectSpStr of K;
cluster additive 0-preserving Relation of the carrier of V,the carrier of K;
existence
ex b1 being Functional of V st
( b1 is additive & b1 is 0-preserving )
proof end;
end;

registration
let K be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let V be non empty right_zeroed VectSpStr of K;
cluster additive -> 0-preserving Relation of the carrier of V,the carrier of K;
coherence
for b1 being Functional of V st b1 is additive holds
b1 is 0-preserving
proof end;
end;

registration
let K be non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let V be non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of K;
cluster homogeneous -> 0-preserving Relation of the carrier of V,the carrier of K;
coherence
for b1 being Functional of V st b1 is homogeneous holds
b1 is 0-preserving
proof end;
end;

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

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr of K;
cluster constant Relation of the carrier of V,the carrier of K;
existence
ex b1 being Functional of V st b1 is constant
proof end;
end;

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

:: deftheorem Def7 defines constant VECTSP10:def 7 :
for K being non empty add-associative right_zeroed right_complementable 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 );

registration
let K be non empty add-associative right_zeroed right_complementable doubleLoopStr ;
let V be non empty right_zeroed VectSpStr of K;
cluster constant additive 0-preserving Relation of the carrier of V,the carrier of K;
existence
ex b1 being Functional of V st
( b1 is constant & b1 is additive & b1 is 0-preserving )
proof end;
end;

registration
let K be non empty 1-sorted ;
let V be non empty VectSpStr of K;
cluster non constant -> non trivial Relation of the carrier of V,the carrier of K;
coherence
for b1 being Functional of V st not b1 is constant holds
not b1 is trivial
proof end;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster non constant additive homogeneous 0-preserving non trivial Relation of the carrier of V,the carrier of K;
existence
ex b1 being Functional of V st
( b1 is additive & b1 is homogeneous & not b1 is constant & not b1 is trivial )
proof end;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster trivial -> constant Relation of the carrier of V,the carrier of K;
coherence
for b1 being Functional of V st b1 is trivial holds
b1 is constant
proof end;
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 -> V71 non trivial linear-Functional of V means :Def8: :: VECTSP10:def 8
( it . v = 1. K & it | the carrier of W = 0Functional W );
existence
ex b1 being V71 non trivial linear-Functional of V st
( b1 . v = 1. K & b1 | the carrier of W = 0Functional W )
proof end;
uniqueness
for b1, b2 being V71 non trivial linear-Functional of V st b1 . v = 1. K & b1 | the carrier of W = 0Functional W & b2 . v = 1. K & b2 | the carrier of W = 0Functional W holds
b1 = b2
proof end;
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 V71 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: :: VECTSP10:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being Field
for V being non trivial VectSp of K
for f being non constant 0-preserving Functional of V ex v being Vector of V st
( v <> 0. V & f . v <> 0. K )
proof end;

theorem Th30: :: VECTSP10:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th31: :: VECTSP10:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & w in W holds
(coeffFunctional v,W) . w = 0. K
proof end;

theorem :: VECTSP10:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & w in W holds
(coeffFunctional v,W) . ((a * v) + w) = a
proof end;

theorem :: VECTSP10:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty LoopStr
for V being non empty VectSpStr of K
for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
proof end;

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

definition
let K be non empty ZeroStr ;
let V be non empty VectSpStr of 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
proof end;
end;

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

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

theorem Th34: :: VECTSP10:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being non empty add-associative right_zeroed right_complementable VectSp-like VectSpStr of K
for f being linear-Functional of V holds ker f is lineary-closed
proof end;

definition
let K be non empty ZeroStr ;
let V be non empty VectSpStr of K;
let f be Functional of V;
attr f 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 of 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 empty non trivial VectSpStr of K;
cluster 0-preserving non degenerated -> non constant non trivial Relation of the carrier of V,the carrier of K;
coherence
for b1 being Functional of V st not b1 is degenerated & b1 is 0-preserving holds
not b1 is constant
proof end;
end;

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;
uniqueness
for b1, b2 being non empty strict Subspace of V st the carrier of b1 = ker f & the carrier of b2 = ker f holds
b1 = b2
by VECTSP_4:37;
end;

:: deftheorem Def11 defines Ker VECTSP10:def 11 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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 Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;
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 ) & ( 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
proof end;
end;

:: deftheorem Def12 defines QFunctional VECTSP10:def 12 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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: :: VECTSP10:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;

definition
let K be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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))
;
proof end;
end;

:: deftheorem defines CQFunctional VECTSP10:def 13 :
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for V being VectSp of K
for f being linear-Functional of V holds CQFunctional f = QFunctional f,(Ker f);

theorem Th36: :: VECTSP10:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for K being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital 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
proof end;

registration
let K be Field;
let V be non trivial VectSp of K;
let f be V71 linear-Functional of V;
cluster CQFunctional f -> V71 0-preserving non trivial ;
coherence
not CQFunctional f is constant
proof end;
end;

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