# Metamath Proof Explorer

## Theorem homco1

Description: Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

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

### Proof

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