# Metamath Proof Explorer

## Theorem homulid2

Description: An operator equals its scalar product with one. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion homulid2
`|- ( T : ~H --> ~H -> ( 1 .op T ) = T )`

### Proof

Step Hyp Ref Expression
1 ax-1cn
` |-  1 e. CC`
2 homval
` |-  ( ( 1 e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( 1 .op T ) ` x ) = ( 1 .h ( T ` x ) ) )`
3 1 2 mp3an1
` |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( 1 .op T ) ` x ) = ( 1 .h ( T ` x ) ) )`
4 ffvelrn
` |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )`
5 ax-hvmulid
` |-  ( ( T ` x ) e. ~H -> ( 1 .h ( T ` x ) ) = ( T ` x ) )`
6 4 5 syl
` |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( 1 .h ( T ` x ) ) = ( T ` x ) )`
7 3 6 eqtrd
` |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( ( 1 .op T ) ` x ) = ( T ` x ) )`
8 7 ralrimiva
` |-  ( T : ~H --> ~H -> A. x e. ~H ( ( 1 .op T ) ` x ) = ( T ` x ) )`
9 homulcl
` |-  ( ( 1 e. CC /\ T : ~H --> ~H ) -> ( 1 .op T ) : ~H --> ~H )`
10 1 9 mpan
` |-  ( T : ~H --> ~H -> ( 1 .op T ) : ~H --> ~H )`
11 hoeq
` |-  ( ( ( 1 .op T ) : ~H --> ~H /\ T : ~H --> ~H ) -> ( A. x e. ~H ( ( 1 .op T ) ` x ) = ( T ` x ) <-> ( 1 .op T ) = T ) )`
12 10 11 mpancom
` |-  ( T : ~H --> ~H -> ( A. x e. ~H ( ( 1 .op T ) ` x ) = ( T ` x ) <-> ( 1 .op T ) = T ) )`
13 8 12 mpbid
` |-  ( T : ~H --> ~H -> ( 1 .op T ) = T )`