Metamath Proof Explorer


Theorem hocadddiri

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

Ref Expression
Hypotheses hods.1 𝑅 : ℋ ⟶ ℋ
hods.2 𝑆 : ℋ ⟶ ℋ
hods.3 𝑇 : ℋ ⟶ ℋ
Assertion hocadddiri ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) = ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) )

Proof

Step Hyp Ref Expression
1 hods.1 𝑅 : ℋ ⟶ ℋ
2 hods.2 𝑆 : ℋ ⟶ ℋ
3 hods.3 𝑇 : ℋ ⟶ ℋ
4 1 2 hoaddcli ( 𝑅 +op 𝑆 ) : ℋ ⟶ ℋ
5 4 3 hocoi ( 𝑥 ∈ ℋ → ( ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) ‘ 𝑥 ) = ( ( 𝑅 +op 𝑆 ) ‘ ( 𝑇𝑥 ) ) )
6 1 3 hocofi ( 𝑅𝑇 ) : ℋ ⟶ ℋ
7 2 3 hocofi ( 𝑆𝑇 ) : ℋ ⟶ ℋ
8 hosval ( ( ( 𝑅𝑇 ) : ℋ ⟶ ℋ ∧ ( 𝑆𝑇 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅𝑇 ) ‘ 𝑥 ) + ( ( 𝑆𝑇 ) ‘ 𝑥 ) ) )
9 6 7 8 mp3an12 ( 𝑥 ∈ ℋ → ( ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅𝑇 ) ‘ 𝑥 ) + ( ( 𝑆𝑇 ) ‘ 𝑥 ) ) )
10 3 ffvelrni ( 𝑥 ∈ ℋ → ( 𝑇𝑥 ) ∈ ℋ )
11 hosval ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ ( 𝑇𝑥 ) ∈ ℋ ) → ( ( 𝑅 +op 𝑆 ) ‘ ( 𝑇𝑥 ) ) = ( ( 𝑅 ‘ ( 𝑇𝑥 ) ) + ( 𝑆 ‘ ( 𝑇𝑥 ) ) ) )
12 1 2 11 mp3an12 ( ( 𝑇𝑥 ) ∈ ℋ → ( ( 𝑅 +op 𝑆 ) ‘ ( 𝑇𝑥 ) ) = ( ( 𝑅 ‘ ( 𝑇𝑥 ) ) + ( 𝑆 ‘ ( 𝑇𝑥 ) ) ) )
13 10 12 syl ( 𝑥 ∈ ℋ → ( ( 𝑅 +op 𝑆 ) ‘ ( 𝑇𝑥 ) ) = ( ( 𝑅 ‘ ( 𝑇𝑥 ) ) + ( 𝑆 ‘ ( 𝑇𝑥 ) ) ) )
14 1 3 hocoi ( 𝑥 ∈ ℋ → ( ( 𝑅𝑇 ) ‘ 𝑥 ) = ( 𝑅 ‘ ( 𝑇𝑥 ) ) )
15 2 3 hocoi ( 𝑥 ∈ ℋ → ( ( 𝑆𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ ( 𝑇𝑥 ) ) )
16 14 15 oveq12d ( 𝑥 ∈ ℋ → ( ( ( 𝑅𝑇 ) ‘ 𝑥 ) + ( ( 𝑆𝑇 ) ‘ 𝑥 ) ) = ( ( 𝑅 ‘ ( 𝑇𝑥 ) ) + ( 𝑆 ‘ ( 𝑇𝑥 ) ) ) )
17 13 16 eqtr4d ( 𝑥 ∈ ℋ → ( ( 𝑅 +op 𝑆 ) ‘ ( 𝑇𝑥 ) ) = ( ( ( 𝑅𝑇 ) ‘ 𝑥 ) + ( ( 𝑆𝑇 ) ‘ 𝑥 ) ) )
18 9 17 eqtr4d ( 𝑥 ∈ ℋ → ( ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) ‘ 𝑥 ) = ( ( 𝑅 +op 𝑆 ) ‘ ( 𝑇𝑥 ) ) )
19 5 18 eqtr4d ( 𝑥 ∈ ℋ → ( ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) ‘ 𝑥 ) = ( ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) ‘ 𝑥 ) )
20 19 rgen 𝑥 ∈ ℋ ( ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) ‘ 𝑥 ) = ( ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) ‘ 𝑥 )
21 4 3 hocofi ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) : ℋ ⟶ ℋ
22 6 7 hoaddcli ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) : ℋ ⟶ ℋ
23 21 22 hoeqi ( ∀ 𝑥 ∈ ℋ ( ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) ‘ 𝑥 ) = ( ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) ‘ 𝑥 ) ↔ ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) = ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) ) )
24 20 23 mpbi ( ( 𝑅 +op 𝑆 ) ∘ 𝑇 ) = ( ( 𝑅𝑇 ) +op ( 𝑆𝑇 ) )