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

Metamath Proof Explorer

Theorem hoaddridi

Description: Sum of a Hilbert space operator with the zero operator. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis hoaddrid.1 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion hoaddridi ( 𝑇 +op 0hop ) = 𝑇

Proof

Step Hyp Ref Expression
1 hoaddrid.1 ⊢ 𝑇 : ℋ ⟶ ℋ
2 ho0f ⊢ 0hop : ℋ ⟶ ℋ
3 hosval ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 0hop : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 +op 0hop ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 0hop ‘ 𝑥 ) ) )
4 1 2 3 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 +op 0hop ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 0hop ‘ 𝑥 ) ) )
5 ho0val ⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
6 5 oveq2d ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 0hop ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ 0ℎ ) )
7 1 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
8 ax-hvaddid ⊢ ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) +ℎ 0ℎ ) = ( 𝑇 ‘ 𝑥 ) )
9 7 8 syl ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) +ℎ 0ℎ ) = ( 𝑇 ‘ 𝑥 ) )
10 4 6 9 3eqtrd ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 +op 0hop ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
11 10 rgen ⊢ ∀ 𝑥 ∈ ℋ ( ( 𝑇 +op 0hop ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 )
12 1 2 hoaddcli ⊢ ( 𝑇 +op 0hop ) : ℋ ⟶ ℋ
13 12 1 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 +op 0hop ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ↔ ( 𝑇 +op 0hop ) = 𝑇 )
14 11 13 mpbi ⊢ ( 𝑇 +op 0hop ) = 𝑇