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:1·opT=T

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 homval 1T:x1·opTx=1Tx
3 1 2 mp3an1 T:x1·opTx=1Tx
4 ffvelrn T:xTx
5 ax-hvmulid Tx1Tx=Tx
6 4 5 syl T:x1Tx=Tx
7 3 6 eqtrd T:x1·opTx=Tx
8 7 ralrimiva T:x1·opTx=Tx
9 homulcl 1T:1·opT:
10 1 9 mpan T:1·opT:
11 hoeq 1·opT:T:x1·opTx=Tx1·opT=T
12 10 11 mpancom T:x1·opTx=Tx1·opT=T
13 8 12 mpbid T:1·opT=T