:: Quotient Vector Spaces and Functionals
:: by Jaros{\l}aw Kotowicz
::
:: Received November 5, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ALGSTR_0, STRUCT_0, VECTSP_1, SUPINF_2, XBOOLE_0, RLVECT_1,
SUBSET_1, ARYTM_3, BINOP_1, LATTICES, FUNCT_1, RELAT_1, MESFUNC1,
ZFMISC_1, RLSUB_1, RLVECT_3, RLVECT_2, CARD_3, FUNCT_2, TARSKI, ARYTM_1,
RLSUB_2, FINSEQ_4, MCART_1, GROUP_1, SETFAM_1, HAHNBAN, MSSUBFAM,
UNIALG_1, HAHNBAN1, GROUP_6, VECTSP10;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, DOMAIN_1, RELSET_1,
FUNCT_2, STRUCT_0, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1,
VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, GRCAT_1, HAHNBAN1;
constructors REALSET2, VECTSP_5, VECTSP_6, VECTSP_7, HAHNBAN1, RELSET_1,
GRCAT_1;
registrations SUBSET_1, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_4,
HAHNBAN1, ALGSTR_0, FUNCT_2, RELAT_1, ZFMISC_1, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions HAHNBAN1, TARSKI, XBOOLE_0, VECTSP_4, VECTSP_5, RLVECT_1, FUNCT_1,
ALGSTR_0, VECTSP_1;
equalities HAHNBAN1, XBOOLE_0, VECTSP_4, STRUCT_0, ALGSTR_0, VECTSP_1;
expansions HAHNBAN1, TARSKI, XBOOLE_0, VECTSP_5, RLVECT_1, FUNCT_1, STRUCT_0,
VECTSP_1;
theorems XBOOLE_1, FUNCT_2, HAHNBAN1, VECTSP_1, RLVECT_1, MCART_1, VECTSP_5,
VECTSP_4, VECTSP_6, VECTSP_7, TARSKI, FUNCT_1, XBOOLE_0, ZFMISC_1,
BINOP_1, GROUP_1, STRUCT_0, ALGSTR_0, XTUPLE_0;
schemes FUNCT_2, BINOP_1;
begin
::Auxiliary Facts about Double Loops and Vector Spaces
definition
let K be doubleLoopStr;
func StructVectSp(K) -> strict ModuleStr over K equals
ModuleStr (# the
carrier of K, the addF of K, 0.K, the multF of K#);
coherence;
end;
registration
let K be non empty doubleLoopStr;
cluster StructVectSp(K) -> non empty;
coherence;
end;
registration
let K be Abelian non empty doubleLoopStr;
cluster StructVectSp(K) -> Abelian;
coherence
proof
set V = StructVectSp(K);
now
let x,y be Vector of V;
reconsider x9=x,y9=y as Element of K;
thus x+y = y9+x9 by RLVECT_1:2
.= y+x;
end;
hence thesis;
end;
end;
registration
let K be add-associative non empty doubleLoopStr;
cluster StructVectSp(K) -> add-associative;
coherence
proof
set V = StructVectSp(K);
now
let x,y,z be Vector of V;
reconsider x9=x,y9=y,z9=z as Element of K;
thus (x+y)+z = (x9+y9)+z9 .= x9+(y9+z9) by RLVECT_1:def 3
.= x+(y+z);
end;
hence thesis;
end;
end;
registration
let K be right_zeroed non empty doubleLoopStr;
cluster StructVectSp(K) -> right_zeroed;
coherence
proof
set V = StructVectSp(K);
now
let x be Vector of V;
reconsider x9=x as Element of K;
thus x+0.V = x9+(0.K) .= x by RLVECT_1:def 4;
end;
hence thesis;
end;
end;
registration
let K be right_complementable non empty doubleLoopStr;
cluster StructVectSp(K) -> right_complementable;
coherence
proof
set V = StructVectSp(K);
let x be Vector of V;
reconsider x9=x as Element of K;
consider t be Element of K such that
A1: x9 + t = 0.K by ALGSTR_0:def 11;
reconsider t9 = t as Vector of V;
take t9;
thus thesis by A1;
end;
end;
registration
let K be associative left_unital distributive non empty doubleLoopStr;
cluster StructVectSp(K) -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
set V = StructVectSp(K);
now
let x,y be Element of K;
let v,w be Vector of V;
reconsider v9 = v, w9 = w as Element of K;
thus x*(v+w) = x*(v9+w9)
.= x*v9+x*w9 by VECTSP_1:def 7
.= x*v+x*w;
thus (x+y)*v = (x+y)*v9
.= x*v9+y*v9 by VECTSP_1:def 7
.= x*v+y*v;
thus (x*y)*v = (x*y)*v9
.= x*(y*v9) by GROUP_1:def 3
.= (the lmult of V).(x,(y*v))
.= x*(y*v);
thus (1.K)*v = (1.K)*v9
.= v;
end;
hence thesis;
end;
end;
registration
let K be non degenerated non empty doubleLoopStr;
cluster StructVectSp(K) -> non trivial;
coherence;
end;
registration
let K be non degenerated non empty doubleLoopStr;
cluster non trivial for ModuleStr over K;
existence
proof
take StructVectSp(K);
thus thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
cluster add-associative right_zeroed right_complementable strict for
non empty
ModuleStr over K;
correctness
proof
take StructVectSp(K);
thus thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
left_unital distributive non empty doubleLoopStr;
cluster add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital strict
for non empty ModuleStr over K;
correctness
proof
take StructVectSp(K);
thus thesis;
end;
end;
registration
let K be Abelian add-associative right_zeroed right_complementable
associative left_unital distributive non degenerated non empty doubleLoopStr;
cluster Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital
strict
for non trivial ModuleStr over K;
existence
proof
take StructVectSp(K);
thus thesis;
end;
end;
theorem Th1:
for K be add-associative right_zeroed right_complementable
associative left_unital distributive non empty doubleLoopStr, a be Element of
K for V be add-associative right_zeroed right_complementable
vector-distributive
scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over K, v be Vector of V holds (0.K)*v = 0.V & a*(0.V) = 0.V
proof
let F be add-associative right_zeroed right_complementable associative
left_unital distributive non empty doubleLoopStr;
let x be Element of F;
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over F, v be Vector of V;
v+(0.F)*v = (1.F)*v + (0.F)*v by VECTSP_1:def 17
.= ((1.F)+(0.F))*v by VECTSP_1:def 15
.= (1.F)*v by RLVECT_1:4
.= v by VECTSP_1:def 17
.= v+0.V by RLVECT_1:4;
hence
A1: (0.F)*v = 0.V by RLVECT_1:8;
hence x*(0.V) = (x*(0.F))*v by VECTSP_1:def 16
.= 0.V by A1;
end;
theorem
for K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr for V be VectSp
of K for S, T be Subspace of V, v be Vector of V st S /\ T = (0).V & v in S & v
in T holds v = 0.V
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K, S, T be Subspace of V, v be Vector of V;
assume that
A1: S /\ T = (0).V and
A2: v in S & v in T;
v in the carrier of S & v in the carrier of T by A2;
then v in (the carrier of S) /\ (the carrier of T) by XBOOLE_0:def 4;
then v in the carrier of (S /\ T) by VECTSP_5:def 2;
then v in {0.V} by A1,VECTSP_4:def 3;
hence thesis by TARSKI:def 1;
end;
theorem Th3:
for K be Field, V be VectSp of K for x be object, v be Vector of V
holds x in Lin{v} iff ex a be Element of K st x =a*v
proof
let K be Field, V be VectSp of K, x be object, v be Vector of V;
thus x in Lin{v} implies ex a be Element of K st x = a * v
proof
assume x in Lin{v};
then consider l be Linear_Combination of {v} such that
A1: x = Sum(l) by VECTSP_7:7;
Sum(l) = l.v * v by VECTSP_6:17;
hence thesis by A1;
end;
given a be Element of K such that
A2: x = a * v;
deffunc F(set) = 0.K;
consider f be Function of the carrier of V, the carrier of K such that
A3: f.v = a and
A4: for z be Vector of V st z <> v holds f.z = F(z) from FUNCT_2:sch 6;
reconsider f as Element of Funcs(the carrier of V,the carrier of K) by
FUNCT_2:8;
now
let z be Vector of V;
assume not z in {v};
then z <> v by TARSKI:def 1;
hence f.z = 0.K by A4;
end;
then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
Carrier f c= {v}
proof
let x be object;
assume
A5: x in Carrier f;
then f.x <> 0.K by VECTSP_6:2;
then x = v by A4,A5;
hence thesis by TARSKI:def 1;
end;
then reconsider f as Linear_Combination of {v} by VECTSP_6:def 4;
Sum(f) = x by A2,A3,VECTSP_6:17;
hence thesis by VECTSP_7:7;
end;
theorem Th4:
for K be Field, V be VectSp of K, v be Vector of V, a,b be Scalar
of V st v <> 0.V & a * v = b * v holds a = b
proof
let K be Field, V be VectSp of K, v be Vector of V, a,b be Scalar of V such
that
A1: v <> 0.V and
A2: a * v = b * v;
a*v - b*v = 0.V by A2,VECTSP_1:19;
then (a-b)*v = 0.V by VECTSP_4:82;
then a-b = 0.K by A1,VECTSP_1:15;
hence thesis by VECTSP_1:19;
end;
theorem Th5:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1
,v2 be Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds v |-- (W1,W2) = [
v1,v2]
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let W1,W2 be Subspace of V;
assume
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be Vector of V;
[v1,v2]`1 = v1 & [v1,v2]`2 = v2;
hence thesis by A1,VECTSP_5:def 6;
end;
theorem Th6:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1
,v2 be Vector of V st v |-- (W1,W2) = [v1,v2] holds v = v1 + v2
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be Vector of V;
assume v |-- (W1,W2) = [v1,v2];
then (v |-- (W1,W2))`1 = v1 & (v |-- (W1,W2))`2 = v2;
hence thesis by A1,VECTSP_5:def 6;
end;
theorem Th7:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1
,v2 be Vector of V st v |-- (W1,W2) = [v1,v2] holds v1 in W1 & v2 in W2
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be Vector of V;
assume v |-- (W1,W2) = [v1,v2];
then (v |-- (W1,W2))`1 = v1 & (v |-- (W1,W2))`2 = v2;
hence thesis by A1,VECTSP_5:def 6;
end;
theorem Th8:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v,v1
,v2 be Vector of V st v |-- (W1,W2) = [v1,v2] holds v |-- (W2,W1) = [v2,v1]
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let W1,W2 be Subspace of V;
assume
A1: V is_the_direct_sum_of W1,W2;
let v,v1,v2 be Vector of V;
assume
A2: v |-- (W1,W2) = [v1,v2];
then
A3: (v |-- (W1,W2))`1 = v1;
then
A4: v1 in W1 by A1,VECTSP_5:def 6;
A5: (v |-- (W1,W2))`2 = v2 by A2;
then
A6: v2 in W2 by A1,VECTSP_5:def 6;
v = v2 + v1 by A1,A3,A5,VECTSP_5:def 6;
hence thesis by A1,A4,A6,Th5,VECTSP_5:41;
end;
theorem Th9:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v be
Vector of V st v in W1 holds v |-- (W1,W2) = [v,0.V]
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let W1,W2 be Subspace of V such that
A1: V is_the_direct_sum_of W1,W2;
let v be Vector of V such that
A2: v in W1;
0.V in W2 & v + 0.V = v by RLVECT_1:4,VECTSP_4:17;
hence thesis by A1,A2,Th5;
end;
theorem Th10:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for W1,W2 be Subspace of V st V is_the_direct_sum_of W1,W2 for v be
Vector of V st v in W2 holds v |-- (W1,W2) = [0.V,v]
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let W1,W2 be Subspace of V;
assume
A1: V is_the_direct_sum_of W1,W2;
let v be Vector of V;
assume v in W2;
then v |-- (W2,W1) = [v,0.V] by A1,Th9,VECTSP_5:41;
hence thesis by A1,Th8,VECTSP_5:41;
end;
theorem Th11:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for V1 be Subspace of V, W1 be Subspace of V1, v be Vector of V st
v in W1 holds v is Vector of V1
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let V1 be Subspace of V, W1 be Subspace of V1, v be Vector of V;
assume v in W1;
then the carrier of W1 c= the carrier of V1 & v in the carrier of W1 by
VECTSP_4:def 2;
hence thesis;
end;
theorem Th12:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr for V be
VectSp of K for V1,V2,W be Subspace of V, W1,W2 be Subspace of W st W1 = V1 &
W2 = V2 holds W1 + W2 = V1 + V2
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let V1,V2,W be Subspace of V, W1,W2 be Subspace of W such that
A1: W1 = V1 & W2 = V2;
reconsider W3 = W1 + W2 as Subspace of V by VECTSP_4:26;
now
let v be Vector of V;
A2: the carrier of W1 c= the carrier of W & the carrier of W2 c= the
carrier of W by VECTSP_4:def 2;
hereby
assume
A3: v in W3;
then reconsider w = v as Vector of W by Th11;
consider w1,w2 be Vector of W such that
A4: w1 in W1 & w2 in W2 and
A5: w = w1 + w2 by A3,VECTSP_5:1;
reconsider v1 = w1, v2 = w2 as Vector of V by VECTSP_4:10;
v = v1 + v2 by A5,VECTSP_4:13;
hence v in V1 + V2 by A1,A4,VECTSP_5:1;
end;
assume v in V1 + V2;
then consider v1,v2 be Vector of V such that
A6: v1 in V1 & v2 in V2 and
A7: v = v1 + v2 by VECTSP_5:1;
v1 in the carrier of W1 & v2 in the carrier of W2 by A1,A6;
then reconsider w1 = v1, w2 = v2 as Vector of W by A2;
v = w1 + w2 by A7,VECTSP_4:13;
hence v in W3 by A1,A6,VECTSP_5:1;
end;
hence thesis by VECTSP_4:30;
end;
theorem Th13:
for K be Field, V be VectSp of K, W be Subspace of V for v be
Vector of V, w be Vector of W st v = w holds Lin{w} = Lin{v}
proof
let K be Field, V be VectSp of K, W be Subspace of V, v be Vector of V, w be
Vector of W such that
A1: v = w;
reconsider W1 = Lin{w} as Subspace of V by VECTSP_4:26;
now
let u be Vector of V;
hereby
assume u in W1;
then consider a be Element of K such that
A2: u = a * w by Th3;
u = a * v by A1,A2,VECTSP_4:14;
hence u in Lin{v} by Th3;
end;
assume u in Lin{v};
then consider a be Element of K such that
A3: u = a * v by Th3;
u = a * w by A1,A3,VECTSP_4:14;
hence u in W1 by Th3;
end;
hence thesis by VECTSP_4:30;
end;
theorem Th14:
for K be Field, V be VectSp of K for v be Vector of V, X be
Subspace of V st not v in X for y be Vector of X + Lin{v}, W be Subspace of X +
Lin{v} st v = y & W = X holds X + Lin{v} is_the_direct_sum_of W,Lin{y}
proof
let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V such
that
A1: not v in X;
let y be Vector of X + Lin{v}, W be Subspace of X + Lin{v};
assume that
A2: v = y and
A3: W = X;
Lin{v} = Lin{y} by A2,Th13;
hence the ModuleStr of X + Lin{v} = W + Lin{y} by A3,Th12;
assume W /\ Lin{y} <> (0).(X + Lin{v});
then consider z be Vector of X + Lin{v} such that
A4: not(z in W /\ Lin{y} iff z in (0).(X + Lin{v})) by VECTSP_4:30;
per cases by A4;
suppose that
A5: z in W /\ Lin{y} and
A6: not z in (0).(X + Lin{v});
z in Lin{y} by A5,VECTSP_5:3;
then consider a be Element of K such that
A7: z = a * y by Th3;
A8: z in W by A5,VECTSP_5:3;
now
per cases;
suppose
a = 0.K;
then z = 0.(X + Lin{v}) by A7,VECTSP_1:15;
hence contradiction by A6,VECTSP_4:17;
end;
suppose
A9: a <> 0.K;
y = (1_K)*y
.= a"*a*y by A9,VECTSP_1:def 10
.= a"*(a*y) by VECTSP_1:def 16;
hence contradiction by A1,A2,A3,A8,A7,VECTSP_4:21;
end;
end;
hence contradiction;
end;
suppose that
A10: not z in W /\ Lin{y} and
A11: z in (0).(X + Lin{v});
z = 0.(X + Lin{v}) by A11,VECTSP_4:35;
hence contradiction by A10,VECTSP_4:17;
end;
end;
theorem Th15:
for K be Field, V be VectSp of K, v be Vector of V, X be
Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y
& X = W & not v in X holds y |-- (W,Lin{y}) = [0.W,y]
proof
let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be
Vector of X + Lin{v}, W be Subspace of X + Lin{v};
assume v = y & X = W & not v in X;
then y in {y} & X + Lin{v} is_the_direct_sum_of W,Lin{y} by Th14,TARSKI:def 1
;
then y |-- (W,Lin{y}) = [0.(X + Lin{v}),y] by Th10,VECTSP_7:8;
hence thesis by VECTSP_4:11;
end;
theorem Th16:
for K be Field, V be VectSp of K, v be Vector of V, X be
Subspace of V for y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v =
y & X = W & not v in X for w be Vector of X + Lin{v} st w in X holds w |-- (W,
Lin{y}) = [w,0.V]
proof
let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be
Vector of X + Lin{v}, W be Subspace of X + Lin{v} such that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th14;
let w be Vector of X + Lin{v};
assume w in X;
then w |-- (W,Lin{y}) = [w,0.(X + Lin{v})] by A2,A4,Th9;
hence thesis by VECTSP_4:11;
end;
theorem Th17:
for K be add-associative right_zeroed right_complementable
associative Abelian well-unital distributive non empty doubleLoopStr, V be
VectSp of K for v be Vector of V, W1,W2 be Subspace of V ex v1,v2 be Vector of
V st v |-- (W1,W2) = [v1,v2]
proof
let K be add-associative right_zeroed right_complementable associative
Abelian well-unital distributive non empty doubleLoopStr, V be VectSp of K;
let v be Vector of V, W1,W2 be Subspace of V;
take (v |-- (W1,W2))`1,(v |-- (W1,W2))`2;
thus thesis by MCART_1:21;
end;
theorem Th18:
for K be Field, V be VectSp of K for v be Vector of V, X be
Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y
& X = W & not v in X for w be Vector of X + Lin{v} ex x be Vector of X, r be
Element of K st w |-- (W,Lin{y}) = [x,r*v]
proof
let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be
Vector of X + Lin{v}, W be Subspace of X + Lin{v} such that
A1: v = y and
A2: X = W and
A3: not v in X;
let w be Vector of X + Lin{v};
consider v1,v2 be Vector of X + Lin{v} such that
A4: w |-- (W,Lin{y}) = [v1,v2] by Th17;
A5: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th14;
then v1 in W by A4,Th7;
then reconsider x = v1 as Vector of X by A2;
v2 in Lin{y} by A5,A4,Th7;
then consider r be Element of K such that
A6: v2 = r * y by Th3;
take x,r;
thus thesis by A1,A4,A6,VECTSP_4:14;
end;
theorem Th19:
for K be Field, V be VectSp of K for v be Vector of V, X be
Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y
& X = W & not v in X for w1,w2 be Vector of X + Lin{v}, x1,x2 be Vector of X,
r1,r2 be 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
let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be
Vector of X + Lin{v}, W be Subspace of X + Lin{v};
assume that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th14;
let w1,w2 be Vector of X + Lin{v}, x1,x2 be Vector of X, r1,r2 be Element of
K such that
A5: w1 |-- (W,Lin{y}) = [x1,r1*v] and
A6: w2 |-- (W,Lin{y}) = [x2,r2*v];
reconsider y1 = x1, y2 = x2 as Vector of X + Lin{v} by A2,VECTSP_4:10;
A7: r2*v = r2*y by A1,VECTSP_4:14;
then
A8: y2 in W by A4,A6,Th7;
(r1+r2)*v = (r1+r2)*y by A1,VECTSP_4:14;
then
A9: (r1+r2)*v in Lin{y} by Th3;
reconsider z1 = x1, z2 = x2 as Vector of V by VECTSP_4:10;
A10: y1 + y2 = z1 + z2 by VECTSP_4:13
.= x1 + x2 by VECTSP_4:13;
A11: r1*v = r1*y by A1,VECTSP_4:14;
then y1 in W by A4,A5,Th7;
then
A12: y1 + y2 in W by A8,VECTSP_4:20;
A13: w2 = y2 + r2*y by A4,A6,A7,Th6;
w1 = y1 + r1*y by A4,A5,A11,Th6;
then
A14: w1 + w2 = y1 + r1*y + y2 + r2*y by A13,RLVECT_1:def 3
.= y1 + y2 + r1*y + r2*y by RLVECT_1:def 3
.= y1 + y2 + (r1*y + r2*y) by RLVECT_1:def 3
.= y1 + y2 + (r1+r2)*y by VECTSP_1:def 15;
(r1+r2)*y = (r1+r2)*v by A1,VECTSP_4:14;
hence thesis by A4,A12,A9,A14,A10,Th5;
end;
theorem Th20:
for K be Field, V be VectSp of K for v be Vector of V, X be
Subspace of V, y be Vector of X + Lin{v}, W be Subspace of X + Lin{v} st v = y
& X = W & not v in X for w be Vector of X + Lin{v}, x be Vector of X, t,r be
Element of K st w |-- (W,Lin{y}) = [x,r*v] holds t*w |-- (W,Lin{y}) = [t*x, t*r
*v]
proof
let K be Field, V be VectSp of K, v be Vector of V, X be Subspace of V, y be
Vector of X + Lin{v}, W be Subspace of X + Lin{v};
assume that
A1: v = y and
A2: X = W and
A3: not v in X;
A4: X + Lin{v} is_the_direct_sum_of W,Lin{y} by A1,A2,A3,Th14;
let w be Vector of X + Lin{v}, x be Vector of X, t,r be Element of K such
that
A5: w |-- (W,Lin{y}) = [x,r*v];
reconsider z = x as Vector of X + Lin{v} by A2,VECTSP_4:10;
r*y = r*v by A1,VECTSP_4:14;
then
A6: t*w = t*(z + r*y) by A4,A5,Th6
.= t*z + t*(r*y) by VECTSP_1:def 14
.= t*z + t*r*y by VECTSP_1:def 16;
reconsider u = x as Vector of V by VECTSP_4:10;
A7: t*r*y in Lin{y} by Th3;
A8: t*r*y = t*r*v by A1,VECTSP_4:14;
A9: t*z = t*u by VECTSP_4:14
.= t*x by VECTSP_4:14;
then t*z in W by A2;
hence thesis by A4,A9,A8,A7,A6,Th5;
end;
begin
:: Quotient Vector Space for non commutative Double Loop
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K;
let W be Subspace of V;
func CosetSet(V,W) ->non empty Subset-Family of V equals
the set of all A where A is Coset
of W;
correctness
proof
set C = the set of all A where A is Coset of W;
A1: C c= bool the carrier of V
proof
let x be object;
assume x in C;
then ex A be Coset of W st A = x;
hence thesis;
end;
the carrier of W is Coset of W by VECTSP_4:73;
then the carrier of W in C;
hence thesis by A1;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K;
let W be Subspace of V;
func addCoset(V,W) -> BinOp of CosetSet(V,W) means
:Def3:
for A,B be Element
of CosetSet(V,W) for a,b be Vector of V st A = a + W & B = b + W holds it.(A,B)
= (a+b)+W;
existence
proof
defpred P[set,set,set] means for a,b be Vector of V st $1 = a + W & $2 = b
+ W holds $3 = (a+b)+W;
set C = CosetSet(V,W);
A1: now
let A,B be Element of C;
A in C;
then consider A1 be Coset of W such that
A2: A1=A;
consider a be Vector of V such that
A3: A1 = a+W by VECTSP_4:def 6;
B in C;
then consider B1 be Coset of W such that
A4: B1=B;
consider b be Vector of V such that
A5: B1 = b+W by VECTSP_4:def 6;
reconsider z = (a+b) + W as Coset of W by VECTSP_4:def 6;
z in C;
then reconsider z as Element of C;
take z;
thus P[A,B,z]
proof
let a1,b1 be Vector of V;
assume that
A6: A = a1 + W and
A7: B = b1 + W;
a1 in a+W by A2,A3,A6,VECTSP_4:44;
then consider w1 be Vector of V such that
A8: w1 in W and
A9: a1 = a+w1 by VECTSP_4:42;
b1 in b +W by A4,A5,A7,VECTSP_4:44;
then consider w2 be Vector of V such that
A10: w2 in W and
A11: b1 = b+w2 by VECTSP_4:42;
A12: w1+w2 in W by A8,A10,VECTSP_4:20;
a1+b1 = w1+ a + b+ w2 by A9,A11,RLVECT_1:def 3
.= w1+ (a + b)+ w2 by RLVECT_1:def 3
.= a + b+ (w1+ w2) by RLVECT_1:def 3;
then
A13: a1+b1 in (a+b)+W by A12;
a1+b1 in (a1+b1) +W by VECTSP_4:44;
hence thesis by A13,VECTSP_4:56;
end;
end;
consider f be Function of [:C,C:],C such that
A14: for A,B be Element of C holds P[A,B, f.(A,B)] from BINOP_1:sch 3(
A1);
reconsider f as BinOp of C;
take f;
let A,B be Element of C;
let a,b be Vector of V;
assume A = a + W & B = b + W;
hence thesis by A14;
end;
uniqueness
proof
set C = CosetSet(V,W);
let f1,f2 be BinOp of CosetSet(V,W) such that
A15: for A,B be Element of CosetSet(V,W) for a,b be Vector of V st A =
a + W & B = b + W holds f1.(A,B) = (a+b) +W and
A16: for A,B be Element of CosetSet(V,W) for a,b be Vector of V st A =
a + W & B = b + W holds f2.(A,B) = (a+b) +W;
now
let A,B be Element of CosetSet(V,W);
A in C;
then consider A1 be Coset of W such that
A17: A1=A;
consider a be Vector of V such that
A18: A1 = a+W by VECTSP_4:def 6;
B in C;
then consider B1 be Coset of W such that
A19: B1=B;
consider b be Vector of V such that
A20: B1 = b+W by VECTSP_4:def 6;
thus f1.(A,B) = a+b + W by A15,A17,A19,A18,A20
.= f2.(A,B) by A16,A17,A19,A18,A20;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K;
let W be Subspace of V;
func zeroCoset(V,W) -> Element of CosetSet(V,W) equals
the carrier of W;
coherence
proof
the carrier of W = 0.V+W by VECTSP_4:45;
then the carrier of W is Coset of W by VECTSP_4:def 6;
then the carrier of W in CosetSet(V,W);
hence thesis;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K;
let W be Subspace of V;
func lmultCoset(V,W) -> Function of [:the carrier of K, CosetSet(V,W):],
CosetSet(V,W) means
:Def5:
for z be Element of K, A be Element of CosetSet(V,W)
for a be Vector of V st A = a+W holds it.(z,A) = z*a +W;
existence
proof
defpred P[Element of K, set, set] means for a be Vector of V st $2 = a + W
holds $3 = $1*a+W;
set cF = the carrier of K;
set C = CosetSet(V,W);
A1: now
let z be Element of K;
let A be Element of C;
A in C;
then consider A1 be Coset of W such that
A2: A1=A;
consider a be Vector of V such that
A3: A1 = a+W by VECTSP_4:def 6;
reconsider c = z*a + W as Coset of W by VECTSP_4:def 6;
c in C;
then reconsider c as Element of C;
take c;
thus P[z, A, c]
proof
let a1 be Vector of V;
assume A = a1 + W;
then a1 in a+W by A2,A3,VECTSP_4:44;
then consider w1 be Vector of V such that
A4: w1 in W & a1 = a+w1 by VECTSP_4:42;
z*a1 = z*a+z*w1 & z*w1 in W by A4,VECTSP_1:def 14,VECTSP_4:21;
then
A5: z*a1 in z*a+W;
z*a1 in z*a1 +W by VECTSP_4:44;
hence thesis by A5,VECTSP_4:56;
end;
end;
consider f be Function of [:cF,C:],C such that
A6: for z be Element of K for A be Element of C holds P[z,A, f.(z,A)]
from BINOP_1:sch 3(A1);
take f;
let z be Element of K, A be Element of C, a be Vector of V;
assume A = a + W;
hence thesis by A6;
end;
uniqueness
proof
set cF = the carrier of K;
set C = CosetSet(V,W);
let f1,f2 be Function of [:cF, C:], C such that
A7: for z be Element of K, A be Element of CosetSet(V,W) for a be
Vector of V st A = a + W holds f1.(z,A) = z*a + W and
A8: for z be Element of K, A be Element of CosetSet(V,W) for a be
Vector of V st A = a + W holds f2.(z,A) = z*a + W;
set C = CosetSet(V,W);
now
let z be Element of K;
let A be Element of CosetSet(V,W);
A in C;
then consider A1 be Coset of W such that
A9: A1=A;
consider a be Vector of V such that
A10: A1 = a+W by VECTSP_4:def 6;
thus f1.(z,A) = z*a + W by A7,A9,A10
.= f2.(z,A) by A8,A9,A10;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K;
let W be Subspace of V;
func VectQuot(V,W) -> strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over K means
:Def6:
the carrier of it = CosetSet(V,W) & the addF of it = addCoset(V,W) & 0.it =
zeroCoset(V,W) & the lmult of it = lmultCoset(V,W);
existence
proof
set C = CosetSet(V,W), aC = addCoset(V,W), zC = zeroCoset(V,W), lC =
lmultCoset(V,W), A = ModuleStr (# C, aC, zC, lC #);
A1: A is right_zeroed
proof
let A1 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A2: A1=aa;
consider a be Vector of V such that
A3: aa = a+W by VECTSP_4:def 6;
0.A = 0.V + W by VECTSP_4:45;
hence A1 + 0.A = (a+0.V) +W by A2,A3,Def3
.= A1 by A2,A3,RLVECT_1:4;
end;
A4: A is right_complementable
proof
let A1 be Element of A;
A5: 0.A = 0.V + W by VECTSP_4:45;
A1 in C;
then consider aa be Coset of W such that
A6: A1=aa;
consider a be Vector of V such that
A7: aa = a+W by VECTSP_4:def 6;
set A2 = -a+ W;
A2 is Coset of W by VECTSP_4:def 6;
then A2 in C;
then reconsider A2 as Element of A;
take A2;
thus A1 + A2 = (a+-a) +W by A6,A7,Def3
.= 0.A by A5,RLVECT_1:5;
end;
A8: now
let x,y be Element of K;
let A1,A2 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A9: A1=aa;
A2 in C;
then consider bb be Coset of W such that
A10: A2=bb;
consider b be Vector of V such that
A11: bb = b+W by VECTSP_4:def 6;
A12: lC.(x,A2) = x*A2 & lC.(x,A2) =x*b+W by A10,A11,Def5;
consider a be Vector of V such that
A13: aa = a+W by VECTSP_4:def 6;
A14: aC.(A1,A2) =a+b+W by A9,A10,A13,A11,Def3;
A15: lC.(x,A1) =x*a+W by A9,A13,Def5;
thus x*(A1+A2) = lC.(x,(the addF of A).(A1,A2))
.= x*(a+b) +W by A14,Def5
.= x*a+x*b +W by VECTSP_1:def 14
.= x*A1+x*A2 by A15,A12,Def3;
A16: lC.(y,A1) =y*a+W by A9,A13,Def5;
thus (x+y)*A1 = (the lmult of A).(x+y,A1)
.= (x+y)*a +W by A9,A13,Def5
.= x*a + y*a + W by VECTSP_1:def 15
.= x*A1+y*A1 by A15,A16,Def3;
thus (x*y)*A1 = (the lmult of A).(x*y,A1)
.= (x*y)*a +W by A9,A13,Def5
.= x*(y*a) +W by VECTSP_1:def 16
.= lC.(x,y*A1) by A16,Def5
.=x*(y*A1);
thus (1_K)*A1 = (the lmult of A).(1_K,A1)
.= 1_K*a +W by A9,A13,Def5
.= A1 by A9,A13;
end;
A17: A is Abelian
proof
let A1,A2 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A18: A1=aa;
consider a be Vector of V such that
A19: aa = a+W by VECTSP_4:def 6;
A2 in C;
then consider bb be Coset of W such that
A20: A2=bb;
consider b be Vector of V such that
A21: bb = b+W by VECTSP_4:def 6;
thus A1+A2 = (a+b) +W by A18,A20,A19,A21,Def3
.= A2+A1 by A18,A20,A19,A21,Def3;
end;
A is add-associative
proof
let A1,A2,A3 be Element of A;
A1 in C;
then consider aa be Coset of W such that
A22: A1=aa;
consider a be Vector of V such that
A23: aa = a+W by VECTSP_4:def 6;
A2 in C;
then consider bb be Coset of W such that
A24: A2=bb;
consider b be Vector of V such that
A25: bb = b+W by VECTSP_4:def 6;
A3 in C;
then consider cc be Coset of W such that
A26: A3=cc;
consider c be Vector of V such that
A27: cc = c+W by VECTSP_4:def 6;
A28: aC.(A2,A3) =b+c+W by A24,A26,A25,A27,Def3;
aC.(A1,A2) =a+b+W by A22,A24,A23,A25,Def3;
hence A1+A2 + A3 = a+b+c +W by A26,A27,Def3
.= a+(b+c) +W by RLVECT_1:def 3
.= A1+(A2+A3) by A22,A23,A28,Def3;
end;
then reconsider A as strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty ModuleStr over K by A17,A1,A4,A8
,VECTSP_1:def 14,def 15,def 16,def 17;
take A;
thus thesis;
end;
uniqueness;
end;
theorem Th21:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr, V be
VectSp of K, W be Subspace of V holds zeroCoset(V,W) = 0.V + W & 0.(VectQuot(V,
W)) = zeroCoset(V,W)
proof
let F be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of F;
let W be Subspace of V;
0.V = 0.W & 0.W in W by VECTSP_4:11;
hence zeroCoset(V,W) = 0.V + W by VECTSP_4:49;
thus thesis by Def6;
end;
theorem Th22:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V be
VectSp of K, W be Subspace of V, w be Vector of VectQuot(V,W) holds w is Coset
of W & ex v be Vector of V st w = v + W
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, W be Subspace of V, w be Vector of VectQuot(V,W);
set qv = VectQuot(V,W), cs = CosetSet(V,W);
cs = the carrier of qv by Def6;
then w in the set of all A where A is Coset of W;
then ex A be Coset of W st A= w;
hence thesis by VECTSP_4:def 6;
end;
theorem Th23:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V be
VectSp of K, W be Subspace of V, v be Vector of V holds v+W is Coset of W & v+W
is Vector of VectQuot(V,W)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, W be Subspace of V, v be Vector of V;
set cs = CosetSet(V,W);
thus v + W is Coset of W by VECTSP_4:def 6;
then v+W in cs;
hence thesis by Def6;
end;
theorem
for K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr for V be VectSp
of K, W be Subspace of V, A be Coset of W holds A is Vector of VectQuot(V,W)
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, W be Subspace of V, A be Coset of W;
set cs = CosetSet(V,W);
A in cs;
hence thesis by Def6;
end;
theorem
for K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, W be Subspace of V for A be Vector of VectQuot(V,W), v be Vector of V, a be
Scalar of V st A = v + W holds a*A = a*v + W
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, W be Subspace of V;
set vw = VectQuot(V,W), lm = the lmult of vw;
let A be Vector of vw, v be Vector of V, a be Scalar of V;
assume
A1: A = v + W;
A is Coset of W by Th22;
then A in the set of all B where B is Coset of W;
then reconsider w=A as Element of CosetSet(V,W);
thus a*A = lm.(a,A)
.= (lmultCoset(V,W)).(a,w) by Def6
.= a*v + W by A1,Def5;
end;
theorem
for K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, W be Subspace of V for A1,A2 be Vector of VectQuot(V,W), v1,v2 be Vector of
V st A1 = v1 + W & A2 = v2 + W holds A1 + A2 = v1 + v2 + W
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, W be Subspace of V;
set vw = VectQuot(V,W);
let A1,A2 be Vector of vw, v1,v2 be Vector of V;
assume
A1: A1 = v1 + W & A2 = v2 + W;
A2 is Coset of W by Th22;
then
A2: A2 in the set of all B where B is Coset of W;
A1 is Coset of W by Th22;
then A1 in the set of all B where B is Coset of W;
then reconsider w1=A1,w2=A2 as Element of CosetSet(V,W) by A2;
thus A1+A2 = (addCoset(V,W)).(w1,w2) by Def6
.= (v1 + v2) + W by A1,Def3;
end;
begin
:: Auxiliary Facts about Functionals
theorem Th27:
for K be Field, V be VectSp of K for X be Subspace of V, fi be
linear-Functional of X, v be Vector of V, y be Vector of X + Lin {v} st v = y &
not v in X for r be Element of K ex psi be linear-Functional of X + Lin{v} st
psi|the carrier of X=fi & psi.y = r
proof
let K be Field, V be VectSp of K, X be Subspace of V, fi be
linear-Functional of X, v be Vector of V, y be Vector of X + Lin{v};
assume that
A1: v = y and
A2: not v in X;
reconsider W1 = X as Subspace of X + Lin{v} by VECTSP_5:7;
let r be Element of K;
defpred P[Element of (X + Lin{v}), Element of K] means for x be Vector of X,
s be Element of K st ($1 |-- (W1,Lin{y}))`1 = x & ($1 |-- (W1,Lin{y}))`2 = s*v
holds $2 = fi.x + s*r;
A3: for e be Element of (X + Lin{v}) ex a be Element of K st P[e,a]
proof
let e be Element of (X + Lin{v});
consider x be Vector of X, s be Element of K such that
A4: e |-- (W1,Lin{y}) = [x,s*v] by A1,A2,Th18;
take fi.x + s*r;
let x9 be Vector of X, t be Element of K such that
A5: (e |-- (W1,Lin{y}))`1 = x9 and
A6: (e |-- (W1,Lin{y}))`2 = t*v;
v <> 0.V by A2,VECTSP_4:17;
then t = s by A4,A6,Th4;
hence thesis by A4,A5;
end;
consider f be Function of the carrier of X + Lin{v},the carrier of K such
that
A7: for e be Element of X + Lin{v} holds P[e,f.e] from FUNCT_2:sch 3(A3);
A8: now
let a be object;
assume a in dom fi;
then reconsider x = a as Vector of X;
X is Subspace of X + Lin{v} by VECTSP_5:7;
then the carrier of X c= the carrier of X + Lin{v} by VECTSP_4:def 2;
then reconsider v1 = x as Vector of X + Lin{v};
v1 in X;
then (v1 |-- (W1,Lin{y})) = [v1,0.V] by A1,A2,Th16
.= [v1,0.K*v] by Th1;
then
A9: ( v1 |-- (W1,Lin{y}))`1 = x & (v1 |-- (W1,Lin{y}))`2 = 0.K*v;
thus fi.a = fi.x + 0.K by RLVECT_1:4
.= fi.x + 0.K*r
.= f.a by A7,A9;
end;
reconsider f as Functional of X + Lin{v};
A10: y |-- (W1,Lin{y}) = [0.W1,y] by A1,A2,Th15;
then
A11: (y |-- (W1,Lin{y}))`1 = 0.X;
A12: f is additive
proof
let v1,v2 be Vector of X + Lin{v};
consider x1 be Vector of X, s1 be Element of K such that
A13: v1 |-- (W1,Lin{y}) = [x1,s1*v] by A1,A2,Th18;
A14: (v1 |-- (W1,Lin{y}))`1 = x1 & (v1 |-- (W1,Lin{y}))`2 = s1*v by A13;
consider x2 be Vector of X, s2 be Element of K such that
A15: v2 |-- (W1,Lin{y}) = [x2,s2*v] by A1,A2,Th18;
A16: (v2 |-- (W1,Lin{y}))`1 = x2 & (v2 |-- (W1,Lin{y}))`2 = s2*v by A15;
v1 + v2 |-- (W1,Lin{y}) = [x1 +x2,(s1+s2)*v] by A1,A2,A13,A15,Th19;
then
(v1 + v2 |-- (W1,Lin{y}))`1 = x1 + x2 & (v1 + v2 |-- (W1,Lin{y}))`2 =
(s1+ s2)*v;
hence f.(v1+v2) = fi.(x1 + x2) + (s1 + s2)*r by A7
.= fi.(x1 + x2) + (s1*r + s2*r) by VECTSP_1:def 3
.= fi.(x1) + fi.(x2) + (s1*r + s2*r) by VECTSP_1:def 20
.= fi.(x1) + fi.(x2) + s1*r + s2*r by RLVECT_1:def 3
.= fi.(x1) + s1*r + fi.(x2) + s2*r by RLVECT_1:def 3
.= fi.(x1) + s1*r + (fi.(x2) + s2*r) by RLVECT_1:def 3
.= f.v1 + (fi.(x2) + s2*r) by A7,A14
.= f.v1+f.v2 by A7,A16;
end;
f is homogeneous
proof
let v0 be Vector of X + Lin{v}, t be Element of K;
consider x0 be Vector of X, s0 be Element of K such that
A17: v0 |-- (W1,Lin{y}) = [x0,s0*v] by A1,A2,Th18;
A18: (v0 |-- (W1,Lin{y}))`1 = x0 & (v0 |-- (W1,Lin{y}))`2 = s0*v by A17;
t*v0 |-- (W1,Lin{y}) = [t*x0,t*s0*v] by A1,A2,A17,Th20;
then (t*v0 |-- (W1,Lin{y}))`1 = t*x0 & (t*v0 |-- (W1,Lin{y}))`2 = t*s0*v;
hence f.(t*v0) = fi.(t*x0) + t*s0*r by A7
.= t*(fi.x0) + t*s0*r by HAHNBAN1:def 8
.= t*(fi.x0) + t*(s0*r) by GROUP_1:def 3
.= t*(fi.x0 + s0*r) by VECTSP_1:def 2
.= t*f.v0 by A7,A18;
end;
then reconsider f as linear-Functional of X + Lin{v} by A12;
take f;
A19: dom fi = the carrier of X by FUNCT_2:def 1;
dom f = the carrier of X + Lin{v} & X is Subspace of X + Lin{v} by
FUNCT_2:def 1,VECTSP_5:7;
then dom fi c= dom f by A19,VECTSP_4:def 2;
then dom fi = dom f /\ the carrier of X by A19,XBOOLE_1:28;
hence f|the carrier of X=fi by A8,FUNCT_1:46;
(y |-- (W1,Lin{y}))`2 = y by A10
.= (1_K)*v by A1;
hence f.y = fi.(0.X) + (1_K)*r by A7,A11
.= 0.K + (1_K)*r by HAHNBAN1:def 9
.= 0.K + r
.= r by RLVECT_1:4;
end;
registration
let K be right_zeroed non empty addLoopStr;
let V be non empty ModuleStr over K;
cluster additive 0-preserving for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let V be right_zeroed non empty ModuleStr over K;
cluster additive -> 0-preserving for Functional of V;
coherence
proof
let f be Functional of V;
assume
A1: f is additive;
f.(0.V) = f.(0.V+0.V) by RLVECT_1:def 4
.= f.(0.V) + f.(0.V) by A1;
hence f.(0.V) = 0.K by RLVECT_1:9;
end;
end;
registration
let K be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let V be add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital non
empty ModuleStr over K;
cluster homogeneous -> 0-preserving for Functional of V;
coherence
proof
let f be Functional of V;
assume
A1: f is homogeneous;
thus f.(0.V) = f.(0.K * 0.V) by Th1
.= 0.K * f.(0.V) by A1
.= 0.K;
end;
end;
registration
let K be non empty ZeroStr;
let V be non empty ModuleStr over K;
cluster 0Functional(V) -> constant;
coherence
proof
let x,y be object;
set f = 0Functional(V);
assume x in dom f & y in dom f;
then reconsider v=x, w=y as Vector of V;
thus f.x = f.v .= 0.K by HAHNBAN1:14
.= f.w by HAHNBAN1:14
.= f.y;
end;
end;
registration
let K be non empty ZeroStr;
let V be non empty ModuleStr over K;
cluster constant for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
definition
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let V be right_zeroed non empty ModuleStr over K;
let f be 0-preserving Functional of V;
redefine attr f is constant means :: redefines constant (FUNCT_1, definition)
f = 0Functional(V);
compatibility
proof
A1: f.(0.V) = 0.K & the carrier of V = dom f by FUNCT_2:def 1,HAHNBAN1:def 9;
hereby
assume
A2: f is constant;
now
let v be Vector of V;
thus f.v = 0.K by A1,A2
.=(0Functional(V)).v by HAHNBAN1:14;
end;
hence f = 0Functional(V) by FUNCT_2:63;
end;
assume
A3: f = 0Functional(V);
now
let x,y be object;
assume x in dom f & y in dom f;
then reconsider v=x, w=y as Vector of V;
thus f.x = (0Functional(V)).v by A3
.= 0.K by HAHNBAN1:14
.= (0Functional(V)).w by HAHNBAN1:14
.= f.y by A3;
end;
hence thesis;
end;
end;
registration
let K be add-associative right_zeroed right_complementable non empty
doubleLoopStr;
let V be right_zeroed non empty ModuleStr over K;
cluster constant additive 0-preserving for Functional of V;
existence
proof
take 0Functional(V);
thus thesis;
end;
end;
registration
let K be Field;
let V be non trivial VectSp of K;
cluster additive homogeneous non constant non trivial for Functional of V;
existence
proof
consider v be Vector of V such that
A1: v <> 0.V by STRUCT_0:def 18;
set W = the Linear_Compl of Lin({v} qua Subset of V);
A2: V is_the_direct_sum_of W, Lin{v} by VECTSP_5:def 5;
then
A3: the ModuleStr of V = W + Lin{v};
then reconsider y = v as Vector of W+Lin{v};
A4: W /\ Lin{v} = (0).V by A2;
now
v in {v} by TARSKI:def 1;
then v in Lin{v} by VECTSP_7:8;
then
A5: v in the carrier of Lin{v};
assume v in W;
then v in the carrier of W;
then v in (the carrier of W)/\(the carrier of Lin{v}) by A5,
XBOOLE_0:def 4;
then v in the carrier of (W /\ Lin{v}) by VECTSP_5:def 2;
then v in {0.V} by A4,VECTSP_4:def 3;
hence contradiction by A1,TARSKI:def 1;
end;
then consider psi be linear-Functional of W + Lin{v} such that
psi|the carrier of W=0Functional(W) and
A6: psi.y = 1_K by Th27;
reconsider f = psi as Functional of V by A3;
take f;
thus f is additive
proof
let v1,v2 be Vector of V;
reconsider w1=v1, w2 =v2 as Vector of W +Lin{v} by A3;
v1+v2 = w1+w2 by A3;
hence thesis by VECTSP_1:def 20;
end;
thus f is homogeneous
proof
let v1 be Vector of V, a be Element of K;
reconsider w1=v1 as Vector of W +Lin{v} by A3;
a*v1 = (the lmult of (W+Lin{v})).(a,w1) by A3
.= a*w1;
hence thesis by HAHNBAN1:def 8;
end;
then reconsider f1=f as homogeneous Functional of V;
thus f is non constant
proof
A7: the carrier of V = dom f & f1.(0.V)=0.K by FUNCT_2:def 1,HAHNBAN1:def 9;
assume f is constant;
hence contradiction by A6,A7;
end;
thus f is non trivial
proof
set x = [v,1_K], y = [0.V, 0.K];
A8: the carrier of V = dom f by FUNCT_2:def 1;
then
A9: x in f by A6,FUNCT_1:1;
f1.(0.V)=0.K by HAHNBAN1:def 9;
then
A10: y in f by A8,FUNCT_1:1;
assume
A11: f is trivial;
per cases by A11,ZFMISC_1:131;
suppose
f = {};
hence contradiction;
end;
suppose
ex z be object st f = {z};
then consider z be object such that
A12: f = {z};
z = x & z = y by A9,A10,A12,TARSKI:def 1;
hence contradiction by XTUPLE_0:1;
end;
end;
end;
end;
registration :: uogolnic !!!
let K be Field;
let V be non trivial VectSp of K;
cluster trivial -> constant for Functional of V;
coherence;
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) -> non constant non trivial linear-Functional of V
means
:Def8:
it.v = 1_K & it|the carrier of W = 0Functional(W);
existence
proof
A2: V is_the_direct_sum_of W, Lin{v} by VECTSP_5:def 5;
then
A3: the ModuleStr of V = W + Lin{v};
then reconsider y = v as Vector of W+Lin{v};
A4: W /\ Lin{v} = (0).V by A2;
now
v in {v} by TARSKI:def 1;
then v in Lin{v} by VECTSP_7:8;
then
A5: v in the carrier of Lin{v};
assume v in W;
then v in the carrier of W;
then v in (the carrier of W)/\(the carrier of Lin{v}) by A5,
XBOOLE_0:def 4;
then v in the carrier of (W /\ Lin{v}) by VECTSP_5:def 2;
then v in {0.V} by A4,VECTSP_4:def 3;
hence contradiction by A1,TARSKI:def 1;
end;
then consider psi be linear-Functional of W + Lin{v} such that
A6: psi|the carrier of W=0Functional(W) and
A7: psi.y = 1_K by Th27;
reconsider f = psi as Functional of V by A3;
A8: f is additive
proof
let v1,v2 be Vector of V;
reconsider w1=v1, w2 =v2 as Vector of W +Lin{v} by A3;
v1+v2 = w1+w2 by A3;
hence thesis by VECTSP_1:def 20;
end;
f is homogeneous
proof
let v1 be Vector of V, a be Element of K;
reconsider w1=v1 as Vector of W +Lin{v} by A3;
a*v1 = (the lmult of (W+Lin{v})).(a,w1) by A3
.= a*w1;
hence thesis by HAHNBAN1:def 8;
end;
then reconsider f as linear-Functional of V by A8;
f is non constant
proof
A9: the carrier of V = dom f & f.(0.V)=0.K by FUNCT_2:def 1,HAHNBAN1:def 9;
assume f is constant;
hence contradiction by A7,A9;
end;
then reconsider f as non constant non trivial linear-Functional of V;
take f;
thus thesis by A6,A7;
end;
uniqueness
proof
let f1, f2 be non constant non trivial linear-Functional of V such that
A10: f1.v = 1_K and
A11: f1|the carrier of W = 0Functional(W) and
A12: f2.v = 1_K and
A13: f2|the carrier of W = 0Functional(W);
V is_the_direct_sum_of W, Lin{v} by VECTSP_5:def 5;
then
A14: the ModuleStr of V = W + Lin{v};
now
let w be Vector of V;
w in W+Lin{v} by A14;
then consider v1,v2 be Vector of V such that
A15: v1 in W and
A16: v2 in Lin{v} and
A17: w = v1 +v2 by VECTSP_5:1;
consider a be Element of K such that
A18: v2 = a* v by A16,Th3;
A19: v1 in the carrier of W by A15;
then
A20: f1.v1 = (f2|the carrier of W).v1 by A11,A13,FUNCT_1:49
.= f2.v1 by A19,FUNCT_1:49;
thus f1.w= f1.v1 + f1.(a*v) by A17,A18,VECTSP_1:def 20
.= f1.v1 + a* f1.v by HAHNBAN1:def 8
.= f1.v1 + f2.(a*v) by A10,A12,HAHNBAN1:def 8
.= f2.w by A17,A18,A20,VECTSP_1:def 20;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th28:
for K be Field, V be non trivial VectSp of K for f be non
constant 0-preserving Functional of V ex v be Vector of V st v <> 0.V & f.v <>
0.K
proof
let K be Field, V be non trivial VectSp of K, f be non constant 0-preserving
Functional of V;
A1: f.(0.V) =0.K by HAHNBAN1:def 9;
assume
A2: for v be Vector of V st v <> 0.V holds f.v = 0.K;
now
let x,y be object;
assume x in dom f & y in dom f;
then reconsider v=x,w=y as Vector of V;
thus f.x = f.v .= 0.K by A2,A1
.= f.w by A2,A1
.= f.y;
end;
hence contradiction by FUNCT_1:def 10;
end;
theorem Th29:
for K be Field, V be non trivial VectSp of K for v be Vector of
V, a be Scalar of V for W be Linear_Compl of Lin{v} st v <> 0.V holds (
coeffFunctional(v,W)).(a*v) = a
proof
let K be Field, V be non trivial VectSp of K, v be Vector of V, a be Scalar
of V, W be Linear_Compl of Lin{v};
assume
A1: v <> 0.V;
set cf = coeffFunctional(v,W);
thus cf.(a*v) = a*cf.v by HAHNBAN1:def 8
.= a*(1_K) by A1,Def8
.= a;
end;
theorem Th30:
for K be Field, V be non trivial VectSp of K for v,w be Vector
of V for W be Linear_Compl of Lin{v} st v <> 0.V & w in W holds (
coeffFunctional(v,W)).w = 0.K
proof
let K be Field, V be non trivial VectSp of K, v,w be Vector of V, W be
Linear_Compl of Lin{v};
assume that
A1: v <> 0.V and
A2: w in W;
set cf = coeffFunctional(v,W), cw = the carrier of W;
reconsider s = w as Vector of W by A2;
w in cw by A2;
hence cf.(w) = (cf|cw).w by FUNCT_1:49
.= (0Functional(W)).s by A1,Def8
.= 0.K by HAHNBAN1:14;
end;
theorem
for K be Field, V be non trivial VectSp of K for v,w be Vector of V, a
be Scalar of V for W be Linear_Compl of Lin{v} st v <> 0.V & w in W holds (
coeffFunctional(v,W)).(a*v+w) = a
proof
let K be Field, V be non trivial VectSp of K, v,w be Vector of V, a be
Scalar of V, W be Linear_Compl of Lin{v};
assume that
A1: v <> 0.V and
A2: w in W;
set cf = coeffFunctional(v,W);
thus cf.(a*v+w) = cf.(a*v)+cf.w by VECTSP_1:def 20
.= cf.(a*v) + 0.K by A1,A2,Th30
.= cf.(a*v) by RLVECT_1:def 4
.= a by A1,Th29;
end;
theorem
for K be non empty addLoopStr for V be non empty ModuleStr over K for
f,g be Functional of V, v be Vector of V holds (f-g).v = f.v - g.v
proof
let K be non empty addLoopStr;
let V be non empty ModuleStr over K;
let f,g be Functional of V, v be Vector of V;
thus (f-g).v = f.v + (-g).v by HAHNBAN1:def 3
.= f.v - g.v by HAHNBAN1:def 4;
end;
registration
let K be Field;
let V be non trivial VectSp of K;
cluster V*' -> non trivial;
coherence
proof
set g = the non constant linear-Functional of V;
A1: g <> 0Functional(V);
reconsider g as Element of (V*') by HAHNBAN1:def 10;
assume V*' is trivial;
then g = 0.(V*');
hence contradiction by A1,HAHNBAN1:def 10;
end;
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 S be non empty 1-sorted;
let Z be ZeroStr;
let f be Function of S,Z;
func ker f -> Subset of S equals
{v where v is Element of S : f.v = 0.Z};
coherence
proof
set A = {v where v is Element of S : f.v = 0.Z};
A c= the carrier of S
proof
let x be object;
assume x in A;
then ex v be Element of S st v = x & f.v = 0.Z;
hence thesis;
end;
hence thesis;
end;
end;
registration
let K be right_zeroed non empty addLoopStr;
let V be non empty ModuleStr over K;
let f be 0-preserving Functional of V;
cluster ker f -> non empty;
coherence
proof
f.(0.V) = 0.K by HAHNBAN1:def 9;
then 0.V in ker f;
hence thesis;
end;
end;
theorem Th33:
for K be add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr for V be
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital non empty
ModuleStr over K for f be linear-Functional of V holds
ker f is linearly-closed
proof
let F be add-associative right_zeroed right_complementable associative
well-unital distributive non empty doubleLoopStr;
let V be add-associative right_zeroed right_complementable
vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over F;
let f be linear-Functional of V;
set V1 = ker f;
thus for v,u be Vector of V st v in V1 & u in V1 holds v + u in V1
proof
let v,u be Vector of V;
assume v in V1 & u in V1;
then
(ex a be Vector of V st a = v & f.a= 0.F )& ex b be Vector of V st b =
u & f.b= 0.F;
then f.(v+u) = 0.F+0.F by VECTSP_1:def 20
.= 0.F by RLVECT_1:4;
hence thesis;
end;
let a be Element of F;
let v be Vector of V;
assume v in V1;
then ex w be Vector of V st w=v & f.w=0.F;
then f.(a*v) = a * 0.F by HAHNBAN1:def 8
.=0.F;
hence thesis;
end;
definition
let K be non empty ZeroStr;
let V be non empty ModuleStr over K;
let f be Functional of V;
attr f is degenerated means
ker f <> {0.V};
end;
registration
let K be non degenerated non empty doubleLoopStr;
let V be non trivial ModuleStr over K;
cluster non degenerated 0-preserving -> non constant for Functional of V;
coherence
proof
let f be Functional of V;
assume that
A1: f is non degenerated and
A2: f is 0-preserving and
A3: f is constant;
A4: f.(0.V) =0.K by A2;
A5: now
assume
A6: for v be Vector of V st v <> 0.V holds f.v = 0.K;
the carrier of V c= ker f
proof
let x be object;
assume x in the carrier of V;
then reconsider v=x as Vector of V;
per cases;
suppose
v = 0.V;
hence thesis by A4;
end;
suppose
v <> 0.V;
then f.v = 0.K by A6;
hence thesis;
end;
end;
then the carrier of V = ker f
.= {0.V} by A1;
hence contradiction;
end;
dom f = the carrier of V by FUNCT_2:def 1;
hence contradiction by A3,A4,A5;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K;
let f be linear-Functional of V;
func Ker f -> strict non empty Subspace of V means
:Def11:
the carrier of it = ker f;
existence by Th33,VECTSP_4:34;
uniqueness by VECTSP_4:29;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty 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:
for A be Vector of VectQuot(V,W), a be Vector of V st A = a+W holds it.A = f.a;
existence
proof
defpred P[set,set] means for a be Vector of V st $1 = a+W holds $2 = f.a;
set aC = addCoset(V,W);
set C = CosetSet(V,W);
set vq = VectQuot(V,W);
A2: now
let A be Vector of vq;
consider a be Vector of V such that
A3: A = a+W by Th22;
take y = f.a;
thus P[A, y]
proof
let a1 be Vector of V;
assume A = a1+W;
then a in a1+W by A3,VECTSP_4:44;
then consider w be Vector of V such that
A4: w in W and
A5: a = a1 + w by VECTSP_4:42;
w in the carrier of W by A4;
then w in ker f by A1;
then
A6: ex aa be Vector of V st aa=w & f.aa =0.K;
thus y = f.a1+f.w by A5,VECTSP_1:def 20
.= f.a1 by A6,RLVECT_1:def 4;
end;
end;
consider ff be Function of the carrier of vq, the carrier of K such that
A7: for A be Vector of vq holds P[A, ff.A] from FUNCT_2:sch 3(A2);
reconsider ff as Functional of vq;
A8: C = the carrier of vq by Def6;
now
A9: the addF of vq = addCoset(V,W) by Def6;
let A,B be Vector of vq;
consider a be Vector of V such that
A10: A = a+W by Th22;
consider b be Vector of V such that
A11: B = b+W by Th22;
aC.(A,B) =a+b+W by A8,A10,A11,Def3;
hence ff.(A+B) = f.(a+b) by A7,A9
.= f.a + f.b by VECTSP_1:def 20
.= ff.A + f.b by A7,A10
.= ff.A + ff.B by A7,A11;
end;
then reconsider ff as additive Functional of vq by VECTSP_1:def 20;
take ff;
thus thesis by A7;
end;
uniqueness
proof
set vq = VectQuot(V,W);
let f1,f2 be additive Functional of vq such that
A12: for A be Vector of VectQuot(V,W) for a be Vector of V st A = a+W
holds f1.A = f.a and
A13: for A be Vector of VectQuot(V,W) for a be Vector of V st A = a+W
holds f2.A = f.a;
now
let A be Vector of vq;
consider a be Vector of V such that
A14: A = a+W by Th22;
thus f1.A = f.a by A12,A14
.= f2.A by A13,A14;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th34:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V be
VectSp of K, W be Subspace of V for f be linear-Functional of V st the carrier
of W c= ker f holds QFunctional(f,W) is homogeneous
proof
let F be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of F;
let W be Subspace of V;
let f be linear-Functional of V;
set qf = QFunctional(f,W);
set vq = VectQuot(V,W);
assume
A1: the carrier of W c= ker f;
now
set C = CosetSet(V,W);
let A be Vector of vq;
let r be Scalar of vq;
A2: C = the carrier of vq by Def6;
then A in C;
then consider aa be Coset of W such that
A3: A = aa;
consider a be Vector of V such that
A4: aa = a+W by VECTSP_4:def 6;
r*A = (the lmult of vq).(r,A)
.= (lmultCoset(V,W)).(r,A) by Def6
.= r*a+ W by A2,A3,A4,Def5;
hence qf.(r*A) = f.(r*a) by A1,Def12
.= r*f.a by HAHNBAN1:def 8
.= r*(qf.A) by A1,A3,A4,Def12;
end;
hence thesis;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty 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
QFunctional(f,Ker f);
correctness
proof
the carrier of (Ker f) = ker f by Def11;
hence thesis by Th34;
end;
end;
theorem Th35:
for K be add-associative right_zeroed right_complementable
Abelian associative well-unital distributive non empty doubleLoopStr for V be
VectSp of K, f be linear-Functional of V for A be Vector of VectQuot(V,Ker f),
v be Vector of V st A = v+Ker f holds (CQFunctional(f)).A = f.v
proof
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr, V be VectSp of
K, f be linear-Functional of V;
let A be Vector of VectQuot(V,Ker f), v be Vector of V;
assume
A1: A = v+Ker f;
the carrier of (Ker f) = ker f by Def11;
hence thesis by A1,Def12;
end;
registration
let K be Field;
let V be non trivial VectSp of K;
let f be non constant linear-Functional of V;
cluster CQFunctional(f) -> non constant;
coherence
proof
set W = Ker f, qf = CQFunctional(f), qv = VectQuot(V,W);
consider v be Vector of V such that
v <> 0.V and
A1: f.v <> 0.K by Th28;
reconsider cv = v+W as Vector of qv by Th23;
assume qf is constant;
then qf = 0Functional(qv);
then 0.K = qf.cv by HAHNBAN1:14
.= f.v by Th35;
hence contradiction by A1;
end;
end;
registration
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr;
let V be VectSp of K;
let f be linear-Functional of V;
cluster CQFunctional(f) -> non degenerated;
coherence
proof
set qf = CQFunctional(f), W = Ker f, qV = VectQuot(V,W);
A1: the carrier of W = ker f by Def11;
A2: the carrier of qV = CosetSet(V,W) by Def6;
thus ker qf c= {0.qV}
proof
let x be object;
assume x in ker qf;
then consider w be Vector of qV such that
A3: x= w and
A4: qf.w=0.K;
w in CosetSet(V,W) by A2;
then consider A be Coset of W such that
A5: w = A;
consider v be Vector of V such that
A6: A = v + W by VECTSP_4:def 6;
f.v = 0.K by A1,A4,A5,A6,Def12;
then v in ker f;
then v in W by A1;
then w = zeroCoset(V,W) by A5,A6,VECTSP_4:49
.= 0.qV by Th21;
hence thesis by A3,TARSKI:def 1;
end;
thus {0.qV} c= ker qf
proof
let x be object;
assume x in {0.qV};
then
A7: x = 0.qV by TARSKI:def 1;
qf.(0.qV) = 0.K by HAHNBAN1:def 9;
hence thesis by A7;
end;
end;
end;