# Metamath Proof Explorer

## Theorem unopf1o

Description: A unitary operator in Hilbert space is one-to-one and onto. (Contributed by NM, 22-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion unopf1o ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{1-1 onto}{⟶}ℋ$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 simplbi ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{onto}{⟶}ℋ$
3 fof ${⊢}{T}:ℋ\underset{onto}{⟶}ℋ\to {T}:ℋ⟶ℋ$
4 2 3 syl ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ⟶ℋ$
5 unop ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{x}$
6 5 3anidm23 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{x}$
7 6 3adant3 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{x}$
8 unop ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={y}{\cdot }_{\mathrm{ih}}{y}$
9 8 3anidm23 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={y}{\cdot }_{\mathrm{ih}}{y}$
10 9 3adant2 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={y}{\cdot }_{\mathrm{ih}}{y}$
11 7 10 oveq12d ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{x}\right)+\left({y}{\cdot }_{\mathrm{ih}}{y}\right)$
12 unop ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)={x}{\cdot }_{\mathrm{ih}}{y}$
13 unop ${⊢}\left({T}\in \mathrm{UniOp}\wedge {y}\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)={y}{\cdot }_{\mathrm{ih}}{x}$
14 13 3com23 ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to {T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)={y}{\cdot }_{\mathrm{ih}}{x}$
15 12 14 oveq12d ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{y}\right)+\left({y}{\cdot }_{\mathrm{ih}}{x}\right)$
16 11 15 oveq12d ${⊢}\left({T}\in \mathrm{UniOp}\wedge {x}\in ℋ\wedge {y}\in ℋ\right)\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)-\left(\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{x}\right)+\left({y}{\cdot }_{\mathrm{ih}}{y}\right)-\left(\left({x}{\cdot }_{\mathrm{ih}}{y}\right)+\left({y}{\cdot }_{\mathrm{ih}}{x}\right)\right)$
17 16 3expb ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)-\left(\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)\right)=\left({x}{\cdot }_{\mathrm{ih}}{x}\right)+\left({y}{\cdot }_{\mathrm{ih}}{y}\right)-\left(\left({x}{\cdot }_{\mathrm{ih}}{y}\right)+\left({y}{\cdot }_{\mathrm{ih}}{x}\right)\right)$
18 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right)\in ℋ$
19 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {y}\in ℋ\right)\to {T}\left({y}\right)\in ℋ$
20 18 19 anim12dan ${⊢}\left({T}:ℋ⟶ℋ\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}\left({x}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)$
21 4 20 sylan ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}\left({x}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)$
22 normlem9at ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to \left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)-\left(\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)\right)$
23 21 22 syl ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)-\left(\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{T}\left({y}\right)\right)+\left({T}\left({y}\right){\cdot }_{\mathrm{ih}}{T}\left({x}\right)\right)\right)$
24 normlem9at ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=\left({x}{\cdot }_{\mathrm{ih}}{x}\right)+\left({y}{\cdot }_{\mathrm{ih}}{y}\right)-\left(\left({x}{\cdot }_{\mathrm{ih}}{y}\right)+\left({y}{\cdot }_{\mathrm{ih}}{x}\right)\right)$
25 24 adantl ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=\left({x}{\cdot }_{\mathrm{ih}}{x}\right)+\left({y}{\cdot }_{\mathrm{ih}}{y}\right)-\left(\left({x}{\cdot }_{\mathrm{ih}}{y}\right)+\left({y}{\cdot }_{\mathrm{ih}}{x}\right)\right)$
26 17 23 25 3eqtr4rd ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)$
27 26 eqeq1d ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left(\left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=0↔\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)=0\right)$
28 hvsubcl ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{-}_{ℎ}{y}\in ℋ$
29 his6 ${⊢}{x}{-}_{ℎ}{y}\in ℋ\to \left(\left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=0↔{x}{-}_{ℎ}{y}={0}_{ℎ}\right)$
30 28 29 syl ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left(\left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=0↔{x}{-}_{ℎ}{y}={0}_{ℎ}\right)$
31 hvsubeq0 ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left({x}{-}_{ℎ}{y}={0}_{ℎ}↔{x}={y}\right)$
32 30 31 bitrd ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to \left(\left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=0↔{x}={y}\right)$
33 32 adantl ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left(\left({x}{-}_{ℎ}{y}\right){\cdot }_{\mathrm{ih}}\left({x}{-}_{ℎ}{y}\right)=0↔{x}={y}\right)$
34 hvsubcl ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to {T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\in ℋ$
35 his6 ${⊢}{T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\in ℋ\to \left(\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)=0↔{T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)={0}_{ℎ}\right)$
36 34 35 syl ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to \left(\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)=0↔{T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)={0}_{ℎ}\right)$
37 hvsubeq0 ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to \left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)={0}_{ℎ}↔{T}\left({x}\right)={T}\left({y}\right)\right)$
38 36 37 bitrd ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {T}\left({y}\right)\in ℋ\right)\to \left(\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)=0↔{T}\left({x}\right)={T}\left({y}\right)\right)$
39 21 38 syl ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left(\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right){\cdot }_{\mathrm{ih}}\left({T}\left({x}\right){-}_{ℎ}{T}\left({y}\right)\right)=0↔{T}\left({x}\right)={T}\left({y}\right)\right)$
40 27 33 39 3bitr3rd ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}\left({x}\right)={T}\left({y}\right)↔{x}={y}\right)$
41 40 biimpd ${⊢}\left({T}\in \mathrm{UniOp}\wedge \left({x}\in ℋ\wedge {y}\in ℋ\right)\right)\to \left({T}\left({x}\right)={T}\left({y}\right)\to {x}={y}\right)$
42 41 ralrimivva ${⊢}{T}\in \mathrm{UniOp}\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({T}\left({x}\right)={T}\left({y}\right)\to {x}={y}\right)$
43 dff13 ${⊢}{T}:ℋ\underset{1-1}{⟶}ℋ↔\left({T}:ℋ⟶ℋ\wedge \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\left({T}\left({x}\right)={T}\left({y}\right)\to {x}={y}\right)\right)$
44 4 42 43 sylanbrc ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{1-1}{⟶}ℋ$
45 df-f1o ${⊢}{T}:ℋ\underset{1-1 onto}{⟶}ℋ↔\left({T}:ℋ\underset{1-1}{⟶}ℋ\wedge {T}:ℋ\underset{onto}{⟶}ℋ\right)$
46 44 2 45 sylanbrc ${⊢}{T}\in \mathrm{UniOp}\to {T}:ℋ\underset{1-1 onto}{⟶}ℋ$