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

Metamath Proof Explorer

Theorem hoid1i

Description: Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis hoaddrid.1 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion hoid1i ( 𝑇 ∘ Iop ) = 𝑇

Proof

Step Hyp Ref Expression
1 hoaddrid.1 ⊢ 𝑇 : ℋ ⟶ ℋ
2 df-iop ⊢ Iop = ( projℎ ‘ ℋ )
3 2 coeq2i ⊢ ( 𝑇 ∘ Iop ) = ( 𝑇 ∘ ( projℎ ‘ ℋ ) )
4 helch ⊢ ℋ ∈ Cℋ
5 4 pjfi ⊢ ( projℎ ‘ ℋ ) : ℋ ⟶ ℋ
6 1 5 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) ) )
7 pjch1 ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) = 𝑥 )
8 7 fveq2d ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) ) = ( 𝑇 ‘ 𝑥 ) )
9 6 8 eqtrd ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
10 9 rgen ⊢ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 )
11 1 5 hocofi ⊢ ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) : ℋ ⟶ ℋ
12 11 1 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ↔ ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) = 𝑇 )
13 10 12 mpbi ⊢ ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) = 𝑇
14 3 13 eqtri ⊢ ( 𝑇 ∘ Iop ) = 𝑇