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

Metamath Proof Explorer

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 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
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 )