# Metamath Proof Explorer

## Theorem hocsubdiri

Description: Distributive law for Hilbert space operator difference. (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 hocsubdiri
`|- ( ( 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 hosubcli
` |-  ( 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 hodval
` |-  ( ( ( 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 ffvelrni
` |-  ( x e. ~H -> ( T ` x ) e. ~H )`
11 hodval
` |-  ( ( 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 hosubcli
` |-  ( ( 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 ) )`