Metamath Proof Explorer

Theorem hhsssh

Description: The predicate " H is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hhsst.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 hhsst.2 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
3 1 2 hhsst โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) )
4 shss โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ๐ป โŠ† โ„‹ )
5 3 4 jca โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) )
6 eleq1 โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ๐ป โˆˆ Sโ„‹ โ†” if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โˆˆ Sโ„‹ ) )
7 eqid โŠข โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ = โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ
8 xpeq1 โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ๐ป ร— ๐ป ) = ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— ๐ป ) )
9 xpeq2 โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— ๐ป ) = ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
10 8 9 eqtrd โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ๐ป ร— ๐ป ) = ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
11 10 reseq2d โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) )
12 xpeq2 โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( โ„‚ ร— ๐ป ) = ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
13 12 reseq2d โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) = ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) )
14 11 13 opeq12d โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ = โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ )
15 reseq2 โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( normโ„Ž โ†พ ๐ป ) = ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
16 14 15 opeq12d โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ = โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ )
17 2 16 eqtrid โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ )
18 17 eleq1d โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โ†” โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) ) )
19 sseq1 โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ๐ป โŠ† โ„‹ โ†” if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โŠ† โ„‹ ) )
20 18 19 anbi12d โŠข ( ๐ป = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) โ†” ( โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โŠ† โ„‹ ) ) )
21 xpeq1 โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( โ„‹ ร— โ„‹ ) = ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— โ„‹ ) )
22 xpeq2 โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— โ„‹ ) = ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
23 21 22 eqtrd โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( โ„‹ ร— โ„‹ ) = ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
24 23 reseq2d โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) = ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) )
25 xpeq2 โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( โ„‚ ร— โ„‹ ) = ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
26 25 reseq2d โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) = ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) )
27 24 26 opeq12d โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ = โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ )
28 reseq2 โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( normโ„Ž โ†พ โ„‹ ) = ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) )
29 27 28 opeq12d โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ โŸจ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ , ( normโ„Ž โ†พ โ„‹ ) โŸฉ = โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ )
30 29 eleq1d โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( โŸจ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ , ( normโ„Ž โ†พ โ„‹ ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โ†” โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) ) )
31 sseq1 โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( โ„‹ โŠ† โ„‹ โ†” if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โŠ† โ„‹ ) )
32 30 31 anbi12d โŠข ( โ„‹ = if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โ†’ ( ( โŸจ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ , ( normโ„Ž โ†พ โ„‹ ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง โ„‹ โŠ† โ„‹ ) โ†” ( โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โŠ† โ„‹ ) ) )
33 ax-hfvadd โŠข +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹
34 ffn โŠข ( +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹ โ†’ +โ„Ž Fn ( โ„‹ ร— โ„‹ ) )
35 fnresdm โŠข ( +โ„Ž Fn ( โ„‹ ร— โ„‹ ) โ†’ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) = +โ„Ž )
36 33 34 35 mp2b โŠข ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) = +โ„Ž
37 ax-hfvmul โŠข ยทโ„Ž : ( โ„‚ ร— โ„‹ ) โŸถ โ„‹
38 ffn โŠข ( ยทโ„Ž : ( โ„‚ ร— โ„‹ ) โŸถ โ„‹ โ†’ ยทโ„Ž Fn ( โ„‚ ร— โ„‹ ) )
39 fnresdm โŠข ( ยทโ„Ž Fn ( โ„‚ ร— โ„‹ ) โ†’ ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) = ยทโ„Ž )
40 37 38 39 mp2b โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) = ยทโ„Ž
41 36 40 opeq12i โŠข โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ = โŸจ +โ„Ž , ยทโ„Ž โŸฉ
42 normf โŠข normโ„Ž : โ„‹ โŸถ โ„
43 ffn โŠข ( normโ„Ž : โ„‹ โŸถ โ„ โ†’ normโ„Ž Fn โ„‹ )
44 fnresdm โŠข ( normโ„Ž Fn โ„‹ โ†’ ( normโ„Ž โ†พ โ„‹ ) = normโ„Ž )
45 42 43 44 mp2b โŠข ( normโ„Ž โ†พ โ„‹ ) = normโ„Ž
46 41 45 opeq12i โŠข โŸจ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ , ( normโ„Ž โ†พ โ„‹ ) โŸฉ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
47 46 1 eqtr4i โŠข โŸจ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ , ( normโ„Ž โ†พ โ„‹ ) โŸฉ = ๐‘ˆ
48 1 hhnv โŠข ๐‘ˆ โˆˆ NrmCVec
49 eqid โŠข ( SubSp โ€˜ ๐‘ˆ ) = ( SubSp โ€˜ ๐‘ˆ )
50 49 sspid โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ๐‘ˆ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) )
51 48 50 ax-mp โŠข ๐‘ˆ โˆˆ ( SubSp โ€˜ ๐‘ˆ )
52 47 51 eqeltri โŠข โŸจ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ , ( normโ„Ž โ†พ โ„‹ ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ )
53 ssid โŠข โ„‹ โŠ† โ„‹
54 52 53 pm3.2i โŠข ( โŸจ โŸจ ( +โ„Ž โ†พ ( โ„‹ ร— โ„‹ ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— โ„‹ ) ) โŸฉ , ( normโ„Ž โ†พ โ„‹ ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง โ„‹ โŠ† โ„‹ )
55 20 32 54 elimhyp โŠข ( โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โŠ† โ„‹ )
56 55 simpli โŠข โŸจ โŸจ ( +โ„Ž โ†พ ( if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) ) โŸฉ , ( normโ„Ž โ†พ if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) ) โŸฉ โˆˆ ( SubSp โ€˜ ๐‘ˆ )
57 55 simpri โŠข if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โŠ† โ„‹
58 1 7 56 57 hhshsslem2 โŠข if ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) , ๐ป , โ„‹ ) โˆˆ Sโ„‹
59 6 58 dedth โŠข ( ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) โ†’ ๐ป โˆˆ Sโ„‹ )
60 5 59 impbii โŠข ( ๐ป โˆˆ Sโ„‹ โ†” ( ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) โˆง ๐ป โŠ† โ„‹ ) )