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 ( 𝑆 ∘ 𝑇 ) )