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}:ℋ⟶ℋ\to 1{·}_{\mathrm{op}}{T}={T}$

Proof

Step Hyp Ref Expression
1 ax-1cn ${⊢}1\in ℂ$
2 homval ${⊢}\left(1\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(1{·}_{\mathrm{op}}{T}\right)\left({x}\right)=1{\cdot }_{ℎ}{T}\left({x}\right)$
3 1 2 mp3an1 ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(1{·}_{\mathrm{op}}{T}\right)\left({x}\right)=1{\cdot }_{ℎ}{T}\left({x}\right)$
4 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
5 ax-hvmulid ${⊢}{T}\left({x}\right)\in ℋ\to 1{\cdot }_{ℎ}{T}\left({x}\right)={T}\left({x}\right)$
6 4 5 syl ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to 1{\cdot }_{ℎ}{T}\left({x}\right)={T}\left({x}\right)$
7 3 6 eqtrd ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(1{·}_{\mathrm{op}}{T}\right)\left({x}\right)={T}\left({x}\right)$
8 7 ralrimiva ${⊢}{T}:ℋ⟶ℋ\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(1{·}_{\mathrm{op}}{T}\right)\left({x}\right)={T}\left({x}\right)$
9 homulcl ${⊢}\left(1\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left(1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
10 1 9 mpan ${⊢}{T}:ℋ⟶ℋ\to \left(1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
11 hoeq ${⊢}\left(\left(1{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {T}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(1{·}_{\mathrm{op}}{T}\right)\left({x}\right)={T}\left({x}\right)↔1{·}_{\mathrm{op}}{T}={T}\right)$
12 10 11 mpancom ${⊢}{T}:ℋ⟶ℋ\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(1{·}_{\mathrm{op}}{T}\right)\left({x}\right)={T}\left({x}\right)↔1{·}_{\mathrm{op}}{T}={T}\right)$
13 8 12 mpbid ${⊢}{T}:ℋ⟶ℋ\to 1{·}_{\mathrm{op}}{T}={T}$