Metamath Proof Explorer

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

Ref Expression
`|- ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( ( A .op T ) : ~H --> ~H /\ ( A .op U ) : ~H --> ~H ) -> ( ( A .op T ) +op ( A .op U ) ) : ~H --> ~H )`
` |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ ( A e. CC /\ U : ~H --> ~H ) ) -> ( ( A .op T ) +op ( A .op U ) ) : ~H --> ~H )`
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( A .op T ) +op ( A .op U ) ) : ~H --> ~H )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( A e. CC /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( A .op ( T +op U ) ) = ( ( A .op T ) +op ( A .op U ) ) )`