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 )