Metamath Proof Explorer

Theorem hoadddi

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

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> A e. CC )
2 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
3 2 3ad2antl2 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( T ` x ) e. ~H )
4 ffvelrn 
 |-  ( ( U : ~H --> ~H /\ x e. ~H ) -> ( U ` x ) e. ~H )
5 4 3ad2antl3 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( U ` x ) e. ~H )
6 ax-hvdistr1 
 |-  ( ( A e. CC /\ ( T ` x ) e. ~H /\ ( U ` x ) e. ~H ) -> ( A .h ( ( T ` x ) +h ( U ` x ) ) ) = ( ( A .h ( T ` x ) ) +h ( A .h ( U ` x ) ) ) )
7 1 3 5 6 syl3anc 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( ( T ` x ) +h ( U ` x ) ) ) = ( ( A .h ( T ` x ) ) +h ( A .h ( U ` x ) ) ) )
8 hosval 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( T +op U ) ` x ) = ( ( T ` x ) +h ( U ` x ) ) )
9 8 oveq2d 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( A .h ( ( T +op U ) ` x ) ) = ( A .h ( ( T ` x ) +h ( U ` x ) ) ) )
10 9 3expa 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( ( T +op U ) ` x ) ) = ( A .h ( ( T ` x ) +h ( U ` x ) ) ) )
11 10 3adantl1 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( ( T +op U ) ` x ) ) = ( A .h ( ( T ` x ) +h ( U ` x ) ) ) )
12 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
13 12 3expa 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
14 13 3adantl3 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
15 homval 
 |-  ( ( A e. CC /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( A .op U ) ` x ) = ( A .h ( U ` x ) ) )
16 15 3expa 
 |-  ( ( ( A e. CC /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op U ) ` x ) = ( A .h ( U ` x ) ) )
17 16 3adantl2 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op U ) ` x ) = ( A .h ( U ` x ) ) )
18 14 17 oveq12d 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) ` x ) +h ( ( A .op U ) ` x ) ) = ( ( A .h ( T ` x ) ) +h ( A .h ( U ` x ) ) ) )
19 7 11 18 3eqtr4d 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( ( T +op U ) ` x ) ) = ( ( ( A .op T ) ` x ) +h ( ( A .op U ) ` x ) ) )
20 hoaddcl 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op U ) : ~H --> ~H )
21 20 anim2i 
 |-  ( ( A e. CC /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( A e. CC /\ ( T +op U ) : ~H --> ~H ) )
22 21 3impb 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A e. CC /\ ( T +op U ) : ~H --> ~H ) )
23 homval 
 |-  ( ( A e. CC /\ ( T +op U ) : ~H --> ~H /\ x e. ~H ) -> ( ( A .op ( T +op U ) ) ` x ) = ( A .h ( ( T +op U ) ` x ) ) )
24 23 3expa 
 |-  ( ( ( A e. CC /\ ( T +op U ) : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op ( T +op U ) ) ` x ) = ( A .h ( ( T +op U ) ` x ) ) )
25 22 24 sylan 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op ( T +op U ) ) ` x ) = ( A .h ( ( T +op U ) ` x ) ) )
26 homulcl 
 |-  ( ( A e. CC /\ T : ~H --> ~H ) -> ( A .op T ) : ~H --> ~H )
27 homulcl 
 |-  ( ( A e. CC /\ U : ~H --> ~H ) -> ( A .op U ) : ~H --> ~H )
28 26 27 anim12i 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( A e. CC /\ U : ~H --> ~H ) ) -> ( ( A .op T ) : ~H --> ~H /\ ( A .op U ) : ~H --> ~H ) )
29 28 3impdi 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( A .op T ) : ~H --> ~H /\ ( A .op U ) : ~H --> ~H ) )
30 hosval 
 |-  ( ( ( A .op T ) : ~H --> ~H /\ ( A .op U ) : ~H --> ~H /\ x e. ~H ) -> ( ( ( A .op T ) +op ( A .op U ) ) ` x ) = ( ( ( A .op T ) ` x ) +h ( ( A .op U ) ` x ) ) )
31 30 3expa 
 |-  ( ( ( ( A .op T ) : ~H --> ~H /\ ( A .op U ) : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) +op ( A .op U ) ) ` x ) = ( ( ( A .op T ) ` x ) +h ( ( A .op U ) ` x ) ) )
32 29 31 sylan 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) +op ( A .op U ) ) ` x ) = ( ( ( A .op T ) ` x ) +h ( ( A .op U ) ` x ) ) )
33 19 25 32 3eqtr4d 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op ( T +op U ) ) ` x ) = ( ( ( A .op T ) +op ( A .op U ) ) ` x ) )
34 33 ralrimiva 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> A. x e. ~H ( ( A .op ( T +op U ) ) ` x ) = ( ( ( A .op T ) +op ( A .op U ) ) ` x ) )
35 homulcl 
 |-  ( ( A e. CC /\ ( T +op U ) : ~H --> ~H ) -> ( A .op ( T +op U ) ) : ~H --> ~H )
36 20 35 sylan2 
 |-  ( ( A e. CC /\ ( T : ~H --> ~H /\ U : ~H --> ~H ) ) -> ( A .op ( T +op U ) ) : ~H --> ~H )
37 36 3impb 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op U ) ) : ~H --> ~H )
38 hoaddcl 
 |-  ( ( ( A .op T ) : ~H --> ~H /\ ( A .op U ) : ~H --> ~H ) -> ( ( A .op T ) +op ( A .op U ) ) : ~H --> ~H )
39 26 27 38 syl2an 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( A e. CC /\ U : ~H --> ~H ) ) -> ( ( A .op T ) +op ( A .op U ) ) : ~H --> ~H )
40 39 3impdi 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( A .op T ) +op ( A .op U ) ) : ~H --> ~H )
41 hoeq 
 |-  ( ( ( A .op ( T +op U ) ) : ~H --> ~H /\ ( ( A .op T ) +op ( A .op U ) ) : ~H --> ~H ) -> ( A. x e. ~H ( ( A .op ( T +op U ) ) ` x ) = ( ( ( A .op T ) +op ( A .op U ) ) ` x ) <-> ( A .op ( T +op U ) ) = ( ( A .op T ) +op ( A .op U ) ) ) )
42 37 40 41 syl2anc 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A. x e. ~H ( ( A .op ( T +op U ) ) ` x ) = ( ( ( A .op T ) +op ( A .op U ) ) ` x ) <-> ( A .op ( T +op U ) ) = ( ( A .op T ) +op ( A .op U ) ) ) )
43 34 42 mpbid 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op U ) ) = ( ( A .op T ) +op ( A .op U ) ) )