# Metamath Proof Explorer

## Theorem pjsdii

Description: Distributive law for Hilbert space operator sum. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjsdi.1
`|- H e. CH`
pjsdi.2
`|- S : ~H --> ~H`
pjsdi.3
`|- T : ~H --> ~H`
Assertion pjsdii
`|- ( ( projh ` H ) o. ( S +op T ) ) = ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) )`

### Proof

Step Hyp Ref Expression
1 pjsdi.1
` |-  H e. CH`
2 pjsdi.2
` |-  S : ~H --> ~H`
3 pjsdi.3
` |-  T : ~H --> ~H`
4 2 ffvelrni
` |-  ( x e. ~H -> ( S ` x ) e. ~H )`
5 3 ffvelrni
` |-  ( x e. ~H -> ( T ` x ) e. ~H )`
` |-  ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( ( projh ` H ) ` ( ( S ` x ) +h ( T ` x ) ) ) = ( ( ( projh ` H ) ` ( S ` x ) ) +h ( ( projh ` H ) ` ( T ` x ) ) ) )`
7 4 5 6 syl2anc
` |-  ( x e. ~H -> ( ( projh ` H ) ` ( ( S ` x ) +h ( T ` x ) ) ) = ( ( ( projh ` H ) ` ( S ` x ) ) +h ( ( projh ` H ) ` ( T ` x ) ) ) )`
8 hosval
` |-  ( ( 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 -> ( ( projh ` H ) ` ( ( S +op T ) ` x ) ) = ( ( projh ` H ) ` ( ( S ` x ) +h ( T ` x ) ) ) )`
11 1 pjfi
` |-  ( projh ` H ) : ~H --> ~H`
12 11 2 hocoi
` |-  ( x e. ~H -> ( ( ( projh ` H ) o. S ) ` x ) = ( ( projh ` H ) ` ( S ` x ) ) )`
13 11 3 hocoi
` |-  ( x e. ~H -> ( ( ( projh ` H ) o. T ) ` x ) = ( ( projh ` H ) ` ( T ` x ) ) )`
14 12 13 oveq12d
` |-  ( x e. ~H -> ( ( ( ( projh ` H ) o. S ) ` x ) +h ( ( ( projh ` H ) o. T ) ` x ) ) = ( ( ( projh ` H ) ` ( S ` x ) ) +h ( ( projh ` H ) ` ( T ` x ) ) ) )`
15 7 10 14 3eqtr4d
` |-  ( x e. ~H -> ( ( projh ` H ) ` ( ( S +op T ) ` x ) ) = ( ( ( ( projh ` H ) o. S ) ` x ) +h ( ( ( projh ` H ) o. T ) ` x ) ) )`
` |-  ( S +op T ) : ~H --> ~H`
17 11 16 hocoi
` |-  ( x e. ~H -> ( ( ( projh ` H ) o. ( S +op T ) ) ` x ) = ( ( projh ` H ) ` ( ( S +op T ) ` x ) ) )`
18 11 2 hocofi
` |-  ( ( projh ` H ) o. S ) : ~H --> ~H`
19 11 3 hocofi
` |-  ( ( projh ` H ) o. T ) : ~H --> ~H`
20 hosval
` |-  ( ( ( ( projh ` H ) o. S ) : ~H --> ~H /\ ( ( projh ` H ) o. T ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) ) ` x ) = ( ( ( ( projh ` H ) o. S ) ` x ) +h ( ( ( projh ` H ) o. T ) ` x ) ) )`
21 18 19 20 mp3an12
` |-  ( x e. ~H -> ( ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) ) ` x ) = ( ( ( ( projh ` H ) o. S ) ` x ) +h ( ( ( projh ` H ) o. T ) ` x ) ) )`
22 15 17 21 3eqtr4d
` |-  ( x e. ~H -> ( ( ( projh ` H ) o. ( S +op T ) ) ` x ) = ( ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) ) ` x ) )`
23 22 rgen
` |-  A. x e. ~H ( ( ( projh ` H ) o. ( S +op T ) ) ` x ) = ( ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) ) ` x )`
24 11 16 hocofi
` |-  ( ( projh ` H ) o. ( S +op T ) ) : ~H --> ~H`
` |-  ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) ) : ~H --> ~H`
` |-  ( A. x e. ~H ( ( ( projh ` H ) o. ( S +op T ) ) ` x ) = ( ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) ) ` x ) <-> ( ( projh ` H ) o. ( S +op T ) ) = ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) ) )`
` |-  ( ( projh ` H ) o. ( S +op T ) ) = ( ( ( projh ` H ) o. S ) +op ( ( projh ` H ) o. T ) )`