Metamath Proof Explorer

Theorem hh0oi

Description: The zero operator in Hilbert space. (Contributed by NM, 7-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hhnmo.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
hh0o.2 โŠข ๐‘ = ( ๐‘ˆ 0op ๐‘ˆ )
Assertion hh0oi 0hop = ๐‘

Proof

Step Hyp Ref Expression
1 hhnmo.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
2 hh0o.2 โŠข ๐‘ = ( ๐‘ˆ 0op ๐‘ˆ )
3 1 hhba โŠข โ„‹ = ( BaseSet โ€˜ ๐‘ˆ )
4 df-ch0 โŠข 0โ„‹ = { 0โ„Ž }
5 1 hh0v โŠข 0โ„Ž = ( 0vec โ€˜ ๐‘ˆ )
6 5 sneqi โŠข { 0โ„Ž } = { ( 0vec โ€˜ ๐‘ˆ ) }
7 4 6 eqtri โŠข 0โ„‹ = { ( 0vec โ€˜ ๐‘ˆ ) }
8 3 7 xpeq12i โŠข ( โ„‹ ร— 0โ„‹ ) = ( ( BaseSet โ€˜ ๐‘ˆ ) ร— { ( 0vec โ€˜ ๐‘ˆ ) } )
9 df0op2 โŠข 0hop = ( โ„‹ ร— 0โ„‹ )
10 1 hhnv โŠข ๐‘ˆ โˆˆ NrmCVec
11 eqid โŠข ( BaseSet โ€˜ ๐‘ˆ ) = ( BaseSet โ€˜ ๐‘ˆ )
12 eqid โŠข ( 0vec โ€˜ ๐‘ˆ ) = ( 0vec โ€˜ ๐‘ˆ )
13 11 12 2 0ofval โŠข ( ( ๐‘ˆ โˆˆ NrmCVec โˆง ๐‘ˆ โˆˆ NrmCVec ) โ†’ ๐‘ = ( ( BaseSet โ€˜ ๐‘ˆ ) ร— { ( 0vec โ€˜ ๐‘ˆ ) } ) )
14 10 10 13 mp2an โŠข ๐‘ = ( ( BaseSet โ€˜ ๐‘ˆ ) ร— { ( 0vec โ€˜ ๐‘ˆ ) } )
15 8 9 14 3eqtr4i โŠข 0hop = ๐‘