Theorem hoaddid1i

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

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

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.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	ffvelrni	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
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 ) = 𝑇