The abstract of the Mizar article:

Quotient Vector Spaces and Functionals

by

Jaroslaw Kotowicz

Received November 5, 2002

MML identifier: VECTSP10

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, VECTSP_1, ARYTM_1, HAHNBAN, FUNCT_1, GRCAT_1, UNIALG_1,
      BINOP_1, LATTICES, RELAT_1, HAHNBAN1, MCART_1, RLSUB_1, RLSUB_2,
      RLVECT_3, RLVECT_2, FUNCT_2, ALGSTR_2, REALSET1, BOOLE, SEQM_3, GROUP_6,
      SETFAM_1, ARYTM_3, VECTSP10;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, FUNCT_1,
      REALSET1, RLVECT_1, BINOP_1, RLVECT_2, VECTSP_1, RELSET_1, FUNCT_2,
      SEQM_3, FRAENKEL, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, HAHNBAN1;
 constructors DOMAIN_1, REALSET1, BINOP_1, RLVECT_2, VECTSP_5, VECTSP_6,
      VECTSP_7, SEQM_3, HAHNBAN1;
 clusters STRUCT_0, SUBSET_1, FUNCT_1, RELSET_1, VECTSP_1, HAHNBAN1, VECTSP_4,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin
::Auxiliary Facts about Double Loops and Vector Spaces

theorem :: VECTSP10:1
  for K be add-associative right_zeroed right_complementable
            left-distributive left_unital (non empty doubleLoopStr)
for a be Element of K holds (- 1_ K) * a = - a;

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

definition
 let K be non empty doubleLoopStr;
cluster StructVectSp(K) -> non empty;
end;

definition
 let K be Abelian (non empty doubleLoopStr);
cluster StructVectSp(K) -> Abelian;
end;

definition
 let K be add-associative (non empty doubleLoopStr);
cluster StructVectSp(K) -> add-associative;
end;

definition
 let K be right_zeroed (non empty doubleLoopStr);
cluster StructVectSp(K) -> right_zeroed;
end;

definition
 let K be right_complementable (non empty doubleLoopStr);
cluster StructVectSp(K) -> right_complementable;
end;

definition
 let K be associative left_unital distributive (non empty doubleLoopStr);
cluster StructVectSp(K) -> VectSp-like;
end;

definition
 let K be non degenerated (non empty doubleLoopStr);
cluster StructVectSp(K) -> non trivial;
end;

definition
 let K be non degenerated (non empty doubleLoopStr);
cluster non trivial (non empty VectSpStr over K);
end;

definition
 let K be add-associative right_zeroed right_complementable
         (non empty doubleLoopStr);
cluster add-associative right_zeroed right_complementable strict
         (non empty VectSpStr over K);
end;

definition
 let K be add-associative right_zeroed right_complementable associative
          left_unital distributive (non empty doubleLoopStr);
cluster add-associative right_zeroed right_complementable VectSp-like strict
        (non empty VectSpStr over K);
end;

definition
 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 VectSp-like
         strict non trivial (non empty VectSpStr over K);
end;

theorem :: VECTSP10:2
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 VectSp-like
        (non empty VectSpStr over K),
     v be Vector of V holds (0.K)*v = 0.V & a*(0.V) = 0.V;

theorem :: VECTSP10:3
  for K be add-associative right_zeroed right_complementable
      Abelian associative left_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;

theorem :: VECTSP10:4
for K be Field, V be VectSp of K
for x be set, v be Vector of V holds
x in Lin{v} iff ex a be Element of K st x =a*v;

theorem :: VECTSP10:5
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;

theorem :: VECTSP10:6
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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];

theorem :: VECTSP10:7
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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;

theorem :: VECTSP10:8
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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;

theorem :: VECTSP10:9
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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];

theorem :: VECTSP10:10
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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];

theorem :: VECTSP10:11
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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];

theorem :: VECTSP10:12
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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;

theorem :: VECTSP10:13
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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;

theorem :: VECTSP10:14
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};

theorem :: VECTSP10:15
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};

theorem :: VECTSP10:16
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];

theorem :: VECTSP10:17
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];

theorem :: VECTSP10:18
for K be add-associative right_zeroed right_complementable associative
          Abelian left_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];

theorem :: VECTSP10:19
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];

theorem :: VECTSP10:20
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];

theorem :: VECTSP10:21
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];

begin
:: Quotient Vector Space for non commutative Double Loop

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_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
:: VECTSP10:def 2
 {A where A is Coset of W: not contradiction};
end;

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_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
:: VECTSP10:def 3
 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;
end;

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_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
:: VECTSP10:def 4
 the carrier of W;
end;

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_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
:: VECTSP10:def 5
 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;
end;

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_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 VectSp-like (non empty VectSpStr over K) means
:: VECTSP10:def 6
  the carrier of it = CosetSet(V,W) &
  the add of it = addCoset(V,W) &
  the Zero of it = zeroCoset(V,W) &
  the lmult of it = lmultCoset(V,W);
end;

theorem :: VECTSP10:22
for K be add-associative right_zeroed right_complementable
    Abelian associative left_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);

theorem :: VECTSP10:23
for K be add-associative right_zeroed right_complementable
    Abelian associative left_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;

theorem :: VECTSP10:24
for K be add-associative right_zeroed right_complementable
    Abelian associative left_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);

theorem :: VECTSP10:25
  for K be add-associative right_zeroed right_complementable
    Abelian associative left_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);

theorem :: VECTSP10:26
  for K be add-associative right_zeroed right_complementable
    Abelian associative left_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;

theorem :: VECTSP10:27
  for K be add-associative right_zeroed right_complementable
    Abelian associative left_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;

begin
:: Auxiliary Facts about Functionals

theorem :: VECTSP10:28
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;

definition
 let K be right_zeroed (non empty LoopStr);
 let V be non empty VectSpStr over K;
cluster additive 0-preserving Functional of V;
end;

definition
 let K be add-associative right_zeroed right_complementable
      (non empty doubleLoopStr);
 let V be right_zeroed (non empty VectSpStr over K);
cluster additive -> 0-preserving Functional of V;
end;

definition
 let K be add-associative right_zeroed right_complementable associative
          left_unital distributive (non empty doubleLoopStr);
 let V be add-associative right_zeroed right_complementable VectSp-like
          (non empty VectSpStr over K);
cluster homogeneous -> 0-preserving Functional of V;
end;

definition
 let K be non empty ZeroStr;
 let V be non empty VectSpStr over K;
cluster 0Functional(V) -> constant;
end;

definition
 let K be non empty ZeroStr;
 let V be non empty VectSpStr over K;
cluster constant Functional of V;
end;

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

definition
 let K be add-associative right_zeroed right_complementable
          (non empty doubleLoopStr);
 let V be right_zeroed (non empty VectSpStr over K);
cluster constant additive 0-preserving Functional of V;
end;

definition
 let K be non empty 1-sorted;
 let V be non empty VectSpStr over K;
cluster non constant -> non trivial Functional of V;
end;

definition
 let K be Field;
 let V be non trivial VectSp of K;
cluster additive homogeneous non constant non trivial Functional of V;
end;

definition
 let K be Field;
 let V be non trivial VectSp of K;
cluster trivial -> constant Functional of V;
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  v <> 0.V;
func coeffFunctional(v,W) -> non constant non trivial linear-Functional of V
means
:: VECTSP10:def 8
it.v = 1_ K & it|the carrier of W = 0Functional(W);
end;

theorem :: VECTSP10:29
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;

theorem :: VECTSP10:30
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;

theorem :: VECTSP10:31
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;

theorem :: VECTSP10:32
  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;

theorem :: VECTSP10:33
  for K be non empty LoopStr
for V be non empty VectSpStr over K
for f,g be Functional of V, v be Vector of V holds (f-g).v = f.v - g.v;

definition
 let K be Field;
 let V be non trivial VectSp of K;
cluster V*' -> non trivial;
end;

begin
:: Kernel of Additive Functional and Subspace Generated by Kernel of
::  Linear Functional. Linear Functionals in Quotient Vector Space
::  generated by Additive Functional

definition
 let K be non empty ZeroStr;
 let V be non empty VectSpStr over K;
 let f be Functional of V;
func ker f -> Subset of V equals
:: VECTSP10:def 9
   {v where v is Vector of V : f.v = 0.K};
end;

definition
 let K be right_zeroed (non empty LoopStr);
 let V be non empty VectSpStr over K;
 let f be 0-preserving Functional of V;
cluster ker f -> non empty;
end;

theorem :: VECTSP10:34
for K be add-associative right_zeroed right_complementable
    associative left_unital distributive (non empty doubleLoopStr)
for V be add-associative right_zeroed right_complementable
         VectSp-like (non empty VectSpStr over K)
for f be linear-Functional of V holds ker f is lineary-closed;

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

definition
 let K be non degenerated (non empty doubleLoopStr);
 let V be non trivial (non empty VectSpStr over K);
cluster non degenerated 0-preserving -> non constant Functional of V;
end;

definition
 let K be add-associative right_zeroed right_complementable
       Abelian associative left_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
:: VECTSP10:def 11
     the carrier of it = ker f;
end;

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_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  the carrier of W c= ker f;
func
 QFunctional(f,W) -> additive Functional of VectQuot(V,W) means
:: VECTSP10:def 12
 for A be Vector of VectQuot(V,W), a be Vector of V
  st A = a+W holds it.A = f.a;
end;

theorem :: VECTSP10:35
for K be add-associative right_zeroed right_complementable
    Abelian associative left_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;

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_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
:: VECTSP10:def 13
  QFunctional(f,Ker f);
end;

theorem :: VECTSP10:36
for K be add-associative right_zeroed right_complementable
    Abelian associative left_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;

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

definition
 let K be add-associative right_zeroed right_complementable
    Abelian associative left_unital distributive (non empty doubleLoopStr);
 let V be VectSp of K;
 let f be linear-Functional of V;
cluster CQFunctional(f) -> non degenerated;
end;