Metamath Proof Explorer

Theorem pjsdii

Description: Distributive law for Hilbert space operator sum. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjsdi.1 ⊢ 𝐻 ∈ Cℋ
pjsdi.2 ⊢ 𝑆 : ℋ ⟶ ℋ
pjsdi.3 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion pjsdii ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 pjsdi.1 ⊢ 𝐻 ∈ Cℋ
2 pjsdi.2 ⊢ 𝑆 : ℋ ⟶ ℋ
3 pjsdi.3 ⊢ 𝑇 : ℋ ⟶ ℋ
4 2 ffvelrni ⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
5 3 ffvelrni ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
6 1 pjaddi ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
7 4 5 6 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
8 hosval ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
9 2 3 8 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
10 9 fveq2d ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
11 1 pjfi ⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
12 11 2 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑥 ) ) )
13 11 3 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝑥 ) ) )
14 12 13 oveq12d ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) ‘ 𝑥 ) +ℎ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
15 7 10 14 3eqtr4d ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) ‘ 𝑥 ) +ℎ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝑥 ) ) )
16 2 3 hoaddcli ⊢ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
17 11 16 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) )
18 11 2 hocofi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) : ℋ ⟶ ℋ
19 11 3 hocofi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) : ℋ ⟶ ℋ
20 hosval ⊢ ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) : ℋ ⟶ ℋ ∧ ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) ‘ 𝑥 ) +ℎ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝑥 ) ) )
21 18 19 20 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) ‘ 𝑥 ) +ℎ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝑥 ) ) )
22 15 17 21 3eqtr4d ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ) ‘ 𝑥 ) )
23 22 rgen ⊢ ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ) ‘ 𝑥 )
24 11 16 hocofi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) : ℋ ⟶ ℋ
25 18 19 hoaddcli ⊢ ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ) : ℋ ⟶ ℋ
26 24 25 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ) ‘ 𝑥 ) ↔ ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ) )
27 23 26 mpbi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 +op 𝑇 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) +op ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) )