Metamath Proof Explorer

Theorem hoaddassi

Description: Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hods.1 ⊢ 𝑅 : ℋ ⟶ ℋ
2 hods.2 ⊢ 𝑆 : ℋ ⟶ ℋ
3 hods.3 ⊢ 𝑇 : ℋ ⟶ ℋ
4 hosval ⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑅 +op 𝑆 ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) )
5 1 2 4 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 +op 𝑆 ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) )
6 5 oveq1d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 +op 𝑆 ) ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( ( ( 𝑅 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
7 1 2 hoaddcli ⊢ ( 𝑅 +op 𝑆 ) : ℋ ⟶ ℋ
8 hosval ⊢ ( ( ( 𝑅 +op 𝑆 ) : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) ‘ 𝑥 ) = ( ( ( 𝑅 +op 𝑆 ) ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
9 7 3 8 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) ‘ 𝑥 ) = ( ( ( 𝑅 +op 𝑆 ) ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
10 hosval ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
11 2 3 10 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
12 11 oveq2d ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 ‘ 𝑥 ) +ℎ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) = ( ( 𝑅 ‘ 𝑥 ) +ℎ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
13 2 3 hoaddcli ⊢ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
14 hosval ⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) +ℎ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) )
15 1 13 14 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) = ( ( 𝑅 ‘ 𝑥 ) +ℎ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) ) )
16 1 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑅 ‘ 𝑥 ) ∈ ℋ )
17 2 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
18 3 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
19 ax-hvass ⊢ ( ( ( 𝑅 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( ( 𝑅 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑅 ‘ 𝑥 ) +ℎ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
20 16 17 18 19 syl3anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑅 ‘ 𝑥 ) +ℎ ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
21 12 15 20 3eqtr4d ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) = ( ( ( 𝑅 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
22 6 9 21 3eqtr4d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) )
23 22 rgen ⊢ ∀ 𝑥 ∈ ℋ ( ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 )
24 7 3 hoaddcli ⊢ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) : ℋ ⟶ ℋ
25 1 13 hoaddcli ⊢ ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) : ℋ ⟶ ℋ
26 24 25 hoeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) ‘ 𝑥 ) ↔ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) )
27 23 26 mpbi ⊢ ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( 𝑅 +op ( 𝑆 +op 𝑇 ) )