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

Metamath Proof Explorer

Theorem hoddii

Description: Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri does not require linearity.) (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hoddi.1 ⊢ 𝑅 ∈ LinOp
hoddi.2 ⊢ 𝑆 : ℋ ⟶ ℋ
hoddi.3 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion hoddii ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) = ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 hoddi.1 ⊢ 𝑅 ∈ LinOp
2 hoddi.2 ⊢ 𝑆 : ℋ ⟶ ℋ
3 hoddi.3 ⊢ 𝑇 : ℋ ⟶ ℋ
4 2 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
5 3 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
6 1 lnopsubi ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( 𝑅 ‘ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 𝑅 ‘ ( 𝑆 ‘ 𝑥 ) ) −ℎ ( 𝑅 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
7 4 5 6 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( 𝑅 ‘ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( 𝑅 ‘ ( 𝑆 ‘ 𝑥 ) ) −ℎ ( 𝑅 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
8 hodval ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 −op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) )
9 2 3 8 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 −op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) )
10 9 fveq2d ⊢ ( 𝑥 ∈ ℋ → ( 𝑅 ‘ ( ( 𝑆 −op 𝑇 ) ‘ 𝑥 ) ) = ( 𝑅 ‘ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
11 1 lnopfi ⊢ 𝑅 : ℋ ⟶ ℋ
12 11 2 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 ∘ 𝑆 ) ‘ 𝑥 ) = ( 𝑅 ‘ ( 𝑆 ‘ 𝑥 ) ) )
13 11 3 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 ∘ 𝑇 ) ‘ 𝑥 ) = ( 𝑅 ‘ ( 𝑇 ‘ 𝑥 ) ) )
14 12 13 oveq12d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 ∘ 𝑆 ) ‘ 𝑥 ) −ℎ ( ( 𝑅 ∘ 𝑇 ) ‘ 𝑥 ) ) = ( ( 𝑅 ‘ ( 𝑆 ‘ 𝑥 ) ) −ℎ ( 𝑅 ‘ ( 𝑇 ‘ 𝑥 ) ) ) )
15 7 10 14 3eqtr4d ⊢ ( 𝑥 ∈ ℋ → ( 𝑅 ‘ ( ( 𝑆 −op 𝑇 ) ‘ 𝑥 ) ) = ( ( ( 𝑅 ∘ 𝑆 ) ‘ 𝑥 ) −ℎ ( ( 𝑅 ∘ 𝑇 ) ‘ 𝑥 ) ) )
16 2 3 hosubcli ⊢ ( 𝑆 −op 𝑇 ) : ℋ ⟶ ℋ
17 11 16 hocoi ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) ‘ 𝑥 ) = ( 𝑅 ‘ ( ( 𝑆 −op 𝑇 ) ‘ 𝑥 ) ) )
18 11 2 hocofi ⊢ ( 𝑅 ∘ 𝑆 ) : ℋ ⟶ ℋ
19 11 3 hocofi ⊢ ( 𝑅 ∘ 𝑇 ) : ℋ ⟶ ℋ
20 hodval ⊢ ( ( ( 𝑅 ∘ 𝑆 ) : ℋ ⟶ ℋ ∧ ( 𝑅 ∘ 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅 ∘ 𝑆 ) ‘ 𝑥 ) −ℎ ( ( 𝑅 ∘ 𝑇 ) ‘ 𝑥 ) ) )
21 18 19 20 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅 ∘ 𝑆 ) ‘ 𝑥 ) −ℎ ( ( 𝑅 ∘ 𝑇 ) ‘ 𝑥 ) ) )
22 15 17 21 3eqtr4d ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) ) ‘ 𝑥 ) )
23 22 rgen ⊢ ∀ 𝑥 ∈ ℋ ( ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) ) ‘ 𝑥 )
24 11 16 hocofi ⊢ ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) : ℋ ⟶ ℋ
25 18 19 hosubcli ⊢ ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) ) : ℋ ⟶ ℋ
26 24 25 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) ) ‘ 𝑥 ) ↔ ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) = ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) ) )
27 23 26 mpbi ⊢ ( 𝑅 ∘ ( 𝑆 −op 𝑇 ) ) = ( ( 𝑅 ∘ 𝑆 ) −op ( 𝑅 ∘ 𝑇 ) )