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

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 
|- R : ~H --> ~H
hods.2 
|- S : ~H --> ~H
hods.3 
|- T : ~H --> ~H
Assertion hocadddiri 
|- ( ( R +op S ) o. T ) = ( ( R o. T ) +op ( S o. 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 1 2 hoaddcli 
 |-  ( R +op S ) : ~H --> ~H
5 4 3 hocoi 
 |-  ( x e. ~H -> ( ( ( R +op S ) o. T ) ` x ) = ( ( R +op S ) ` ( T ` x ) ) )
6 1 3 hocofi 
 |-  ( R o. T ) : ~H --> ~H
7 2 3 hocofi 
 |-  ( S o. T ) : ~H --> ~H
8 hosval 
 |-  ( ( ( R o. T ) : ~H --> ~H /\ ( S o. T ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( R o. T ) +op ( S o. T ) ) ` x ) = ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) )
9 6 7 8 mp3an12 
 |-  ( x e. ~H -> ( ( ( R o. T ) +op ( S o. T ) ) ` x ) = ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) )
10 3 ffvelcdmi 
 |-  ( x e. ~H -> ( T ` x ) e. ~H )
11 hosval 
 |-  ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ ( T ` x ) e. ~H ) -> ( ( R +op S ) ` ( T ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) )
12 1 2 11 mp3an12 
 |-  ( ( T ` x ) e. ~H -> ( ( R +op S ) ` ( T ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) )
13 10 12 syl 
 |-  ( x e. ~H -> ( ( R +op S ) ` ( T ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) )
14 1 3 hocoi 
 |-  ( x e. ~H -> ( ( R o. T ) ` x ) = ( R ` ( T ` x ) ) )
15 2 3 hocoi 
 |-  ( x e. ~H -> ( ( S o. T ) ` x ) = ( S ` ( T ` x ) ) )
16 14 15 oveq12d 
 |-  ( x e. ~H -> ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) = ( ( R ` ( T ` x ) ) +h ( S ` ( T ` x ) ) ) )
17 13 16 eqtr4d 
 |-  ( x e. ~H -> ( ( R +op S ) ` ( T ` x ) ) = ( ( ( R o. T ) ` x ) +h ( ( S o. T ) ` x ) ) )
18 9 17 eqtr4d 
 |-  ( x e. ~H -> ( ( ( R o. T ) +op ( S o. T ) ) ` x ) = ( ( R +op S ) ` ( T ` x ) ) )
19 5 18 eqtr4d 
 |-  ( x e. ~H -> ( ( ( R +op S ) o. T ) ` x ) = ( ( ( R o. T ) +op ( S o. T ) ) ` x ) )
20 19 rgen 
 |-  A. x e. ~H ( ( ( R +op S ) o. T ) ` x ) = ( ( ( R o. T ) +op ( S o. T ) ) ` x )
21 4 3 hocofi 
 |-  ( ( R +op S ) o. T ) : ~H --> ~H
22 6 7 hoaddcli 
 |-  ( ( R o. T ) +op ( S o. T ) ) : ~H --> ~H
23 21 22 hoeqi 
 |-  ( A. x e. ~H ( ( ( R +op S ) o. T ) ` x ) = ( ( ( R o. T ) +op ( S o. T ) ) ` x ) <-> ( ( R +op S ) o. T ) = ( ( R o. T ) +op ( S o. T ) ) )
24 20 23 mpbi 
 |-  ( ( R +op S ) o. T ) = ( ( R o. T ) +op ( S o. T ) )