# Metamath Proof Explorer

## Theorem elunop2

Description: An operator is unitary iff it is linear, onto, and idempotent in the norm. Similar to theorem in AkhiezerGlazman p. 73, and its converse. (Contributed by NM, 24-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion elunop2 ${⊢}{T}\in \mathrm{UniOp}↔\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 unoplin ${⊢}{T}\in \mathrm{UniOp}\to {T}\in \mathrm{LinOp}$
2 elunop ${⊢}{T}\in \mathrm{UniOp}↔\left({T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}\right)$
3 2 simplbi ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{onto}{⟶}ℋ$
4 unopnorm ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\right)\to {norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)$
5 4 ralrimiva ${⊢}{T}\in \mathrm{UniOp}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)$
6 1 3 5 3jca ${⊢}{T}\in \mathrm{UniOp}\to \left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right)$
7 eleq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({T}\in \mathrm{UniOp}↔if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{UniOp}\right)$
8 eleq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({T}\in \mathrm{LinOp}↔if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\right)$
9 foeq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({T}:ℋ\underset{onto}{⟶}ℋ↔if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ\right)$
10 2fveq3 ${⊢}{x}={y}\to {norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({T}\left({y}\right)\right)$
11 fveq2 ${⊢}{x}={y}\to {norm}_{ℎ}\left({x}\right)={norm}_{ℎ}\left({y}\right)$
12 10 11 eqeq12d ${⊢}{x}={y}\to \left({norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)↔{norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
13 12 cbvralvw ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
14 fveq1 ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to {T}\left({y}\right)=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)$
15 14 fveqeq2d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)↔{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
16 15 ralbidv ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
17 13 16 syl5bb ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
18 8 9 17 3anbi123d ${⊢}{T}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right)↔\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)\right)$
19 eleq1 ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}↔if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\right)$
20 foeq1 ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\left({\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ↔if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ\right)$
21 fveq1 ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)$
22 21 fveqeq2d ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left({norm}_{ℎ}\left(\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)↔{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
23 22 ralbidv ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)↔\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
24 19 20 23 3anbi123d ${⊢}{\mathrm{I}↾}_{ℋ}=if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\to \left(\left({\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}\wedge \left({\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)↔\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)\right)$
25 idlnop ${⊢}{\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}$
26 f1oi ${⊢}\left({\mathrm{I}↾}_{ℋ}\right):ℋ\underset{1-1 onto}{⟶}ℋ$
27 f1ofo ${⊢}\left({\mathrm{I}↾}_{ℋ}\right):ℋ\underset{1-1 onto}{⟶}ℋ\to \left({\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ$
28 26 27 ax-mp ${⊢}\left({\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ$
29 fvresi ${⊢}{y}\in ℋ\to \left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)={y}$
30 29 fveq2d ${⊢}{y}\in ℋ\to {norm}_{ℎ}\left(\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
31 30 rgen ${⊢}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
32 25 28 31 3pm3.2i ${⊢}\left({\mathrm{I}↾}_{ℋ}\in \mathrm{LinOp}\wedge \left({\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(\left({\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
33 18 24 32 elimhyp ${⊢}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}\wedge if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ\wedge \forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)\right)$
34 33 simp1i ${⊢}if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{LinOp}$
35 33 simp2i ${⊢}if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right):ℋ\underset{onto}{⟶}ℋ$
36 33 simp3i ${⊢}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left(if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\left({y}\right)\right)={norm}_{ℎ}\left({y}\right)$
37 34 35 36 lnopunii ${⊢}if\left(\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right),{T},{\mathrm{I}↾}_{ℋ}\right)\in \mathrm{UniOp}$
38 7 37 dedth ${⊢}\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right)\to {T}\in \mathrm{UniOp}$
39 6 38 impbii ${⊢}{T}\in \mathrm{UniOp}↔\left({T}\in \mathrm{LinOp}\wedge {T}:ℋ\underset{onto}{⟶}ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{norm}_{ℎ}\left({T}\left({x}\right)\right)={norm}_{ℎ}\left({x}\right)\right)$