:: Subspaces and Cosets of Subspace of Real Unitary Space
::  by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002-2021 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 BHSP_1, RLSUB_1, STRUCT_0, TARSKI, SUPINF_2, ALGSTR_0, REALSET1,
      RLVECT_1, RELAT_1, ZFMISC_1, NUMBERS, ARYTM_3, FUNCT_1, REAL_1, PROB_2,
      ARYTM_1, SUBSET_1, XBOOLE_0, BINOP_1, CARD_1, XXREAL_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ALGSTR_0, ORDINAL1,
      NUMBERS, XCMPLX_0, XREAL_0, MCART_1, RELAT_1, FUNCT_1, REAL_1, FUNCT_2,
      DOMAIN_1, BINOP_1, REALSET1, RLVECT_1, RLSUB_1, BHSP_1, XXREAL_0;
 constructors PARTFUN1, BINOP_1, XXREAL_0, REAL_1, REALSET1, RLSUB_1, BHSP_1,
      VALUED_1, RELSET_1, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, NUMBERS, MEMBERED,
      REALSET1, STRUCT_0, BHSP_1, VALUED_0, ALGSTR_0, XREAL_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Definition and Axioms of the Subspace of Real Unitary Space

definition
  let V be RealUnitarySpace;
  mode Subspace of V -> RealUnitarySpace means
:: RUSUB_1:def 1

    the carrier of it c= the
carrier of V & 0.it = 0.V & the addF of it = (the addF of V)||the carrier of it
& the Mult of it = (the Mult of V)|([:REAL, the carrier of it:]) & the scalar
    of it = (the scalar of V)||the carrier of it;
end;

theorem :: RUSUB_1:1
  for V being RealUnitarySpace, W1,W2 being Subspace of V, x being object
  st x in W1 & W1 is Subspace of W2 holds x in W2;

theorem :: RUSUB_1:2
  for V being RealUnitarySpace, W being Subspace of V, x being object
  st x in W holds x in V;

theorem :: RUSUB_1:3
  for V being RealUnitarySpace, W being Subspace of V, w being
  VECTOR of W holds w is VECTOR of V;

theorem :: RUSUB_1:4
  for V being RealUnitarySpace, W being Subspace of V holds 0.W = 0.V;

theorem :: RUSUB_1:5
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 = 0.W2;

theorem :: RUSUB_1:6
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V, w1,w2 being VECTOR of W st w1 = v & w2 = u holds w1 + w2 = v + u
;

theorem :: RUSUB_1:7
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V, w being VECTOR of W, a being Real st w = v
    holds a * w = a * v;

theorem :: RUSUB_1:8
  for V being RealUnitarySpace, W being Subspace of V, v1,v2 being
VECTOR of V, w1,w2 being VECTOR of W st w1 = v1 & w2 = v2 holds w1 .|. w2 = v1
  .|. v2;

theorem :: RUSUB_1:9
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V, w being VECTOR of W st w = v holds - v = - w;

theorem :: RUSUB_1:10
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V, w1,w2 being VECTOR of W st w1 = v & w2 = u holds w1 - w2 = v - u
;

theorem :: RUSUB_1:11
  for V being RealUnitarySpace, W being Subspace of V holds 0.V in W;

theorem :: RUSUB_1:12
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds 0.W1 in W2;

theorem :: RUSUB_1:13
  for V being RealUnitarySpace, W being Subspace of V holds 0.W in V;

theorem :: RUSUB_1:14
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V st u in W & v in W holds u + v in W;

theorem :: RUSUB_1:15
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V, a being Real st v in W holds a * v in W;

theorem :: RUSUB_1:16
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V st v in W holds - v in W;

theorem :: RUSUB_1:17
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V st u in W & v in W holds u - v in W;

theorem :: RUSUB_1:18
  for V being RealUnitarySpace, V1 being Subset of V, D being non
  empty set, d1 being Element of D, A being BinOp of D, M being Function of [:
REAL, D:], D, S being Function of [:D,D:],REAL st V1 = D & d1 = 0.V & A = (the
addF of V)||V1 & M = (the Mult of V) | [:REAL,V1:] & S = (the scalar of V)||V1
  holds UNITSTR (# D,d1,A,M,S #) is Subspace of V;

theorem :: RUSUB_1:19
  for V being RealUnitarySpace holds V is Subspace of V;

theorem :: RUSUB_1:20
  for V,X being strict RealUnitarySpace holds V is Subspace of X &
  X is Subspace of V implies V = X;

theorem :: RUSUB_1:21
  for V,X,Y being RealUnitarySpace st V is Subspace of X & X is
  Subspace of Y holds V is Subspace of Y;

theorem :: RUSUB_1:22
  for V being RealUnitarySpace, W1,W2 being Subspace of V st the
  carrier of W1 c= the carrier of W2 holds W1 is Subspace of W2;

theorem :: RUSUB_1:23
  for V being RealUnitarySpace, W1,W2 being Subspace of V st (for v
  being VECTOR of V st v in W1 holds v in W2) holds W1 is Subspace of W2;

registration
  let V be RealUnitarySpace;
  cluster strict for Subspace of V;
end;

theorem :: RUSUB_1:24
  for V being RealUnitarySpace, W1,W2 being strict Subspace of V
  st the carrier of W1 = the carrier of W2 holds W1 = W2;

theorem :: RUSUB_1:25
  for V being RealUnitarySpace, W1,W2 being strict Subspace of V
  st (for v being VECTOR of V holds v in W1 iff v in W2) holds W1 = W2;

theorem :: RUSUB_1:26
  for V being strict RealUnitarySpace, W being strict Subspace of V st
  the carrier of W = the carrier of V holds W = V;

theorem :: RUSUB_1:27
  for V being strict RealUnitarySpace, W being strict Subspace of V st (
  for v being VECTOR of V holds v in W iff v in V) holds W = V;

theorem :: RUSUB_1:28
  for V being RealUnitarySpace, W being Subspace of V, V1 being Subset
  of V st the carrier of W = V1 holds V1 is linearly-closed;

theorem :: RUSUB_1:29
  for V being RealUnitarySpace, V1 being Subset of V st V1 <> {} &
V1 is linearly-closed holds ex W being strict Subspace of V st V1 = the carrier
  of W;

begin

:: Definition of Zero Subspace and Improper Subspace of Real Unitary Space

definition
  let V being RealUnitarySpace;
  func (0).V -> strict Subspace of V means
:: RUSUB_1:def 2

  the carrier of it = {0.V};
end;

definition
  let V being RealUnitarySpace;
  func (Omega).V -> strict Subspace of V equals
:: RUSUB_1:def 3
  the UNITSTR of V;
end;

begin :: Theorems of Zero Subspace and Improper Subspace

theorem :: RUSUB_1:30
  for V being RealUnitarySpace, W being Subspace of V holds (0).W = (0).V;

theorem :: RUSUB_1:31
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1 = (0).W2
;

theorem :: RUSUB_1:32
  for V being RealUnitarySpace, W being Subspace of V holds (0).W is
  Subspace of V;

theorem :: RUSUB_1:33
  for V being RealUnitarySpace, W being Subspace of V holds (0).V is
  Subspace of W;

theorem :: RUSUB_1:34
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds (0).W1
  is Subspace of W2;

theorem :: RUSUB_1:35
  for V being strict RealUnitarySpace holds V is Subspace of (Omega).V;

begin :: The Cosets of Subspace of Real Unitary Space

definition
  let V be RealUnitarySpace, v be VECTOR of V, W be Subspace of V;
  func v + W -> Subset of V equals
:: RUSUB_1:def 4
  {v + u where u is VECTOR of V : u in W};
end;

definition
  let V be RealUnitarySpace;
  let W be Subspace of V;
  mode Coset of W -> Subset of V means
:: RUSUB_1:def 5

    ex v be VECTOR of V st it = v + W;
end;

begin :: Theorems of the Cosets

theorem :: RUSUB_1:36
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V holds 0.V in v + W iff v in W;

theorem :: RUSUB_1:37
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V holds v in v + W;

theorem :: RUSUB_1:38
  for V being RealUnitarySpace, W being Subspace of V holds 0.V + W =
  the carrier of W;

theorem :: RUSUB_1:39
  for V being RealUnitarySpace, v being VECTOR of V holds v + (0). V = {v};

theorem :: RUSUB_1:40
  for V being RealUnitarySpace, v being VECTOR of V holds v +
  (Omega).V = the carrier of V;

theorem :: RUSUB_1:41
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V holds 0.V in v + W iff v + W = the carrier of W;

theorem :: RUSUB_1:42
  for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of
  V holds v in W iff v + W = the carrier of W;

theorem :: RUSUB_1:43
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V, a being Real st v in W holds (a * v) + W = the carrier of W;

theorem :: RUSUB_1:44
  for V being RealUnitarySpace, W being Subspace of V, v being
VECTOR of V, a being Real st a <> 0 & (a * v) + W = the carrier of W holds v in
  W;

theorem :: RUSUB_1:45
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V holds v in W iff - v + W = the carrier of W;

theorem :: RUSUB_1:46
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V holds u in W iff v + W = (v + u) + W;

theorem :: RUSUB_1:47
  for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR
  of V holds u in W iff v + W = (v - u) + W;

theorem :: RUSUB_1:48
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V holds v in u + W iff u + W = v + W;

theorem :: RUSUB_1:49
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V holds v + W = (- v) + W iff v in W;

theorem :: RUSUB_1:50
  for V being RealUnitarySpace, W being Subspace of V, u,v1,v2
  being VECTOR of V st u in v1 + W & u in v2 + W holds v1 + W = v2 + W;

theorem :: RUSUB_1:51
  for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR
  of V st u in v + W & u in (- v) + W holds v in W;

theorem :: RUSUB_1:52
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V, a being Real st a <> 1 & a * v in v + W holds v in W;

theorem :: RUSUB_1:53
  for V being RealUnitarySpace, W being Subspace of V, v being
  VECTOR of V, a being Real st v in W holds a * v in v + W;

theorem :: RUSUB_1:54
  for V being RealUnitarySpace, W being Subspace of V, v being VECTOR of
  V holds - v in v + W iff v in W;

theorem :: RUSUB_1:55
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V holds u + v in v + W iff u in W;

theorem :: RUSUB_1:56
  for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR
  of V holds v - u in v + W iff u in W;

theorem :: RUSUB_1:57
  for V being RealUnitarySpace, W being Subspace of V, u,v being
  VECTOR of V holds u in v + W iff ex v1 being VECTOR of V st v1 in W & u = v +
  v1;

theorem :: RUSUB_1:58
  for V being RealUnitarySpace, W being Subspace of V, u,v being VECTOR
  of V holds u in v + W iff ex v1 being VECTOR of V st v1 in W & u = v - v1;

theorem :: RUSUB_1:59
  for V being RealUnitarySpace, W being Subspace of V, v1,v2 being
VECTOR of V holds (ex v being VECTOR of V st v1 in v + W & v2 in v + W) iff v1
  - v2 in W;

theorem :: RUSUB_1:60
  for V being RealUnitarySpace, W being Subspace of V, u,v being
VECTOR of V st v + W = u + W holds ex v1 being VECTOR of V st v1 in W & v + v1
  = u;

theorem :: RUSUB_1:61
  for V being RealUnitarySpace, W being Subspace of V, u,v being
VECTOR of V st v + W = u + W holds ex v1 being VECTOR of V st v1 in W & v - v1
  = u;

theorem :: RUSUB_1:62
  for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
  v being VECTOR of V holds v + W1 = v + W2 iff W1 = W2;

theorem :: RUSUB_1:63
  for V being RealUnitarySpace, W1,W2 being strict Subspace of V,
  u,v being VECTOR of V st v + W1 = u + W2 holds W1 = W2;

theorem :: RUSUB_1:64
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of
  W holds C is linearly-closed iff C = the carrier of W;

theorem :: RUSUB_1:65
  for V being RealUnitarySpace, W1,W2 being strict Subspace of V, C1
  being Coset of W1, C2 being Coset of W2 holds C1 = C2 implies W1 = W2;

theorem :: RUSUB_1:66
  for V being RealUnitarySpace, v being VECTOR of V holds {v} is Coset of (0).V
;

theorem :: RUSUB_1:67
  for V being RealUnitarySpace, V1 being Subset of V holds V1 is Coset
  of (0).V implies ex v being VECTOR of V st V1 = {v};

theorem :: RUSUB_1:68
  for V being RealUnitarySpace, W being Subspace of V holds the carrier
  of W is Coset of W;

theorem :: RUSUB_1:69
  for V being RealUnitarySpace holds the carrier of V is Coset of (Omega).V;

theorem :: RUSUB_1:70
  for V being RealUnitarySpace, V1 being Subset of V st V1 is Coset of
  (Omega).V holds V1 = the carrier of V;

theorem :: RUSUB_1:71
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of
  W holds 0.V in C iff C = the carrier of W;

theorem :: RUSUB_1:72
  for V being RealUnitarySpace, W being Subspace of V, C being
  Coset of W, u being VECTOR of V holds u in C iff C = u + W;

theorem :: RUSUB_1:73
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of
W, u,v being VECTOR of V st u in C & v in C holds ex v1 being VECTOR of V st v1
  in W & u + v1 = v;

theorem :: RUSUB_1:74
  for V being RealUnitarySpace, W being Subspace of V, C being Coset of
W, u,v being VECTOR of V st u in C & v in C holds ex v1 being VECTOR of V st v1
  in W & u - v1 = v;

theorem :: RUSUB_1:75
  for V being RealUnitarySpace, W being Subspace of V, v1,v2 being
VECTOR of V holds (ex C being Coset of W st v1 in C & v2 in C) iff v1 - v2 in W
;

theorem :: RUSUB_1:76
  for V being RealUnitarySpace, W being Subspace of V, u being VECTOR of
  V, B,C being Coset of W st u in B & u in C holds B = C;