The abstract of the Mizar article:

Operations on Subspaces in Real Unitary Space

by

Noboru Endou,

Takashi Mitsuishi, and

Yasunari Shidama

Received October 9, 2002

MML identifier: RUSUB_2

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, BINOP_1, FUNCT_1, ARYTM_1, RELAT_1, BHSP_1, BOOLE,
      RLSUB_1, RLSUB_2, TARSKI, MCART_1, LATTICES;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, STRUCT_0, FUNCT_1,
      BINOP_1, LATTICES, RELSET_1, REAL_1, DOMAIN_1, RLVECT_1, RLSUB_1, BHSP_1,
      RUSUB_1;
 constructors REAL_1, DOMAIN_1, RUSUB_1, BINOP_1, LATTICES, RLSUB_2, MEMBERED;
 clusters SUBSET_1, STRUCT_0, RELSET_1, BHSP_1, RUSUB_1, LATTICES, RLSUB_2,
      MEMBERED;
 requirements NUMERALS, SUBSET, BOOLE;


begin :: Definitions of sum and intersection of subspaces.

definition
let V be RealUnitarySpace, W1,W2 be Subspace of V;
func W1 + W2 -> strict Subspace of V means
:: RUSUB_2:def 1

     the carrier of it = {v + u where v,u is VECTOR of V: v in W1 & u in W2};
end;

definition
let V be RealUnitarySpace, W1,W2 be Subspace of V;
func W1 /\ W2 -> strict Subspace of V means
:: RUSUB_2:def 2

     the carrier of it = (the carrier of W1) /\ (the carrier of W2);
end;

begin :: Theorems of sum and intersection of subspaces.

theorem :: RUSUB_2:1
for V being RealUnitarySpace, W1,W2 being Subspace of V, x being set holds
 x in W1 + W2 iff
  (ex v1,v2 being VECTOR of V st v1 in W1 & v2 in W2 & x = v1 + v2);

theorem :: RUSUB_2:2
for V being RealUnitarySpace, W1,W2 being Subspace of V,
 v being VECTOR of V st
  v in W1 or v in W2 holds v in W1 + W2;

theorem :: RUSUB_2:3
for V being RealUnitarySpace, W1,W2 being Subspace of V,
 x being set holds
  x in W1 /\ W2 iff x in W1 & x in W2;

theorem :: RUSUB_2:4
  for V being RealUnitarySpace, W being strict Subspace of V holds
 W + W = W;

theorem :: RUSUB_2:5
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 W1 + W2 = W2 + W1;

theorem :: RUSUB_2:6
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V holds
 W1 + (W2 + W3) = (W1 + W2) + W3;

theorem :: RUSUB_2:7
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2;

theorem :: RUSUB_2:8
for V being RealUnitarySpace, W1 being Subspace of V,
 W2 being strict Subspace of V holds
  W1 is Subspace of W2 iff W1 + W2 = W2;

theorem :: RUSUB_2:9
for V being RealUnitarySpace, W being strict Subspace of V holds
 (0).V + W = W & W + (0).V = W;

theorem :: RUSUB_2:10
for V being RealUnitarySpace holds
 (0).V + (Omega).V = the UNITSTR of V &
  (Omega).V + (0).V = the UNITSTR of V;

theorem :: RUSUB_2:11
for V being RealUnitarySpace, W being Subspace of V holds
 (Omega).V + W = the UNITSTR of V &
  W + (Omega).V = the UNITSTR of V;

theorem :: RUSUB_2:12
  for V being strict RealUnitarySpace holds
 (Omega).V + (Omega).V = V;

theorem :: RUSUB_2:13
  for V being RealUnitarySpace, W being strict Subspace of V holds
 W /\ W = W;

theorem :: RUSUB_2:14
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 W1 /\ W2 = W2 /\ W1;

theorem :: RUSUB_2:15
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V holds
 W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;

theorem :: RUSUB_2:16
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2;

theorem :: RUSUB_2:17
for V being RealUnitarySpace, W2 being Subspace of V,
 W1 being strict Subspace of V holds
  W1 is Subspace of W2 iff W1 /\ W2 = W1;

theorem :: RUSUB_2:18
for V being RealUnitarySpace, W being Subspace of V holds
 (0).V /\ W = (0).V & W /\ (0).V = (0).V;

theorem :: RUSUB_2:19
  for V being RealUnitarySpace holds
 (0).V /\ (Omega).V = (0).V & (Omega).V /\ (0).V = (0).V;

theorem :: RUSUB_2:20
for V being RealUnitarySpace, W being strict Subspace of V holds
 (Omega).V /\ W = W & W /\ (Omega).V = W;

theorem :: RUSUB_2:21
  for V being strict RealUnitarySpace holds
 (Omega).V /\ (Omega).V = V;

theorem :: RUSUB_2:22
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 W1 /\ W2 is Subspace of W1 + W2;

theorem :: RUSUB_2:23
for V being RealUnitarySpace, W1 being Subspace of V,
 W2 being strict Subspace of V holds
  (W1 /\ W2) + W2 = W2;

theorem :: RUSUB_2:24
for V being RealUnitarySpace, W1 being Subspace of V,
 W2 being strict Subspace of V holds
  W2 /\ (W2 + W1) = W2;

theorem :: RUSUB_2:25
  for V being RealUnitarySpace, W1,W2,W3 being Subspace of V holds
 (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3);

theorem :: RUSUB_2:26
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st
 W1 is Subspace of W2 holds
  W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3);

theorem :: RUSUB_2:27
  for V being RealUnitarySpace, W1,W2,W3 being Subspace of V holds
 W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3);

theorem :: RUSUB_2:28
  for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st
 W1 is Subspace of W2 holds
  W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);

theorem :: RUSUB_2:29
for V being RealUnitarySpace, W1,W2,W3 being Subspace of V st
 W1 is strict Subspace of W3 holds
  W1 + (W2 /\ W3) = (W1 + W2) /\ W3;

theorem :: RUSUB_2:30
  for V being RealUnitarySpace, W1,W2 being strict Subspace of V holds
 W1 + W2 = W2 iff W1 /\ W2 = W1;

theorem :: RUSUB_2:31
  for V being RealUnitarySpace, W1 being Subspace of V,
 W2,W3 being strict Subspace of V holds
  W1 is Subspace of W2 implies W1 + W3 is Subspace of W2 + W3;

theorem :: RUSUB_2:32
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 (ex W being Subspace of V st the carrier of W
  = (the carrier of W1) \/ (the carrier of W2)) iff
   W1 is Subspace of W2 or W2 is Subspace of W1;

begin ::  Introduction of a set of subspaces of real unitary space.

definition let V be RealUnitarySpace;
func Subspaces(V) -> set means
:: RUSUB_2:def 3

  for x being set holds x in it iff x is strict Subspace of V;
end;

definition let V be RealUnitarySpace;
cluster Subspaces(V) -> non empty;
end;

theorem :: RUSUB_2:33
   for V being strict RealUnitarySpace holds
 V in Subspaces(V);

begin ::  Definition of the direct sum and linear complement of subspace

definition
let V be RealUnitarySpace;
let W1,W2 be Subspace of V;
 pred V is_the_direct_sum_of W1,W2 means
:: RUSUB_2:def 4
   the UNITSTR of V = W1 + W2 & W1 /\ W2 = (0).V;
end;

definition
let V be RealUnitarySpace; let W be Subspace of V;
mode Linear_Compl of W -> Subspace of V means
:: RUSUB_2:def 5

  V is_the_direct_sum_of it,W;
end;

definition
let V be RealUnitarySpace; let W be Subspace of V;
cluster strict Linear_Compl of W;
end;

theorem :: RUSUB_2:34
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1;

theorem :: RUSUB_2:35
for V being RealUnitarySpace, W being Subspace of V,
 L being Linear_Compl of W holds
  V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L;

begin
:: Theorems concerning the direct sum, linear complement
:: and coset of a subspace

theorem :: RUSUB_2:36
for V being RealUnitarySpace, W being Subspace of V,
 L being Linear_Compl of W holds
  W + L = the UNITSTR of V & L + W = the UNITSTR of V;

theorem :: RUSUB_2:37
for V being RealUnitarySpace, W being Subspace of V,
 L being Linear_Compl of W holds
  W /\ L = (0).V & L /\ W = (0).V;

theorem :: RUSUB_2:38
  for V being RealUnitarySpace, W1,W2 being Subspace of V st
 V is_the_direct_sum_of W1,W2 holds V is_the_direct_sum_of W2,W1;

theorem :: RUSUB_2:39
for V being RealUnitarySpace holds
 V is_the_direct_sum_of (0).V,(Omega).V &
  V is_the_direct_sum_of (Omega).V,(0).V;

theorem :: RUSUB_2:40
  for V being RealUnitarySpace, W being Subspace of V,
 L being Linear_Compl of W holds W is Linear_Compl of L;

theorem :: RUSUB_2:41
  for V being RealUnitarySpace holds
 (0).V is Linear_Compl of (Omega).V & (Omega).V is Linear_Compl of (0).V;

theorem :: RUSUB_2:42
for V being RealUnitarySpace, W1,W2 being Subspace of V,
 C1 being Coset of W1, C2 being Coset of W2 st
  C1 meets C2 holds C1 /\ C2 is Coset of W1 /\ W2;

theorem :: RUSUB_2:43
for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 V is_the_direct_sum_of W1,W2 iff
  for C1 being Coset of W1, C2 being Coset of W2
   ex v being VECTOR of V st C1 /\ C2 = {v};

begin :: Decomposition of a vector of real unitary space

theorem :: RUSUB_2:44
  for V being RealUnitarySpace, W1,W2 being Subspace of V holds
 W1 + W2 = the UNITSTR of V iff
  for v being VECTOR of V
   ex v1,v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2;

theorem :: RUSUB_2:45
for V being RealUnitarySpace, W1,W2 being Subspace of V,
 v,v1,v2,u1,u2 being VECTOR of V st
  V is_the_direct_sum_of W1,W2 & v = v1 + v2 &
   v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
    v1 = u1 & v2 = u2;

theorem :: RUSUB_2:46
  for V being RealUnitarySpace, W1,W2 being Subspace of V st
 V = W1 + W2 &
  (ex v being VECTOR of V st
   for v1,v2,u1,u2 being VECTOR of V st
    v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds
     v1 = u1 & v2 = u2) holds V is_the_direct_sum_of W1,W2;

definition
let V be RealUnitarySpace; let v be VECTOR of V;
let W1,W2 be Subspace of V;
assume  V is_the_direct_sum_of W1,W2;
 func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:] means
:: RUSUB_2:def 6

   v = it`1 + it`2 & it`1 in W1 & it`2 in W2;
end;

theorem :: RUSUB_2:47
for V being RealUnitarySpace, v being VECTOR of V,
 W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
  (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2;

theorem :: RUSUB_2:48
for V being RealUnitarySpace, v being VECTOR of V, W1,W2 being Subspace of V st
 V is_the_direct_sum_of W1,W2 holds (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1;

theorem :: RUSUB_2:49
  for V being RealUnitarySpace, W being Subspace of V,
    L being Linear_Compl of W, v being VECTOR of V,
    t being Element of [:the carrier of V, the carrier of V:] st
 t`1 + t`2 = v & t`1 in W & t`2 in L holds t = v |-- (W,L);

theorem :: RUSUB_2:50
  for V being RealUnitarySpace, W being Subspace of V,
    L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`1 + (v |-- (W,L))`2 = v;

theorem :: RUSUB_2:51
  for V being RealUnitarySpace, W being Subspace of V,
    L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`1 in W & (v |-- (W,L))`2 in L;

theorem :: RUSUB_2:52
  for V being RealUnitarySpace, W being Subspace of V,
    L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`1 = (v |-- (L,W))`2;

theorem :: RUSUB_2:53
  for V being RealUnitarySpace, W being Subspace of V,
    L being Linear_Compl of W, v being VECTOR of V holds
 (v |-- (W,L))`2 = (v |-- (L,W))`1;

begin :: Introduction of operations on set of subspaces

 definition let V be RealUnitarySpace;
func SubJoin(V) -> BinOp of Subspaces(V) means
:: RUSUB_2:def 7

  for A1,A2 being Element of Subspaces(V),
      W1,W2 being Subspace of V st
   A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2;
end;

 definition let V be RealUnitarySpace;
func SubMeet(V) -> BinOp of Subspaces(V) means
:: RUSUB_2:def 8

  for A1,A2 being Element of Subspaces(V),
      W1,W2 being Subspace of V st
    A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2;
end;

begin :: Theorems of functions SubJoin, SubMeet

theorem :: RUSUB_2:54
for V being RealUnitarySpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is Lattice;

definition let V be RealUnitarySpace;
  cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) -> Lattice-like;
end;

theorem :: RUSUB_2:55
for V being RealUnitarySpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is lower-bounded;

theorem :: RUSUB_2:56
for V being RealUnitarySpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is upper-bounded;

theorem :: RUSUB_2:57
for V being RealUnitarySpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is 01_Lattice;

theorem :: RUSUB_2:58
for V being RealUnitarySpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is modular;

theorem :: RUSUB_2:59
for V being RealUnitarySpace holds
 LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) is complemented;

definition let V be RealUnitarySpace;
  cluster LattStr (# Subspaces(V), SubJoin(V), SubMeet(V) #) ->
    lower-bounded upper-bounded modular complemented;
end;

theorem :: RUSUB_2:60
  for V being RealUnitarySpace,
    W1,W2,W3 being strict Subspace of V holds
 W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3;

begin :: Auxiliary theorems in real unitary space

theorem :: RUSUB_2:61
   for V being RealUnitarySpace, W being strict Subspace of V holds
 (for v being VECTOR of V holds v in W) implies W = the UNITSTR of V;

theorem :: RUSUB_2:62
  for V being RealUnitarySpace, W being Subspace of V,
 v being VECTOR of V holds ex C being Coset of W st v in C;

theorem :: RUSUB_2:63
  for V being RealUnitarySpace, W being Subspace of V,
 v being VECTOR of V, x being set holds
  x in v + W iff ex u being VECTOR of V st u in W & x = v + u;