Metamath Proof Explorer

Theorem hhsssm

Description: The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhss.1 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
Assertion hhsssm ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) = ( ยท๐‘ OLD โ€˜ ๐‘Š )

Proof

Step Hyp Ref Expression
1 hhss.1 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
2 eqid โŠข ( ยท๐‘ OLD โ€˜ ๐‘Š ) = ( ยท๐‘ OLD โ€˜ ๐‘Š )
3 2 smfval โŠข ( ยท๐‘ OLD โ€˜ ๐‘Š ) = ( 2nd โ€˜ ( 1st โ€˜ ๐‘Š ) )
4 1 fveq2i โŠข ( 1st โ€˜ ๐‘Š ) = ( 1st โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ )
5 opex โŠข โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ โˆˆ V
6 normf โŠข normโ„Ž : โ„‹ โŸถ โ„
7 ax-hilex โŠข โ„‹ โˆˆ V
8 fex โŠข ( ( normโ„Ž : โ„‹ โŸถ โ„ โˆง โ„‹ โˆˆ V ) โ†’ normโ„Ž โˆˆ V )
9 6 7 8 mp2an โŠข normโ„Ž โˆˆ V
10 9 resex โŠข ( normโ„Ž โ†พ ๐ป ) โˆˆ V
11 5 10 op1st โŠข ( 1st โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) = โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ
12 4 11 eqtri โŠข ( 1st โ€˜ ๐‘Š ) = โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ
13 12 fveq2i โŠข ( 2nd โ€˜ ( 1st โ€˜ ๐‘Š ) ) = ( 2nd โ€˜ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ )
14 hilablo โŠข +โ„Ž โˆˆ AbelOp
15 resexg โŠข ( +โ„Ž โˆˆ AbelOp โ†’ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ V )
16 14 15 ax-mp โŠข ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ V
17 hvmulex โŠข ยทโ„Ž โˆˆ V
18 17 resex โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โˆˆ V
19 16 18 op2nd โŠข ( 2nd โ€˜ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ ) = ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) )
20 3 13 19 3eqtrri โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) = ( ยท๐‘ OLD โ€˜ ๐‘Š )