Metamath Proof Explorer

Theorem hhshsslem1

Description: Lemma for hhsssh . (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hhsst.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 hhsst.2 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
3 hhssp3.3 โŠข ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ )
4 hhssp3.4 โŠข ๐ป โŠ† โ„‹
5 eqid โŠข ( BaseSet โ€˜ ๐‘Š ) = ( BaseSet โ€˜ ๐‘Š )
6 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘Š ) = ( +๐‘ฃ โ€˜ ๐‘Š )
7 5 6 bafval โŠข ( BaseSet โ€˜ ๐‘Š ) = ran ( +๐‘ฃ โ€˜ ๐‘Š )
8 1 hhnv โŠข ๐‘ˆ โˆˆ NrmCVec
9 eqid โŠข ( SubSp โ€˜ ๐‘ˆ ) = ( SubSp โ€˜ ๐‘ˆ )
10 9 sspnv โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ( SubSp โ€˜ ๐‘ˆ ) ) โ†’ ๐‘Š โˆˆ NrmCVec )
11 8 3 10 mp2an โŠข ๐‘Š โˆˆ NrmCVec
12 6 nvgrp โŠข ( ๐‘Š โˆˆ NrmCVec โ†’ ( +๐‘ฃ โ€˜ ๐‘Š ) โˆˆ GrpOp )
13 grporndm โŠข ( ( +๐‘ฃ โ€˜ ๐‘Š ) โˆˆ GrpOp โ†’ ran ( +๐‘ฃ โ€˜ ๐‘Š ) = dom dom ( +๐‘ฃ โ€˜ ๐‘Š ) )
14 11 12 13 mp2b โŠข ran ( +๐‘ฃ โ€˜ ๐‘Š ) = dom dom ( +๐‘ฃ โ€˜ ๐‘Š )
15 2 fveq2i โŠข ( +๐‘ฃ โ€˜ ๐‘Š ) = ( +๐‘ฃ โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ )
16 eqid โŠข ( +๐‘ฃ โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) = ( +๐‘ฃ โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ )
17 16 vafval โŠข ( +๐‘ฃ โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) = ( 1st โ€˜ ( 1st โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) )
18 opex โŠข โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ โˆˆ V
19 normf โŠข normโ„Ž : โ„‹ โŸถ โ„
20 ax-hilex โŠข โ„‹ โˆˆ V
21 fex โŠข ( ( normโ„Ž : โ„‹ โŸถ โ„ โˆง โ„‹ โˆˆ V ) โ†’ normโ„Ž โˆˆ V )
22 19 20 21 mp2an โŠข normโ„Ž โˆˆ V
23 22 resex โŠข ( normโ„Ž โ†พ ๐ป ) โˆˆ V
24 18 23 op1st โŠข ( 1st โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) = โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ
25 24 fveq2i โŠข ( 1st โ€˜ ( 1st โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) ) = ( 1st โ€˜ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ )
26 hilablo โŠข +โ„Ž โˆˆ AbelOp
27 resexg โŠข ( +โ„Ž โˆˆ AbelOp โ†’ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ V )
28 26 27 ax-mp โŠข ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) โˆˆ V
29 hvmulex โŠข ยทโ„Ž โˆˆ V
30 29 resex โŠข ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โˆˆ V
31 28 30 op1st โŠข ( 1st โ€˜ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ ) = ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) )
32 25 31 eqtri โŠข ( 1st โ€˜ ( 1st โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) ) = ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) )
33 17 32 eqtri โŠข ( +๐‘ฃ โ€˜ โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ ) = ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) )
34 15 33 eqtri โŠข ( +๐‘ฃ โ€˜ ๐‘Š ) = ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) )
35 34 dmeqi โŠข dom ( +๐‘ฃ โ€˜ ๐‘Š ) = dom ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) )
36 xpss12 โŠข ( ( ๐ป โŠ† โ„‹ โˆง ๐ป โŠ† โ„‹ ) โ†’ ( ๐ป ร— ๐ป ) โŠ† ( โ„‹ ร— โ„‹ ) )
37 4 4 36 mp2an โŠข ( ๐ป ร— ๐ป ) โŠ† ( โ„‹ ร— โ„‹ )
38 ax-hfvadd โŠข +โ„Ž : ( โ„‹ ร— โ„‹ ) โŸถ โ„‹
39 38 fdmi โŠข dom +โ„Ž = ( โ„‹ ร— โ„‹ )
40 37 39 sseqtrri โŠข ( ๐ป ร— ๐ป ) โŠ† dom +โ„Ž
41 ssdmres โŠข ( ( ๐ป ร— ๐ป ) โŠ† dom +โ„Ž โ†” dom ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( ๐ป ร— ๐ป ) )
42 40 41 mpbi โŠข dom ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( ๐ป ร— ๐ป )
43 35 42 eqtri โŠข dom ( +๐‘ฃ โ€˜ ๐‘Š ) = ( ๐ป ร— ๐ป )
44 43 dmeqi โŠข dom dom ( +๐‘ฃ โ€˜ ๐‘Š ) = dom ( ๐ป ร— ๐ป )
45 dmxpid โŠข dom ( ๐ป ร— ๐ป ) = ๐ป
46 44 45 eqtri โŠข dom dom ( +๐‘ฃ โ€˜ ๐‘Š ) = ๐ป
47 14 46 eqtri โŠข ran ( +๐‘ฃ โ€˜ ๐‘Š ) = ๐ป
48 7 47 eqtri โŠข ( BaseSet โ€˜ ๐‘Š ) = ๐ป
49 48 eqcomi โŠข ๐ป = ( BaseSet โ€˜ ๐‘Š )