# 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
`|- R : ~H --> ~H`
hods.2
`|- S : ~H --> ~H`
hods.3
`|- T : ~H --> ~H`
Assertion hoaddassi
`|- ( ( R +op S ) +op T ) = ( R +op ( S +op T ) )`

### Proof

Step Hyp Ref Expression
1 hods.1
` |-  R : ~H --> ~H`
2 hods.2
` |-  S : ~H --> ~H`
3 hods.3
` |-  T : ~H --> ~H`
4 hosval
` |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ x e. ~H ) -> ( ( R +op S ) ` x ) = ( ( R ` x ) +h ( S ` x ) ) )`
5 1 2 4 mp3an12
` |-  ( x e. ~H -> ( ( R +op S ) ` x ) = ( ( R ` x ) +h ( S ` x ) ) )`
6 5 oveq1d
` |-  ( x e. ~H -> ( ( ( R +op S ) ` x ) +h ( T ` x ) ) = ( ( ( R ` x ) +h ( S ` x ) ) +h ( T ` x ) ) )`
7 1 2 hoaddcli
` |-  ( R +op S ) : ~H --> ~H`
8 hosval
` |-  ( ( ( R +op S ) : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( ( R +op S ) +op T ) ` x ) = ( ( ( R +op S ) ` x ) +h ( T ` x ) ) )`
9 7 3 8 mp3an12
` |-  ( x e. ~H -> ( ( ( R +op S ) +op T ) ` x ) = ( ( ( R +op S ) ` x ) +h ( T ` x ) ) )`
10 hosval
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
11 2 3 10 mp3an12
` |-  ( x e. ~H -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )`
12 11 oveq2d
` |-  ( x e. ~H -> ( ( R ` x ) +h ( ( S +op T ) ` x ) ) = ( ( R ` x ) +h ( ( S ` x ) +h ( T ` x ) ) ) )`
13 2 3 hoaddcli
` |-  ( S +op T ) : ~H --> ~H`
14 hosval
` |-  ( ( R : ~H --> ~H /\ ( S +op T ) : ~H --> ~H /\ x e. ~H ) -> ( ( R +op ( S +op T ) ) ` x ) = ( ( R ` x ) +h ( ( S +op T ) ` x ) ) )`
15 1 13 14 mp3an12
` |-  ( x e. ~H -> ( ( R +op ( S +op T ) ) ` x ) = ( ( R ` x ) +h ( ( S +op T ) ` x ) ) )`
16 1 ffvelrni
` |-  ( x e. ~H -> ( R ` x ) e. ~H )`
17 2 ffvelrni
` |-  ( x e. ~H -> ( S ` x ) e. ~H )`
18 3 ffvelrni
` |-  ( x e. ~H -> ( T ` x ) e. ~H )`
19 ax-hvass
` |-  ( ( ( R ` x ) e. ~H /\ ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( ( ( R ` x ) +h ( S ` x ) ) +h ( T ` x ) ) = ( ( R ` x ) +h ( ( S ` x ) +h ( T ` x ) ) ) )`
20 16 17 18 19 syl3anc
` |-  ( x e. ~H -> ( ( ( R ` x ) +h ( S ` x ) ) +h ( T ` x ) ) = ( ( R ` x ) +h ( ( S ` x ) +h ( T ` x ) ) ) )`
21 12 15 20 3eqtr4d
` |-  ( x e. ~H -> ( ( R +op ( S +op T ) ) ` x ) = ( ( ( R ` x ) +h ( S ` x ) ) +h ( T ` x ) ) )`
22 6 9 21 3eqtr4d
` |-  ( x e. ~H -> ( ( ( R +op S ) +op T ) ` x ) = ( ( R +op ( S +op T ) ) ` x ) )`
23 22 rgen
` |-  A. x e. ~H ( ( ( R +op S ) +op T ) ` x ) = ( ( R +op ( S +op T ) ) ` x )`
24 7 3 hoaddcli
` |-  ( ( R +op S ) +op T ) : ~H --> ~H`
25 1 13 hoaddcli
` |-  ( R +op ( S +op T ) ) : ~H --> ~H`
26 24 25 hoeqi
` |-  ( A. x e. ~H ( ( ( R +op S ) +op T ) ` x ) = ( ( R +op ( S +op T ) ) ` x ) <-> ( ( R +op S ) +op T ) = ( R +op ( S +op T ) ) )`
27 23 26 mpbi
` |-  ( ( R +op S ) +op T ) = ( R +op ( S +op T ) )`