Metamath Proof Explorer


Theorem hilims

Description: Hilbert space distance metric. (Contributed by NM, 13-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hilims.1 โŠข โ„‹ = ( BaseSet โ€˜ ๐‘ˆ )
hilims.2 โŠข +โ„Ž = ( +๐‘ฃ โ€˜ ๐‘ˆ )
hilims.3 โŠข ยทโ„Ž = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
hilims.5 โŠข ยทih = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
hilims.8 โŠข ๐ท = ( IndMet โ€˜ ๐‘ˆ )
hilims.9 โŠข ๐‘ˆ โˆˆ NrmCVec
Assertion hilims ๐ท = ( normโ„Ž โˆ˜ โˆ’โ„Ž )

Proof

Step Hyp Ref Expression
1 hilims.1 โŠข โ„‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 hilims.2 โŠข +โ„Ž = ( +๐‘ฃ โ€˜ ๐‘ˆ )
3 hilims.3 โŠข ยทโ„Ž = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
4 hilims.5 โŠข ยทih = ( ยท๐‘–OLD โ€˜ ๐‘ˆ )
5 hilims.8 โŠข ๐ท = ( IndMet โ€˜ ๐‘ˆ )
6 hilims.9 โŠข ๐‘ˆ โˆˆ NrmCVec
7 1 2 3 4 6 hilhhi โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
8 7 5 hhims2 โŠข ๐ท = ( normโ„Ž โˆ˜ โˆ’โ„Ž )