Metamath Proof Explorer

Theorem hhssnvt

Description: Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhssnvt.1 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
Assertion hhssnvt ( ๐ป โˆˆ Sโ„‹ โ†’ ๐‘Š โˆˆ NrmCVec )

Proof

Step Hyp Ref Expression
1 hhssnvt.1 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
2 xpeq1 โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( ๐ป ร— ๐ป ) = ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— ๐ป ) )
3 xpeq2 โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— ๐ป ) = ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) )
4 2 3 eqtrd โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( ๐ป ร— ๐ป ) = ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) )
5 4 reseq2d โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) )
6 xpeq2 โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( โ„‚ ร— ๐ป ) = ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) )
7 6 reseq2d โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) = ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) )
8 5 7 opeq12d โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ = โŸจ ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) โŸฉ )
9 reseq2 โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( normโ„Ž โ†พ ๐ป ) = ( normโ„Ž โ†พ if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) )
10 8 9 opeq12d โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ = โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) โŸฉ )
11 1 10 eqtrid โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) โŸฉ )
12 11 eleq1d โŠข ( ๐ป = if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โ†’ ( ๐‘Š โˆˆ NrmCVec โ†” โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) โŸฉ โˆˆ NrmCVec ) )
13 eqid โŠข โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) โŸฉ = โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) โŸฉ
14 h0elsh โŠข 0โ„‹ โˆˆ Sโ„‹
15 14 elimel โŠข if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) โˆˆ Sโ„‹
16 13 15 hhssnv โŠข โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ๐ป โˆˆ Sโ„‹ , ๐ป , 0โ„‹ ) ) โŸฉ โˆˆ NrmCVec
17 12 16 dedth โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ๐‘Š โˆˆ NrmCVec )