Metamath Proof Explorer

Theorem issh

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. (Contributed by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion issh ( ๐ป โˆˆ Sโ„‹ โ†” ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex โŠข โ„‹ โˆˆ V
2 1 elpw2 โŠข ( ๐ป โˆˆ ๐’ซ โ„‹ โ†” ๐ป โŠ† โ„‹ )
3 3anass โŠข ( ( 0โ„Ž โˆˆ ๐ป โˆง ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) โ†” ( 0โ„Ž โˆˆ ๐ป โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) )
4 2 3 anbi12i โŠข ( ( ๐ป โˆˆ ๐’ซ โ„‹ โˆง ( 0โ„Ž โˆˆ ๐ป โˆง ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) โ†” ( ๐ป โŠ† โ„‹ โˆง ( 0โ„Ž โˆˆ ๐ป โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) ) )
5 eleq2 โŠข ( โ„Ž = ๐ป โ†’ ( 0โ„Ž โˆˆ โ„Ž โ†” 0โ„Ž โˆˆ ๐ป ) )
6 id โŠข ( โ„Ž = ๐ป โ†’ โ„Ž = ๐ป )
7 6 sqxpeqd โŠข ( โ„Ž = ๐ป โ†’ ( โ„Ž ร— โ„Ž ) = ( ๐ป ร— ๐ป ) )
8 7 imaeq2d โŠข ( โ„Ž = ๐ป โ†’ ( +โ„Ž โ€œ ( โ„Ž ร— โ„Ž ) ) = ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) )
9 8 6 sseq12d โŠข ( โ„Ž = ๐ป โ†’ ( ( +โ„Ž โ€œ ( โ„Ž ร— โ„Ž ) ) โŠ† โ„Ž โ†” ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป ) )
10 xpeq2 โŠข ( โ„Ž = ๐ป โ†’ ( โ„‚ ร— โ„Ž ) = ( โ„‚ ร— ๐ป ) )
11 10 imaeq2d โŠข ( โ„Ž = ๐ป โ†’ ( ยทโ„Ž โ€œ ( โ„‚ ร— โ„Ž ) ) = ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) )
12 11 6 sseq12d โŠข ( โ„Ž = ๐ป โ†’ ( ( ยทโ„Ž โ€œ ( โ„‚ ร— โ„Ž ) ) โŠ† โ„Ž โ†” ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) )
13 5 9 12 3anbi123d โŠข ( โ„Ž = ๐ป โ†’ ( ( 0โ„Ž โˆˆ โ„Ž โˆง ( +โ„Ž โ€œ ( โ„Ž ร— โ„Ž ) ) โŠ† โ„Ž โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— โ„Ž ) ) โŠ† โ„Ž ) โ†” ( 0โ„Ž โˆˆ ๐ป โˆง ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) )
14 df-sh โŠข Sโ„‹ = { โ„Ž โˆˆ ๐’ซ โ„‹ โˆฃ ( 0โ„Ž โˆˆ โ„Ž โˆง ( +โ„Ž โ€œ ( โ„Ž ร— โ„Ž ) ) โŠ† โ„Ž โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— โ„Ž ) ) โŠ† โ„Ž ) }
15 13 14 elrab2 โŠข ( ๐ป โˆˆ Sโ„‹ โ†” ( ๐ป โˆˆ ๐’ซ โ„‹ โˆง ( 0โ„Ž โˆˆ ๐ป โˆง ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) )
16 anass โŠข ( ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) โ†” ( ๐ป โŠ† โ„‹ โˆง ( 0โ„Ž โˆˆ ๐ป โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) ) )
17 4 15 16 3bitr4i โŠข ( ๐ป โˆˆ Sโ„‹ โ†” ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) )