Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

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

Back to top