:: by Jaros{\l}aw Kotowicz

::

:: Received November 5, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

::Auxiliary Facts about Double Loops and Vector Spaces

definition

let K be doubleLoopStr ;

ModuleStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is strict ModuleStr over K ;

end;
func StructVectSp K -> strict ModuleStr over K equals :: VECTSP10:def 1

ModuleStr(# the carrier of K, the addF of K,(0. K), the multF of K #);

coherence ModuleStr(# the carrier of K, the addF of K,(0. K), the multF of K #);

ModuleStr(# the carrier of K, the addF of K,(0. K), the multF of K #) is strict ModuleStr over K ;

:: deftheorem defines StructVectSp VECTSP10:def 1 :

for K being doubleLoopStr holds StructVectSp K = ModuleStr(# the carrier of K, the addF of K,(0. K), the multF of K #);

for K being doubleLoopStr holds StructVectSp K = ModuleStr(# the carrier of K, the addF of K,(0. K), the multF of K #);

registration
end;

registration

let K be non empty add-associative doubleLoopStr ;

coherence

StructVectSp K is add-associative

end;
coherence

StructVectSp K is add-associative

proof end;

registration
end;

registration

let K be non empty right_complementable doubleLoopStr ;

coherence

StructVectSp K is right_complementable

end;
coherence

StructVectSp K is right_complementable

proof end;

registration

let K be non empty distributive left_unital associative doubleLoopStr ;

( StructVectSp K is vector-distributive & StructVectSp K is scalar-distributive & StructVectSp K is scalar-associative & StructVectSp K is scalar-unital )

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

proof end;

registration
end;

registration

let K be non empty non degenerated doubleLoopStr ;

existence

not for b_{1} being ModuleStr over K holds b_{1} is trivial

end;
existence

not for b

proof end;

registration

let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

correctness

existence

ex b_{1} being non empty ModuleStr over K st

( b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict );

end;
correctness

existence

ex b

( b

proof end;

registration

let K be non empty right_complementable add-associative right_zeroed distributive left_unital associative doubleLoopStr ;

existence

ex b_{1} being non empty ModuleStr over K st

( b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is strict );

end;
cluster non empty right_complementable add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for ModuleStr over K;

correctness existence

ex b

( b

proof end;

registration

let K be non empty non degenerated right_complementable Abelian add-associative right_zeroed distributive left_unital associative doubleLoopStr ;

ex b_{1} being non trivial ModuleStr over K st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is strict )

end;
cluster non empty non trivial right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for ModuleStr over K;

existence ex b

( b

proof end;

theorem Th1: :: VECTSP10:1

for K being non empty right_complementable add-associative right_zeroed distributive left_unital associative 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 ModuleStr over K

for v being Vector of V holds

( (0. K) * v = 0. V & a * (0. V) = 0. V )

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 ModuleStr over K

for v being Vector of V holds

( (0. K) * v = 0. V & a * (0. V) = 0. V )

proof end;

theorem :: VECTSP10:2

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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 Th3: :: VECTSP10:3

for K being Field

for V being VectSp of K

for x being object

for v being Vector of V holds

( x in Lin {v} iff ex a being Element of K st x = a * v )

for V being VectSp of K

for x being object

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 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 & a * v = b * v holds

a = b

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 Th5: :: VECTSP10:5

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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]

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 Th6: :: VECTSP10:6

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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 Th7: :: VECTSP10:7

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 )

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 Th8: :: VECTSP10:8

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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]

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 Th9: :: VECTSP10:9

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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)]

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 Th10: :: VECTSP10:10

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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]

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 Th11: :: VECTSP10:11

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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 Th12: :: VECTSP10:12

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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

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 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 & W = X holds

X + (Lin {v}) is_the_direct_sum_of W, Lin {y}

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 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 & X = W & not v in X holds

y |-- (W,(Lin {y})) = [(0. W),y]

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 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 & 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)]

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 Th17: :: VECTSP10:17

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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]

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 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 & 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)]

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 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 & 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)]

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 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 & 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)]

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;

:: Quotient Vector Space for non commutative Double Loop

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;

coherence

{ A where A is Coset of W : verum } is non empty Subset-Family of V;

end;
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 { A where A is Coset of W : verum } ;

coherence

{ A where A is Coset of W : verum } is non empty Subset-Family of V;

proof end;

:: deftheorem defines CosetSet VECTSP10:def 2 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 } ;

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 well-unital distributive associative doubleLoopStr ;

let V be VectSp of K;

let W be Subspace of V;

ex b_{1} 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

b_{1} . (A,B) = (a + b) + W

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (A,B) = (a + b) + W ) holds

b_{1} = b_{2}

end;
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 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;

ex b

for A, B being Element of CosetSet (V,W)

for a, b being Vector of V st A = a + W & B = b + W holds

b

proof end;

uniqueness for b

for a, b being Vector of V st A = a + W & B = b + W holds

b

for a, b being Vector of V st A = a + W & B = b + W holds

b

b

proof end;

:: deftheorem Def3 defines addCoset VECTSP10:def 3 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for W being Subspace of V

for b_{4} being BinOp of (CosetSet (V,W)) holds

( b_{4} = 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

b_{4} . (A,B) = (a + b) + W );

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for W being Subspace of V

for b

( b

for a, b being Vector of V st A = a + W & B = b + W holds

b

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;

coherence

the carrier of W is Element of CosetSet (V,W)

end;
let V be VectSp of K;

let W be Subspace of V;

coherence

the carrier of W is Element of CosetSet (V,W)

proof end;

:: deftheorem defines zeroCoset VECTSP10:def 4 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for W being Subspace of V holds zeroCoset (V,W) = the carrier of W;

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 well-unital distributive associative doubleLoopStr ;

let V be VectSp of K;

let W be Subspace of V;

ex b_{1} 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

b_{1} . (z,A) = (z * a) + W

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (z,A) = (z * a) + W ) holds

b_{1} = b_{2}

end;
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 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;

ex b

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

b

proof end;

uniqueness for b

for A being Element of CosetSet (V,W)

for a being Vector of V st A = a + W holds

b

for A being Element of CosetSet (V,W)

for a being Vector of V st A = a + W holds

b

b

proof end;

:: deftheorem Def5 defines lmultCoset VECTSP10:def 5 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for W being Subspace of V

for b_{4} being Function of [: the carrier of K,(CosetSet (V,W)):],(CosetSet (V,W)) holds

( b_{4} = 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

b_{4} . (z,A) = (z * a) + W );

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for W being Subspace of V

for b

( b

for A being Element of CosetSet (V,W)

for a being Vector of V st A = a + W holds

b

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;

ex b_{1} 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 b_{1} = CosetSet (V,W) & the addF of b_{1} = addCoset (V,W) & 0. b_{1} = zeroCoset (V,W) & the lmult of b_{1} = lmultCoset (V,W) )

for b_{1}, b_{2} 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 b_{1} = CosetSet (V,W) & the addF of b_{1} = addCoset (V,W) & 0. b_{1} = zeroCoset (V,W) & the lmult of b_{1} = lmultCoset (V,W) & the carrier of b_{2} = CosetSet (V,W) & the addF of b_{2} = addCoset (V,W) & 0. b_{2} = zeroCoset (V,W) & the lmult of b_{2} = lmultCoset (V,W) holds

b_{1} = b_{2}
;

end;
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 ModuleStr over 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 ( 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) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines VectQuot VECTSP10:def 6 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for W being Subspace of V

for b_{4} being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K holds

( b_{4} = VectQuot (V,W) iff ( the carrier of b_{4} = CosetSet (V,W) & the addF of b_{4} = addCoset (V,W) & 0. b_{4} = zeroCoset (V,W) & the lmult of b_{4} = lmultCoset (V,W) ) );

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for W being Subspace of V

for b

( b

theorem Th21: :: VECTSP10:21

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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) )

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 Th22: :: VECTSP10:22

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 )

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 Th23: :: VECTSP10:23

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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)) )

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:24

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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))

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:25

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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:26

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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;

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

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 addLoopStr ;

let V be non empty ModuleStr over K;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is 0-preserving )

end;
let V be non empty ModuleStr over K;

cluster V1() 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 b

( b

proof end;

registration

let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let V be non empty right_zeroed ModuleStr over K;

for b_{1} being Functional of V st b_{1} is additive holds

b_{1} is 0-preserving

end;
let V be non empty right_zeroed ModuleStr over K;

cluster Function-like quasi_total additive -> 0-preserving for Element of bool [: the carrier of V, the carrier of K:];

coherence for b

b

proof end;

registration

let K be non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr ;

let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K;

for b_{1} being Functional of V st b_{1} is homogeneous holds

b_{1} is 0-preserving

end;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K;

cluster Function-like quasi_total homogeneous -> 0-preserving for Element of bool [: the carrier of V, the carrier of K:];

coherence for b

b

proof end;

registration

let K be non empty ZeroStr ;

let V be non empty ModuleStr over K;

coherence

0Functional V is constant

end;
let V be non empty ModuleStr over K;

coherence

0Functional V is constant

proof end;

registration

let K be non empty ZeroStr ;

let V be non empty ModuleStr over K;

ex b_{1} being Functional of V st b_{1} is constant

end;
let V be non empty ModuleStr over K;

cluster V1() 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 b

proof end;

definition

let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;

let V be non empty right_zeroed ModuleStr over K;

let f be 0-preserving Functional of V;

compatibility

( f is constant iff f = 0Functional V )

end;
let V be non empty right_zeroed ModuleStr over K;

let f be 0-preserving Functional of V;

compatibility

( f is constant iff f = 0Functional V )

proof end;

:: deftheorem defines constant VECTSP10:def 7 :

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr

for V being non empty right_zeroed ModuleStr over K

for f being 0-preserving Functional of V holds

( f is constant iff f = 0Functional V );

for K being non empty right_complementable add-associative right_zeroed doubleLoopStr

for V being non empty right_zeroed ModuleStr 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 ModuleStr over K;

ex b_{1} being Functional of V st

( b_{1} is constant & b_{1} is additive & b_{1} is 0-preserving )

end;
let V be non empty right_zeroed ModuleStr over K;

cluster V1() 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 b

( b

proof end;

registration

let K be Field;

let V be non trivial VectSp of K;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is homogeneous & not b_{1} is constant & not b_{1} is trivial )

end;
let V be non trivial VectSp of K;

cluster V1() 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 b

( b

proof end;

registration

let K be Field;

let V be non trivial VectSp of K;

for b_{1} being Functional of V st b_{1} is trivial holds

b_{1} is constant
;

end;
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 b

b

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 ;

ex b_{1} being V8() non trivial linear-Functional of V st

( b_{1} . v = 1_ K & b_{1} | the carrier of W = 0Functional W )

for b_{1}, b_{2} being V8() non trivial linear-Functional of V st b_{1} . v = 1_ K & b_{1} | the carrier of W = 0Functional W & b_{2} . v = 1_ K & b_{2} | the carrier of W = 0Functional W holds

b_{1} = b_{2}

end;
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 & it | the carrier of W = 0Functional W );

existence ( it . v = 1_ K & it | the carrier of W = 0Functional W );

ex b

( b

proof end;

uniqueness for b

b

proof 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 b_{5} being V8() non trivial linear-Functional of V holds

( b_{5} = coeffFunctional (v,W) iff ( b_{5} . v = 1_ K & b_{5} | the carrier of W = 0Functional W ) );

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 b

( b

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 & f . v <> 0. K )

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 & f . v <> 0. K )

proof end;

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

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 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 & w in W holds

(coeffFunctional (v,W)) . w = 0. K

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: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 & w in W holds

(coeffFunctional (v,W)) . ((a * v) + w) = a

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:32

for K being non empty addLoopStr

for V being non empty ModuleStr over K

for f, g being Functional of V

for v being Vector of V holds (f - g) . v = (f . v) - (g . v)

for V being non empty ModuleStr over 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
end;

:: Kernel of Additive Functional and Subspace Generated by Kernel of

:: Linear Functional. Linear Functionals in Quotient Vector Space

:: generated by Additive Functional

:: Linear Functional. Linear Functionals in Quotient Vector Space

:: generated by Additive Functional

definition

let S be non empty 1-sorted ;

let Z be ZeroStr ;

let f be Function of S,Z;

coherence

{ v where v is Element of S : f . v = 0. Z } is Subset of S

end;
let Z be ZeroStr ;

let f be Function of S,Z;

coherence

{ v where v is Element of S : f . v = 0. Z } is Subset of S

proof end;

:: deftheorem defines ker VECTSP10:def 9 :

for S being non empty 1-sorted

for Z being ZeroStr

for f being Function of S,Z holds ker f = { v where v is Element of S : f . v = 0. Z } ;

for S being non empty 1-sorted

for Z being ZeroStr

for f being Function of S,Z holds ker f = { v where v is Element of S : f . v = 0. Z } ;

registration

let K be non empty right_zeroed addLoopStr ;

let V be non empty ModuleStr over K;

let f be 0-preserving Functional of V;

coherence

not ker f is empty

end;
let V be non empty ModuleStr over K;

let f be 0-preserving Functional of V;

coherence

not ker f is empty

proof end;

theorem Th33: :: VECTSP10:33

for K being non empty right_complementable add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K

for f being linear-Functional of V holds ker f is linearly-closed

for V being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over K

for f being linear-Functional of V holds ker f is linearly-closed

proof end;

definition
end;

:: deftheorem defines degenerated VECTSP10:def 10 :

for K being non empty ZeroStr

for V being non empty ModuleStr over K

for f being Functional of V holds

( f is degenerated iff ker f <> {(0. V)} );

for K being non empty ZeroStr

for V being non empty ModuleStr 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 ModuleStr over K;

for b_{1} being Functional of V st not b_{1} is degenerated & b_{1} is 0-preserving holds

not b_{1} is constant

end;
let V be non trivial ModuleStr 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 b

not b

proof 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 f be linear-Functional of V;

ex b_{1} being non empty strict Subspace of V st the carrier of b_{1} = ker f
by Th33, VECTSP_4:34;

uniqueness

for b_{1}, b_{2} being non empty strict Subspace of V st the carrier of b_{1} = ker f & the carrier of b_{2} = ker f holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
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 the carrier of it = ker f;

ex b

uniqueness

for b

b

:: deftheorem Def11 defines Ker VECTSP10:def 11 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for f being linear-Functional of V

for b_{4} being non empty strict Subspace of V holds

( b_{4} = Ker f iff the carrier of b_{4} = ker f );

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for f being linear-Functional of V

for b

( b

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;

let f be additive Functional of V;

assume A1: the carrier of W c= ker f ;

ex b_{1} 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

b_{1} . A = f . a

for b_{1}, b_{2} 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

b_{1} . A = f . a ) & ( for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b_{2} . A = f . a ) holds

b_{1} = b_{2}

end;
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 for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

it . A = f . a;

ex b

for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b

proof end;

uniqueness for b

for a being Vector of V st A = a + W holds

b

for a being Vector of V st A = a + W holds

b

b

proof end;

:: deftheorem Def12 defines QFunctional VECTSP10:def 12 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 b_{5} being additive Functional of (VectQuot (V,W)) holds

( b_{5} = QFunctional (f,W) iff for A being Vector of (VectQuot (V,W))

for a being Vector of V st A = a + W holds

b_{5} . A = f . a );

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 b

( b

for a being Vector of V st A = a + W holds

b

theorem Th34: :: VECTSP10:34

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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

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 right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;

let V be VectSp of K;

let f be linear-Functional of V;

coherence

QFunctional (f,(Ker f)) is linear-Functional of (VectQuot (V,(Ker f)));

end;
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 QFunctional (f,(Ker f));

coherence

QFunctional (f,(Ker f)) is linear-Functional of (VectQuot (V,(Ker f)));

proof end;

:: deftheorem defines CQFunctional VECTSP10:def 13 :

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr

for V being VectSp of K

for f being linear-Functional of V holds CQFunctional f = QFunctional (f,(Ker f));

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative 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 well-unital distributive associative 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

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 V8() linear-Functional of V;

coherence

not CQFunctional f is constant

end;
let V be non trivial VectSp of K;

let f be V8() linear-Functional of V;

coherence

not CQFunctional f is constant

proof end;

registration

let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ;

let V be VectSp of K;

let f be linear-Functional of V;

coherence

not CQFunctional f is degenerated

end;
let V be VectSp of K;

let f be linear-Functional of V;

coherence

not CQFunctional f is degenerated

proof end;