# Metamath Proof Explorer

## Theorem hoddii

Description: Distributive law for Hilbert space operator difference. (Interestingly, the reverse distributive law hocsubdiri does not require linearity.) (Contributed by NM, 11-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hoddi.1
`|- R e. LinOp`
hoddi.2
`|- S : ~H --> ~H`
hoddi.3
`|- T : ~H --> ~H`
Assertion hoddii
`|- ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) )`

### Proof

Step Hyp Ref Expression
1 hoddi.1
` |-  R e. LinOp`
2 hoddi.2
` |-  S : ~H --> ~H`
3 hoddi.3
` |-  T : ~H --> ~H`
4 2 ffvelrni
` |-  ( x e. ~H -> ( S ` x ) e. ~H )`
5 3 ffvelrni
` |-  ( x e. ~H -> ( T ` x ) e. ~H )`
6 1 lnopsubi
` |-  ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( R ` ( ( S ` x ) -h ( T ` x ) ) ) = ( ( R ` ( S ` x ) ) -h ( R ` ( T ` x ) ) ) )`
7 4 5 6 syl2anc
` |-  ( x e. ~H -> ( R ` ( ( S ` x ) -h ( T ` x ) ) ) = ( ( R ` ( S ` x ) ) -h ( R ` ( T ` x ) ) ) )`
8 hodval
` |-  ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S -op T ) ` x ) = ( ( S ` x ) -h ( T ` x ) ) )`
9 2 3 8 mp3an12
` |-  ( x e. ~H -> ( ( S -op T ) ` x ) = ( ( S ` x ) -h ( T ` x ) ) )`
10 9 fveq2d
` |-  ( x e. ~H -> ( R ` ( ( S -op T ) ` x ) ) = ( R ` ( ( S ` x ) -h ( T ` x ) ) ) )`
11 1 lnopfi
` |-  R : ~H --> ~H`
12 11 2 hocoi
` |-  ( x e. ~H -> ( ( R o. S ) ` x ) = ( R ` ( S ` x ) ) )`
13 11 3 hocoi
` |-  ( x e. ~H -> ( ( R o. T ) ` x ) = ( R ` ( T ` x ) ) )`
14 12 13 oveq12d
` |-  ( x e. ~H -> ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) = ( ( R ` ( S ` x ) ) -h ( R ` ( T ` x ) ) ) )`
15 7 10 14 3eqtr4d
` |-  ( x e. ~H -> ( R ` ( ( S -op T ) ` x ) ) = ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) )`
16 2 3 hosubcli
` |-  ( S -op T ) : ~H --> ~H`
17 11 16 hocoi
` |-  ( x e. ~H -> ( ( R o. ( S -op T ) ) ` x ) = ( R ` ( ( S -op T ) ` x ) ) )`
18 11 2 hocofi
` |-  ( R o. S ) : ~H --> ~H`
19 11 3 hocofi
` |-  ( R o. T ) : ~H --> ~H`
20 hodval
` |-  ( ( ( R o. S ) : ~H --> ~H /\ ( R o. T ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( R o. S ) -op ( R o. T ) ) ` x ) = ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) )`
21 18 19 20 mp3an12
` |-  ( x e. ~H -> ( ( ( R o. S ) -op ( R o. T ) ) ` x ) = ( ( ( R o. S ) ` x ) -h ( ( R o. T ) ` x ) ) )`
22 15 17 21 3eqtr4d
` |-  ( x e. ~H -> ( ( R o. ( S -op T ) ) ` x ) = ( ( ( R o. S ) -op ( R o. T ) ) ` x ) )`
23 22 rgen
` |-  A. x e. ~H ( ( R o. ( S -op T ) ) ` x ) = ( ( ( R o. S ) -op ( R o. T ) ) ` x )`
24 11 16 hocofi
` |-  ( R o. ( S -op T ) ) : ~H --> ~H`
25 18 19 hosubcli
` |-  ( ( R o. S ) -op ( R o. T ) ) : ~H --> ~H`
26 24 25 hoeqi
` |-  ( A. x e. ~H ( ( R o. ( S -op T ) ) ` x ) = ( ( ( R o. S ) -op ( R o. T ) ) ` x ) <-> ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) ) )`
27 23 26 mpbi
` |-  ( R o. ( S -op T ) ) = ( ( R o. S ) -op ( R o. T ) )`