This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = 𝑍