HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  issh2 Unicode version

Theorem issh2 21618
Description: Subspace  H of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
issh2  |-  ( H  e.  SH  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  ( A. x  e.  H  A. y  e.  H  ( x  +h  y
)  e.  H  /\  A. x  e.  CC  A. y  e.  H  (
x  .h  y )  e.  H ) ) )
Distinct variable group:    x, y, H

Proof of Theorem issh2
StepHypRef Expression
1 issh 21617 . 2  |-  ( H  e.  SH  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  (
(  +h  " ( H  X.  H ) ) 
C_  H  /\  (  .h  " ( CC  X.  H ) )  C_  H ) ) )
2 ax-hfvadd 21410 . . . . . . 7  |-  +h  :
( ~H  X.  ~H )
--> ~H
3 ffun 5248 . . . . . . 7  |-  (  +h  : ( ~H  X.  ~H ) --> ~H  ->  Fun  +h  )
42, 3ax-mp 10 . . . . . 6  |-  Fun  +h
5 xpss12 4699 . . . . . . . 8  |-  ( ( H  C_  ~H  /\  H  C_ 
~H )  ->  ( H  X.  H )  C_  ( ~H  X.  ~H )
)
65anidms 629 . . . . . . 7  |-  ( H 
C_  ~H  ->  ( H  X.  H )  C_  ( ~H  X.  ~H )
)
72fdmi 5251 . . . . . . 7  |-  dom  +h  =  ( ~H  X.  ~H )
86, 7syl6sseqr 3146 . . . . . 6  |-  ( H 
C_  ~H  ->  ( H  X.  H )  C_  dom  +h  )
9 funimassov 5849 . . . . . 6  |-  ( ( Fun  +h  /\  ( H  X.  H )  C_  dom  +h  )  ->  (
(  +h  " ( H  X.  H ) ) 
C_  H  <->  A. x  e.  H  A. y  e.  H  ( x  +h  y )  e.  H
) )
104, 8, 9sylancr 647 . . . . 5  |-  ( H 
C_  ~H  ->  ( (  +h  " ( H  X.  H ) ) 
C_  H  <->  A. x  e.  H  A. y  e.  H  ( x  +h  y )  e.  H
) )
11 ax-hfvmul 21415 . . . . . . 7  |-  .h  :
( CC  X.  ~H )
--> ~H
12 ffun 5248 . . . . . . 7  |-  (  .h  : ( CC  X.  ~H ) --> ~H  ->  Fun  .h  )
1311, 12ax-mp 10 . . . . . 6  |-  Fun  .h
14 xpss2 4703 . . . . . . 7  |-  ( H 
C_  ~H  ->  ( CC 
X.  H )  C_  ( CC  X.  ~H )
)
1511fdmi 5251 . . . . . . 7  |-  dom  .h  =  ( CC  X.  ~H )
1614, 15syl6sseqr 3146 . . . . . 6  |-  ( H 
C_  ~H  ->  ( CC 
X.  H )  C_  dom  .h  )
17 funimassov 5849 . . . . . 6  |-  ( ( Fun  .h  /\  ( CC  X.  H )  C_  dom  .h  )  ->  (
(  .h  " ( CC  X.  H ) ) 
C_  H  <->  A. x  e.  CC  A. y  e.  H  ( x  .h  y )  e.  H
) )
1813, 16, 17sylancr 647 . . . . 5  |-  ( H 
C_  ~H  ->  ( (  .h  " ( CC 
X.  H ) ) 
C_  H  <->  A. x  e.  CC  A. y  e.  H  ( x  .h  y )  e.  H
) )
1910, 18anbi12d 694 . . . 4  |-  ( H 
C_  ~H  ->  ( ( (  +h  " ( H  X.  H ) ) 
C_  H  /\  (  .h  " ( CC  X.  H ) )  C_  H )  <->  ( A. x  e.  H  A. y  e.  H  (
x  +h  y )  e.  H  /\  A. x  e.  CC  A. y  e.  H  ( x  .h  y )  e.  H
) ) )
2019adantr 453 . . 3  |-  ( ( H  C_  ~H  /\  0h  e.  H )  ->  (
( (  +h  " ( H  X.  H ) ) 
C_  H  /\  (  .h  " ( CC  X.  H ) )  C_  H )  <->  ( A. x  e.  H  A. y  e.  H  (
x  +h  y )  e.  H  /\  A. x  e.  CC  A. y  e.  H  ( x  .h  y )  e.  H
) ) )
2120pm5.32i 621 . 2  |-  ( ( ( H  C_  ~H  /\ 
0h  e.  H )  /\  ( (  +h  " ( H  X.  H ) )  C_  H  /\  (  .h  "
( CC  X.  H
) )  C_  H
) )  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  ( A. x  e.  H  A. y  e.  H  ( x  +h  y
)  e.  H  /\  A. x  e.  CC  A. y  e.  H  (
x  .h  y )  e.  H ) ) )
221, 21bitri 242 1  |-  ( H  e.  SH  <->  ( ( H  C_  ~H  /\  0h  e.  H )  /\  ( A. x  e.  H  A. y  e.  H  ( x  +h  y
)  e.  H  /\  A. x  e.  CC  A. y  e.  H  (
x  .h  y )  e.  H ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    e. wcel 1621   A.wral 2509    C_ wss 3078    X. cxp 4578   dom cdm 4580   "cima 4583   Fun wfun 4586   -->wf 4588  (class class class)co 5710   CCcc 8615   ~Hchil 21329    +h cva 21330    .h csm 21331   0hc0v 21334   SHcsh 21338
This theorem is referenced by:  shaddcl  21626  shmulcl  21627  shmulclOLD  21628  issh3  21629  helch  21653  hsn0elch  21657  hhshsslem2  21675  ocsh  21692  shscli  21726  shintcli  21738  imaelshi  22468
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403  ax-hilex 21409  ax-hfvadd 21410  ax-hfvmul 21415
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-iun 3805  df-br 3921  df-opab 3975  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-fv 4608  df-ov 5713  df-sh 21616
  Copyright terms: Public domain W3C validator