Metamath Proof Explorer

Theorem homulass

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

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

Proof

Step Hyp Ref Expression
1 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
2 homval 
 |-  ( ( ( A x. B ) e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( ( A x. B ) .op T ) ` x ) = ( ( A x. B ) .h ( T ` x ) ) )
3 1 2 syl3an1 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( ( A x. B ) .op T ) ` x ) = ( ( A x. B ) .h ( T ` x ) ) )
4 3 3expia 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ T : ~H --> ~H ) -> ( x e. ~H -> ( ( ( A x. B ) .op T ) ` x ) = ( ( A x. B ) .h ( T ` x ) ) ) )
5 4 3impa 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( x e. ~H -> ( ( ( A x. B ) .op T ) ` x ) = ( ( A x. B ) .h ( T ` x ) ) ) )
6 5 imp 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A x. B ) .op T ) ` x ) = ( ( A x. B ) .h ( T ` x ) ) )
7 homval 
 |-  ( ( B e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( B .op T ) ` x ) = ( B .h ( T ` x ) ) )
8 7 oveq2d 
 |-  ( ( B e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( A .h ( ( B .op T ) ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) )
9 8 3expa 
 |-  ( ( ( B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( ( B .op T ) ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) )
10 9 3adantl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( ( B .op T ) ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) )
11 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
12 ax-hvmulass 
 |-  ( ( A e. CC /\ B e. CC /\ ( T ` x ) e. ~H ) -> ( ( A x. B ) .h ( T ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) )
13 11 12 syl3an3 
 |-  ( ( A e. CC /\ B e. CC /\ ( T : ~H --> ~H /\ x e. ~H ) ) -> ( ( A x. B ) .h ( T ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) )
14 13 3expa 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( T : ~H --> ~H /\ x e. ~H ) ) -> ( ( A x. B ) .h ( T ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) )
15 14 exp43 
 |-  ( A e. CC -> ( B e. CC -> ( T : ~H --> ~H -> ( x e. ~H -> ( ( A x. B ) .h ( T ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) ) ) ) )
16 15 3imp1 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A x. B ) .h ( T ` x ) ) = ( A .h ( B .h ( T ` x ) ) ) )
17 10 16 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( A .h ( ( B .op T ) ` x ) ) = ( ( A x. B ) .h ( T ` x ) ) )
18 6 17 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A x. B ) .op T ) ` x ) = ( A .h ( ( B .op T ) ` x ) ) )
19 homulcl 
 |-  ( ( B e. CC /\ T : ~H --> ~H ) -> ( B .op T ) : ~H --> ~H )
20 homval 
 |-  ( ( A e. CC /\ ( B .op T ) : ~H --> ~H /\ x e. ~H ) -> ( ( A .op ( B .op T ) ) ` x ) = ( A .h ( ( B .op T ) ` x ) ) )
21 19 20 syl3an2 
 |-  ( ( A e. CC /\ ( B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op ( B .op T ) ) ` x ) = ( A .h ( ( B .op T ) ` x ) ) )
22 21 3expia 
 |-  ( ( A e. CC /\ ( B e. CC /\ T : ~H --> ~H ) ) -> ( x e. ~H -> ( ( A .op ( B .op T ) ) ` x ) = ( A .h ( ( B .op T ) ` x ) ) ) )
23 22 3impb 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( x e. ~H -> ( ( A .op ( B .op T ) ) ` x ) = ( A .h ( ( B .op T ) ` x ) ) ) )
24 23 imp 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op ( B .op T ) ) ` x ) = ( A .h ( ( B .op T ) ` x ) ) )
25 18 24 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A x. B ) .op T ) ` x ) = ( ( A .op ( B .op T ) ) ` x ) )
26 25 ralrimiva 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> A. x e. ~H ( ( ( A x. B ) .op T ) ` x ) = ( ( A .op ( B .op T ) ) ` x ) )
27 homulcl 
 |-  ( ( ( A x. B ) e. CC /\ T : ~H --> ~H ) -> ( ( A x. B ) .op T ) : ~H --> ~H )
28 1 27 stoic3 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A x. B ) .op T ) : ~H --> ~H )
29 homulcl 
 |-  ( ( A e. CC /\ ( B .op T ) : ~H --> ~H ) -> ( A .op ( B .op T ) ) : ~H --> ~H )
30 19 29 sylan2 
 |-  ( ( A e. CC /\ ( B e. CC /\ T : ~H --> ~H ) ) -> ( A .op ( B .op T ) ) : ~H --> ~H )
31 30 3impb 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( A .op ( B .op T ) ) : ~H --> ~H )
32 hoeq 
 |-  ( ( ( ( A x. B ) .op T ) : ~H --> ~H /\ ( A .op ( B .op T ) ) : ~H --> ~H ) -> ( A. x e. ~H ( ( ( A x. B ) .op T ) ` x ) = ( ( A .op ( B .op T ) ) ` x ) <-> ( ( A x. B ) .op T ) = ( A .op ( B .op T ) ) ) )
33 28 31 32 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( A. x e. ~H ( ( ( A x. B ) .op T ) ` x ) = ( ( A .op ( B .op T ) ) ` x ) <-> ( ( A x. B ) .op T ) = ( A .op ( B .op T ) ) ) )
34 26 33 mpbid 
 |-  ( ( A e. CC /\ B e. CC /\ T : ~H --> ~H ) -> ( ( A x. B ) .op T ) = ( A .op ( B .op T ) ) )