# 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 ) ) ) )`
` |-  ( ( ( 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 ) ) )`