Metamath Proof Explorer

Theorem pjddii

Description: Distributive law for Hilbert space operator difference. (Contributed by NM, 24-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 pjddii 
|- ( ( 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 )
6 1 pjsubi 
 |-  ( ( ( 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 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 -> ( ( 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 ) ) )
16 2 3 hosubcli 
 |-  ( 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 hodval 
 |-  ( ( ( ( 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
25 18 19 hosubcli 
 |-  ( ( ( projh ` H ) o. S ) -op ( ( projh ` H ) o. T ) ) : ~H --> ~H
26 24 25 hoeqi 
 |-  ( 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 ) ) )
27 23 26 mpbi 
 |-  ( ( projh ` H ) o. ( S -op T ) ) = ( ( ( projh ` H ) o. S ) -op ( ( projh ` H ) o. T ) )