Metamath Proof Explorer

Theorem pjddii

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

Ref Expression
Hypotheses pjsdi.1 ⊢ 𝐻 ∈ Cℋ
pjsdi.2 ⊢ 𝑆 : ℋ ⟶ ℋ
pjsdi.3 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion pjddii ( ( 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 pjsubi ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑥 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
7 4 5 6 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑆 ‘ 𝑥 ) ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
8 hodval ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 −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 hosubcli ⊢ ( 𝑆 −op 𝑇 ) : ℋ ⟶ ℋ
17 11 16 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ ( 𝑆 −op 𝑇 ) ) ‘ 𝑥 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝑆 −op 𝑇 ) ‘ 𝑥 ) ) )
18 11 2 hocofi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ 𝑆 ) : ℋ ⟶ ℋ
19 11 3 hocofi ⊢ ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) : ℋ ⟶ ℋ
20 hodval ⊢ ( ( ( ( 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 hosubcli ⊢ ( ( ( 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ℎ ‘ 𝐻 ) ∘ 𝑇 ) )