Metamath Proof Explorer

Theorem hoadddir

Description: Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoadddir 
|- ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A + B ) .op T ) = ( ( A .op T ) +op ( B .op T ) ) )

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
2 1 anim1i 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ T : ~H --> ~H ) -> ( ( A + B ) e. CC /\ T : ~H --> ~H ) )
3 2 3impa 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A + B ) e. CC /\ T : ~H --> ~H ) )
4 homval 
 |-  ( ( ( A + B ) e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( ( A + B ) .op T ) ` x ) = ( ( A + B ) .h ( T ` x ) ) )
5 4 3expa 
 |-  ( ( ( ( A + B ) e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A + B ) .op T ) ` x ) = ( ( A + B ) .h ( T ` x ) ) )
6 3 5 sylan 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A + B ) .op T ) ` x ) = ( ( A + B ) .h ( T ` x ) ) )
7 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
8 7 3expa 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
9 8 3adantl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
10 homval 
 |-  ( ( B e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( B .op T ) ` x ) = ( B .h ( T ` x ) ) )
11 10 3expa 
 |-  ( ( ( B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( B .op T ) ` x ) = ( B .h ( T ` x ) ) )
12 11 3adantl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( B .op T ) ` x ) = ( B .h ( T ` x ) ) )
13 9 12 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) ` x ) +h ( ( B .op T ) ` x ) ) = ( ( A .h ( T ` x ) ) +h ( B .h ( T ` x ) ) ) )
14 ffvelcdm 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
15 ax-hvdistr2 
 |-  ( ( A e. CC /\ B e. CC /\ ( T ` x ) e. ~H ) -> ( ( A + B ) .h ( T ` x ) ) = ( ( A .h ( T ` x ) ) +h ( B .h ( T ` x ) ) ) )
16 14 15 syl3an3 
 |-  ( ( A e. CC /\ B e. CC /\ ( T : ~H --> ~H /\ x e. ~H ) ) -> ( ( A + B ) .h ( T ` x ) ) = ( ( A .h ( T ` x ) ) +h ( B .h ( T ` x ) ) ) )
17 16 3exp 
 |-  ( A e. CC -> ( B e. CC -> ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( A + B ) .h ( T ` x ) ) = ( ( A .h ( T ` x ) ) +h ( B .h ( T ` x ) ) ) ) ) )
18 17 exp4a 
 |-  ( A e. CC -> ( B e. CC -> ( T : ~H --> ~H -> ( x e. ~H -> ( ( A + B ) .h ( T ` x ) ) = ( ( A .h ( T ` x ) ) +h ( B .h ( T ` x ) ) ) ) ) ) )
19 18 3imp1 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A + B ) .h ( T ` x ) ) = ( ( A .h ( T ` x ) ) +h ( B .h ( T ` x ) ) ) )
20 13 19 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) ` x ) +h ( ( B .op T ) ` x ) ) = ( ( A + B ) .h ( T ` x ) ) )
21 6 20 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A + B ) .op T ) ` x ) = ( ( ( A .op T ) ` x ) +h ( ( B .op T ) ` x ) ) )
22 homulcl 
 |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
23 homulcl 
 |-  ( ( B e. CC /\ T : ~H --> ~H ) -> ( B .op T ) : ~H --> ~H )
24 22 23 anim12i 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( B e. CC /\ T : ~H --> ~H ) ) -> ( ( A .op T ) : ~H --> ~H /\ ( B .op T ) : ~H --> ~H ) )
25 24 3impdir 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A .op T ) : ~H --> ~H /\ ( B .op T ) : ~H --> ~H ) )
26 hosval 
 |-  ( ( ( A .op T ) : ~H --> ~H /\ ( B .op T ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( A .op T ) +op ( B .op T ) ) ` x ) = ( ( ( A .op T ) ` x ) +h ( ( B .op T ) ` x ) ) )
27 26 3expa 
 |-  ( ( ( ( A .op T ) : ~H --> ~H /\ ( B .op T ) : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) +op ( B .op T ) ) ` x ) = ( ( ( A .op T ) ` x ) +h ( ( B .op T ) ` x ) ) )
28 25 27 sylan 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) +op ( B .op T ) ) ` x ) = ( ( ( A .op T ) ` x ) +h ( ( B .op T ) ` x ) ) )
29 21 28 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A + B ) .op T ) ` x ) = ( ( ( A .op T ) +op ( B .op T ) ) ` x ) )
30 29 ralrimiva 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> A. x e. ~H ( ( ( A + B ) .op T ) ` x ) = ( ( ( A .op T ) +op ( B .op T ) ) ` x ) )
31 homulcl 
 |-  ( ( ( A + B ) e. CC /\ T : ~H --> ~H ) -> ( ( A + B ) .op T ) : ~H --> ~H )
32 1 31 stoic3 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A + B ) .op T ) : ~H --> ~H )
33 hoaddcl 
 |-  ( ( ( A .op T ) : ~H --> ~H /\ ( B .op T ) : ~H --> ~H ) -> ( ( A .op T ) +op ( B .op T ) ) : ~H --> ~H )
34 22 23 33 syl2an 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( B e. CC /\ T : ~H --> ~H ) ) -> ( ( A .op T ) +op ( B .op T ) ) : ~H --> ~H )
35 34 3impdir 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A .op T ) +op ( B .op T ) ) : ~H --> ~H )
36 hoeq 
 |-  ( ( ( ( A + B ) .op T ) : ~H --> ~H /\ ( ( A .op T ) +op ( B .op T ) ) : ~H --> ~H ) -> ( A. x e. ~H ( ( ( A + B ) .op T ) ` x ) = ( ( ( A .op T ) +op ( B .op T ) ) ` x ) <-> ( ( A + B ) .op T ) = ( ( A .op T ) +op ( B .op T ) ) ) )
37 32 35 36 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( A. x e. ~H ( ( ( A + B ) .op T ) ` x ) = ( ( ( A .op T ) +op ( B .op T ) ) ` x ) <-> ( ( A + B ) .op T ) = ( ( A .op T ) +op ( B .op T ) ) ) )
38 30 37 mpbid 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A + B ) .op T ) = ( ( A .op T ) +op ( B .op T ) ) )