Metamath Proof Explorer


Theorem hhssvs

Description: The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hhsssh2.1 โŠข ๐‘Š = โŸจ โŸจ ( +โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) , ( ยทโ„Ž โ†พ ( โ„‚ ร— ๐ป ) ) โŸฉ , ( normโ„Ž โ†พ ๐ป ) โŸฉ
2 hhssba.2 โŠข ๐ป โˆˆ Sโ„‹
3 eqid โŠข โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
4 3 hhnv โŠข โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ โˆˆ NrmCVec
5 3 1 hhsst โŠข ( ๐ป โˆˆ Sโ„‹ โ†’ ๐‘Š โˆˆ ( SubSp โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ ) )
6 2 5 ax-mp โŠข ๐‘Š โˆˆ ( SubSp โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ )
7 1 2 hhssba โŠข ๐ป = ( BaseSet โ€˜ ๐‘Š )
8 3 hhvs โŠข โˆ’โ„Ž = ( โˆ’๐‘ฃ โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ )
9 eqid โŠข ( โˆ’๐‘ฃ โ€˜ ๐‘Š ) = ( โˆ’๐‘ฃ โ€˜ ๐‘Š )
10 eqid โŠข ( SubSp โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ ) = ( SubSp โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ )
11 7 8 9 10 sspm โŠข ( ( โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ โˆˆ NrmCVec โˆง ๐‘Š โˆˆ ( SubSp โ€˜ โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ ) ) โ†’ ( โˆ’๐‘ฃ โ€˜ ๐‘Š ) = ( โˆ’โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) )
12 4 6 11 mp2an โŠข ( โˆ’๐‘ฃ โ€˜ ๐‘Š ) = ( โˆ’โ„Ž โ†พ ( ๐ป ร— ๐ป ) )
13 12 eqcomi โŠข ( โˆ’โ„Ž โ†พ ( ๐ป ร— ๐ป ) ) = ( โˆ’๐‘ฃ โ€˜ ๐‘Š )