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

Theorem issh2 22668
 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
Distinct variable group:   ,,

Proof of Theorem issh2
StepHypRef Expression
1 issh 22667 . 2
2 ax-hfvadd 22460 . . . . . . 7
3 ffun 5556 . . . . . . 7
42, 3ax-mp 8 . . . . . 6
5 xpss12 4944 . . . . . . . 8
65anidms 627 . . . . . . 7
72fdmi 5559 . . . . . . 7
86, 7syl6sseqr 3359 . . . . . 6
9 funimassov 6186 . . . . . 6
104, 8, 9sylancr 645 . . . . 5
11 ax-hfvmul 22465 . . . . . . 7
12 ffun 5556 . . . . . . 7
1311, 12ax-mp 8 . . . . . 6
14 xpss2 4948 . . . . . . 7
1511fdmi 5559 . . . . . . 7
1614, 15syl6sseqr 3359 . . . . . 6
17 funimassov 6186 . . . . . 6
1813, 16, 17sylancr 645 . . . . 5
1910, 18anbi12d 692 . . . 4