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

Theorem issh2 30956
Description: Subspace ๐ป 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 (๐ป โˆˆ Sโ„‹ โ†” ((๐ป โІ โ„‹ โˆง 0โ„Ž โˆˆ ๐ป) โˆง (โˆ€๐‘ฅ โˆˆ ๐ป โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ป โˆง โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ ยทโ„Ž ๐‘ฆ) โˆˆ ๐ป)))
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐ป

Proof of Theorem issh2
StepHypRef Expression
1 issh 30955 . 2 (๐ป โˆˆ Sโ„‹ โ†” ((๐ป โІ โ„‹ โˆง 0โ„Ž โˆˆ ๐ป) โˆง (( +โ„Ž โ€œ (๐ป ร— ๐ป)) โІ ๐ป โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— ๐ป)) โІ ๐ป)))
2 ax-hfvadd 30747 . . . . . . 7 +โ„Ž :( โ„‹ ร— โ„‹)โŸถ โ„‹
3 ffun 6711 . . . . . . 7 ( +โ„Ž :( โ„‹ ร— โ„‹)โŸถ โ„‹ โ†’ Fun +โ„Ž )
42, 3ax-mp 5 . . . . . 6 Fun +โ„Ž
5 xpss12 5682 . . . . . . . 8 ((๐ป โІ โ„‹ โˆง ๐ป โІ โ„‹) โ†’ (๐ป ร— ๐ป) โІ ( โ„‹ ร— โ„‹))
65anidms 566 . . . . . . 7 (๐ป โІ โ„‹ โ†’ (๐ป ร— ๐ป) โІ ( โ„‹ ร— โ„‹))
72fdmi 6720 . . . . . . 7 dom +โ„Ž = ( โ„‹ ร— โ„‹)
86, 7sseqtrrdi 4026 . . . . . 6 (๐ป โІ โ„‹ โ†’ (๐ป ร— ๐ป) โІ dom +โ„Ž )
9 funimassov 7578 . . . . . 6 ((Fun +โ„Ž โˆง (๐ป ร— ๐ป) โІ dom +โ„Ž ) โ†’ (( +โ„Ž โ€œ (๐ป ร— ๐ป)) โІ ๐ป โ†” โˆ€๐‘ฅ โˆˆ ๐ป โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ป))
104, 8, 9sylancr 586 . . . . 5 (๐ป โІ โ„‹ โ†’ (( +โ„Ž โ€œ (๐ป ร— ๐ป)) โІ ๐ป โ†” โˆ€๐‘ฅ โˆˆ ๐ป โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ป))
11 ax-hfvmul 30752 . . . . . . 7 ยทโ„Ž :(โ„‚ ร— โ„‹)โŸถ โ„‹
12 ffun 6711 . . . . . . 7 ( ยทโ„Ž :(โ„‚ ร— โ„‹)โŸถ โ„‹ โ†’ Fun ยทโ„Ž )
1311, 12ax-mp 5 . . . . . 6 Fun ยทโ„Ž
14 xpss2 5687 . . . . . . 7 (๐ป โІ โ„‹ โ†’ (โ„‚ ร— ๐ป) โІ (โ„‚ ร— โ„‹))
1511fdmi 6720 . . . . . . 7 dom ยทโ„Ž = (โ„‚ ร— โ„‹)
1614, 15sseqtrrdi 4026 . . . . . 6 (๐ป โІ โ„‹ โ†’ (โ„‚ ร— ๐ป) โІ dom ยทโ„Ž )
17 funimassov 7578 . . . . . 6 ((Fun ยทโ„Ž โˆง (โ„‚ ร— ๐ป) โІ dom ยทโ„Ž ) โ†’ (( ยทโ„Ž โ€œ (โ„‚ ร— ๐ป)) โІ ๐ป โ†” โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ ยทโ„Ž ๐‘ฆ) โˆˆ ๐ป))
1813, 16, 17sylancr 586 . . . . 5 (๐ป โІ โ„‹ โ†’ (( ยทโ„Ž โ€œ (โ„‚ ร— ๐ป)) โІ ๐ป โ†” โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ ยทโ„Ž ๐‘ฆ) โˆˆ ๐ป))
1910, 18anbi12d 630 . . . 4 (๐ป โІ โ„‹ โ†’ ((( +โ„Ž โ€œ (๐ป ร— ๐ป)) โІ ๐ป โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— ๐ป)) โІ ๐ป) โ†” (โˆ€๐‘ฅ โˆˆ ๐ป โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ป โˆง โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ ยทโ„Ž ๐‘ฆ) โˆˆ ๐ป)))
2019adantr 480 . . 3 ((๐ป โІ โ„‹ โˆง 0โ„Ž โˆˆ ๐ป) โ†’ ((( +โ„Ž โ€œ (๐ป ร— ๐ป)) โІ ๐ป โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— ๐ป)) โІ ๐ป) โ†” (โˆ€๐‘ฅ โˆˆ ๐ป โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ป โˆง โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ ยทโ„Ž ๐‘ฆ) โˆˆ ๐ป)))
2120pm5.32i 574 . 2 (((๐ป โІ โ„‹ โˆง 0โ„Ž โˆˆ ๐ป) โˆง (( +โ„Ž โ€œ (๐ป ร— ๐ป)) โІ ๐ป โˆง ( ยทโ„Ž โ€œ (โ„‚ ร— ๐ป)) โІ ๐ป)) โ†” ((๐ป โІ โ„‹ โˆง 0โ„Ž โˆˆ ๐ป) โˆง (โˆ€๐‘ฅ โˆˆ ๐ป โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ป โˆง โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ ยทโ„Ž ๐‘ฆ) โˆˆ ๐ป)))
221, 21bitri 275 1 (๐ป โˆˆ Sโ„‹ โ†” ((๐ป โІ โ„‹ โˆง 0โ„Ž โˆˆ ๐ป) โˆง (โˆ€๐‘ฅ โˆˆ ๐ป โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ +โ„Ž ๐‘ฆ) โˆˆ ๐ป โˆง โˆ€๐‘ฅ โˆˆ โ„‚ โˆ€๐‘ฆ โˆˆ ๐ป (๐‘ฅ ยทโ„Ž ๐‘ฆ) โˆˆ ๐ป)))
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 395   โˆˆ wcel 2098  โˆ€wral 3053   โІ wss 3941   ร— cxp 5665  dom cdm 5667   โ€œ cima 5670  Fun wfun 6528  โŸถwf 6530  (class class class)co 7402  โ„‚cc 11105   โ„‹chba 30666   +โ„Ž cva 30667   ยทโ„Ž csm 30668  0โ„Žc0v 30671   Sโ„‹ csh 30675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418  ax-hilex 30746  ax-hfvadd 30747  ax-hfvmul 30752
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-fv 6542  df-ov 7405  df-sh 30954
This theorem is referenced by:  shaddcl  30964  shmulcl  30965  issh3  30966  helch  30990  hsn0elch  30995  hhshsslem2  31015  ocsh  31030  shscli  31064  shintcli  31076  imaelshi  31805
  Copyright terms: Public domain W3C validator