Metamath Proof Explorer

Theorem issh2

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.)

Ref Expression
Assertion issh2 ( ๐ป โˆˆ Sโ„‹ โ†” ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( โˆ€ ๐‘ฅ โˆˆ ๐ป โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป ) ) )

Proof

Step Hyp Ref Expression
1 issh โŠข ( ๐ป โˆˆ Sโ„‹ โ†” ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) )
2 ax-hfvadd โŠข +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹
3 ffun โŠข ( +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹ โ†’ Fun +โ„Ž )
4 2 3 ax-mp โŠข Fun +โ„Ž
5 xpss12 โŠข ( ( ๐ป โŠ† โ„‹ โˆง ๐ป โŠ† โ„‹ ) โ†’ ( ๐ป ร— ๐ป ) โŠ† ( โ„‹ ร— โ„‹ ) )
6 5 anidms โŠข ( ๐ป โŠ† โ„‹ โ†’ ( ๐ป ร— ๐ป ) โŠ† ( โ„‹ ร— โ„‹ ) )
7 2 fdmi โŠข dom +โ„Ž = ( โ„‹ ร— โ„‹ )
8 6 7 sseqtrrdi โŠข ( ๐ป โŠ† โ„‹ โ†’ ( ๐ป ร— ๐ป ) โŠ† dom +โ„Ž )
9 funimassov โŠข ( ( Fun +โ„Ž โˆง ( ๐ป ร— ๐ป ) โŠ† dom +โ„Ž ) โ†’ ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โ†” โˆ€ ๐‘ฅ โˆˆ ๐ป โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป ) )
10 4 8 9 sylancr โŠข ( ๐ป โŠ† โ„‹ โ†’ ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โ†” โˆ€ ๐‘ฅ โˆˆ ๐ป โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป ) )
11 ax-hfvmul โŠข ยทโ„Ž : ( โ„‚ ร— โ„‹ ) โŸถ โ„‹
12 ffun โŠข ( ยทโ„Ž : ( โ„‚ ร— โ„‹ ) โŸถ โ„‹ โ†’ Fun ยทโ„Ž )
13 11 12 ax-mp โŠข Fun ยทโ„Ž
14 xpss2 โŠข ( ๐ป โŠ† โ„‹ โ†’ ( โ„‚ ร— ๐ป ) โŠ† ( โ„‚ ร— โ„‹ ) )
15 11 fdmi โŠข dom ยทโ„Ž = ( โ„‚ ร— โ„‹ )
16 14 15 sseqtrrdi โŠข ( ๐ป โŠ† โ„‹ โ†’ ( โ„‚ ร— ๐ป ) โŠ† dom ยทโ„Ž )
17 funimassov โŠข ( ( Fun ยทโ„Ž โˆง ( โ„‚ ร— ๐ป ) โŠ† dom ยทโ„Ž ) โ†’ ( ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป โ†” โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป ) )
18 13 16 17 sylancr โŠข ( ๐ป โŠ† โ„‹ โ†’ ( ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป โ†” โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป ) )
19 10 18 anbi12d โŠข ( ๐ป โŠ† โ„‹ โ†’ ( ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) โ†” ( โˆ€ ๐‘ฅ โˆˆ ๐ป โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป ) ) )
20 19 adantr โŠข ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โ†’ ( ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) โ†” ( โˆ€ ๐‘ฅ โˆˆ ๐ป โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป ) ) )
21 20 pm5.32i โŠข ( ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( ( +โ„Ž โ€œ ( ๐ป ร— ๐ป ) ) โŠ† ๐ป โˆง ( ยทโ„Ž โ€œ ( โ„‚ ร— ๐ป ) ) โŠ† ๐ป ) ) โ†” ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( โˆ€ ๐‘ฅ โˆˆ ๐ป โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป ) ) )
22 1 21 bitri โŠข ( ๐ป โˆˆ Sโ„‹ โ†” ( ( ๐ป โŠ† โ„‹ โˆง 0โ„Ž โˆˆ ๐ป ) โˆง ( โˆ€ ๐‘ฅ โˆˆ ๐ป โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ +โ„Ž ๐‘ฆ ) โˆˆ ๐ป โˆง โˆ€ ๐‘ฅ โˆˆ โ„‚ โˆ€ ๐‘ฆ โˆˆ ๐ป ( ๐‘ฅ ยทโ„Ž ๐‘ฆ ) โˆˆ ๐ป ) ) )