Metamath Proof Explorer

Theorem hhsst

Description: A member of SH is a subspace. (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhsst.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
hhsst.2 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
Assertion hhsst ( ๐ป โˆˆ Sโ„‹ โ†’ ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) )

Proof

Step Hyp Ref Expression
1 hhsst.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 hhsst.2 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
3 2 hhssnvt โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ๐‘Š โˆˆ NrmCVec )
4 resss โŠข ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โŠ† +โ„Ž
5 resss โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŠ† ยทโ„Ž
6 resss โŠข ( normโ„Ž โ†พ ๐ป ) โŠ† normโ„Ž
7 4 5 6 3pm3.2i โŠข ( ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โŠ† +โ„Ž โˆง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŠ† ยทโ„Ž โˆง ( normโ„Ž โ†พ ๐ป ) โŠ† normโ„Ž )
8 3 7 jctir โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ( ๐‘Š โˆˆ NrmCVec โˆง ( ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โŠ† +โ„Ž โˆง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŠ† ยทโ„Ž โˆง ( normโ„Ž โ†พ ๐ป ) โŠ† normโ„Ž ) ) )
9 1 hhnv โŠข ๐‘ˆ โˆˆ NrmCVec
10 1 hhva โŠข +โ„Ž = ( +๐‘ฃ โ€˜ ๐‘ˆ )
11 2 hhssva โŠข ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( +๐‘ฃ โ€˜ ๐‘Š )
12 1 hhsm โŠข ยทโ„Ž = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
13 2 hhsssm โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) = ( ยท๐‘ OLD โ€˜ ๐‘Š )
14 1 hhnm โŠข normโ„Ž = ( normCV โ€˜ ๐‘ˆ )
15 2 hhssnm โŠข ( normโ„Ž โ†พ ๐ป ) = ( normCV โ€˜ ๐‘Š )
16 eqid โŠข ( SubSp โ€˜ ๐‘ˆ ) = ( SubSp โ€˜ ๐‘ˆ )
17 10 11 12 13 14 15 16 isssp โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โ†” ( ๐‘Š โˆˆ NrmCVec โˆง ( ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โŠ† +โ„Ž โˆง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŠ† ยทโ„Ž โˆง ( normโ„Ž โ†พ ๐ป ) โŠ† normโ„Ž ) ) ) )
18 9 17 ax-mp โŠข ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โ†” ( ๐‘Š โˆˆ NrmCVec โˆง ( ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โŠ† +โ„Ž โˆง ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŠ† ยทโ„Ž โˆง ( normโ„Ž โ†พ ๐ป ) โŠ† normโ„Ž ) ) )
19 8 18 sylibr โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) )