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