Theorem ho01i

Description: A condition implying that a Hilbert space operator is identically zero. Lemma 3.2(S8) of Beran p. 95. (Contributed by NM, 28-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ho0.1	⊢ 𝑇 : ℋ ⟶ ℋ
Assertion	ho01i	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = 0 ↔ 𝑇 = 0hop )

Proof

Step	Hyp	Ref	Expression
1		ho0.1	⊢ 𝑇 : ℋ ⟶ ℋ
2		ffn	⊢ ( 𝑇 : ℋ ⟶ ℋ → 𝑇 Fn ℋ )
3	1 2	ax-mp	⊢ 𝑇 Fn ℋ
4		ax-hv0cl	⊢ 0ℎ ∈ ℋ
5	4	elexi	⊢ 0ℎ ∈ V
6	5	fconst	⊢ ( ℋ × { 0ℎ } ) : ℋ ⟶ { 0ℎ }
7		ffn	⊢ ( ( ℋ × { 0ℎ } ) : ℋ ⟶ { 0ℎ } → ( ℋ × { 0ℎ } ) Fn ℋ )
8	6 7	ax-mp	⊢ ( ℋ × { 0ℎ } ) Fn ℋ
9		eqfnfv	⊢ ( ( 𝑇 Fn ℋ ∧ ( ℋ × { 0ℎ } ) Fn ℋ ) → ( 𝑇 = ( ℋ × { 0ℎ } ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( ( ℋ × { 0ℎ } ) ‘ 𝑥 ) ) )
10	3 8 9	mp2an	⊢ ( 𝑇 = ( ℋ × { 0ℎ } ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( ( ℋ × { 0ℎ } ) ‘ 𝑥 ) )
11		df0op2	⊢ 0hop = ( ℋ × 0ℋ )
12		df-ch0	⊢ 0ℋ = { 0ℎ }
13	12	xpeq2i	⊢ ( ℋ × 0ℋ ) = ( ℋ × { 0ℎ } )
14	11 13	eqtri	⊢ 0hop = ( ℋ × { 0ℎ } )
15	14	eqeq2i	⊢ ( 𝑇 = 0hop ↔ 𝑇 = ( ℋ × { 0ℎ } ) )
16	1	ffvelrni	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
17		hial0	⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = 0 ↔ ( 𝑇 ‘ 𝑥 ) = 0ℎ ) )
18	16 17	syl	⊢ ( 𝑥 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = 0 ↔ ( 𝑇 ‘ 𝑥 ) = 0ℎ ) )
19	5	fvconst2	⊢ ( 𝑥 ∈ ℋ → ( ( ℋ × { 0ℎ } ) ‘ 𝑥 ) = 0ℎ )
20	19	eqeq2d	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) = ( ( ℋ × { 0ℎ } ) ‘ 𝑥 ) ↔ ( 𝑇 ‘ 𝑥 ) = 0ℎ ) )
21	18 20	bitr4d	⊢ ( 𝑥 ∈ ℋ → ( ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = 0 ↔ ( 𝑇 ‘ 𝑥 ) = ( ( ℋ × { 0ℎ } ) ‘ 𝑥 ) ) )
22	21	ralbiia	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = 0 ↔ ∀ 𝑥 ∈ ℋ ( 𝑇 ‘ 𝑥 ) = ( ( ℋ × { 0ℎ } ) ‘ 𝑥 ) )
23	10 15 22	3bitr4ri	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = 0 ↔ 𝑇 = 0hop )