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∈UniOp↔T∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x

Proof

Step Hyp Ref Expression
1 unoplin ⊢T∈UniOp→T∈LinOp
2 elunop ⊢T∈UniOp↔T:ℋ⟶ontoℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihT⁡y=x⋅ihy
3 2 simplbi ⊢T∈UniOp→T:ℋ⟶ontoℋ
4 unopnorm ⊢T∈UniOp∧x∈ℋ→normℎ⁡T⁡x=normℎ⁡x
5 4 ralrimiva ⊢T∈UniOp→∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x
6 1 3 5 3jca ⊢T∈UniOp→T∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x
7 eleq1 ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→T∈UniOp↔ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈UniOp
8 eleq1 ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→T∈LinOp↔ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈LinOp
9 foeq1 ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→T:ℋ⟶ontoℋ↔ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ:ℋ⟶ontoℋ
10 2fveq3 ⊢x=y→normℎ⁡T⁡x=normℎ⁡T⁡y
11 fveq2 ⊢x=y→normℎ⁡x=normℎ⁡y
12 10 11 eqeq12d ⊢x=y→normℎ⁡T⁡x=normℎ⁡x↔normℎ⁡T⁡y=normℎ⁡y
13 12 cbvralvw ⊢∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x↔∀y∈ℋnormℎ⁡T⁡y=normℎ⁡y
14 fveq1 ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→T⁡y=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y
15 14 fveqeq2d ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→normℎ⁡T⁡y=normℎ⁡y↔normℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
16 15 ralbidv ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→∀y∈ℋnormℎ⁡T⁡y=normℎ⁡y↔∀y∈ℋnormℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
17 13 16 bitrid ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x↔∀y∈ℋnormℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
18 8 9 17 3anbi123d ⊢T=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→T∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x↔ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈LinOp∧ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ:ℋ⟶ontoℋ∧∀y∈ℋnormℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
19 eleq1 ⊢I↾ℋ=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→I↾ℋ∈LinOp↔ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈LinOp
20 foeq1 ⊢I↾ℋ=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→I↾ℋ:ℋ⟶ontoℋ↔ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ:ℋ⟶ontoℋ
21 fveq1 ⊢I↾ℋ=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→I↾ℋ⁡y=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y
22 21 fveqeq2d ⊢I↾ℋ=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→normℎ⁡I↾ℋ⁡y=normℎ⁡y↔normℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
23 22 ralbidv ⊢I↾ℋ=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→∀y∈ℋnormℎ⁡I↾ℋ⁡y=normℎ⁡y↔∀y∈ℋnormℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
24 19 20 23 3anbi123d ⊢I↾ℋ=ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ→I↾ℋ∈LinOp∧I↾ℋ:ℋ⟶ontoℋ∧∀y∈ℋnormℎ⁡I↾ℋ⁡y=normℎ⁡y↔ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈LinOp∧ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ:ℋ⟶ontoℋ∧∀y∈ℋnormℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
25 idlnop ⊢I↾ℋ∈LinOp
26 f1oi ⊢I↾ℋ:ℋ⟶1-1 ontoℋ
27 f1ofo ⊢I↾ℋ:ℋ⟶1-1 ontoℋ→I↾ℋ:ℋ⟶ontoℋ
28 26 27 ax-mp ⊢I↾ℋ:ℋ⟶ontoℋ
29 fvresi ⊢y∈ℋ→I↾ℋ⁡y=y
30 29 fveq2d ⊢y∈ℋ→normℎ⁡I↾ℋ⁡y=normℎ⁡y
31 30 rgen ⊢∀y∈ℋnormℎ⁡I↾ℋ⁡y=normℎ⁡y
32 25 28 31 3pm3.2i ⊢I↾ℋ∈LinOp∧I↾ℋ:ℋ⟶ontoℋ∧∀y∈ℋnormℎ⁡I↾ℋ⁡y=normℎ⁡y
33 18 24 32 elimhyp ⊢ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈LinOp∧ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ:ℋ⟶ontoℋ∧∀y∈ℋnormℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
34 33 simp1i ⊢ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈LinOp
35 33 simp2i ⊢ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ:ℋ⟶ontoℋ
36 33 simp3i ⊢∀y∈ℋnormℎ⁡ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ⁡y=normℎ⁡y
37 34 35 36 lnopunii ⊢ifT∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡xTI↾ℋ∈UniOp
38 7 37 dedth ⊢T∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x→T∈UniOp
39 6 38 impbii ⊢T∈UniOp↔T∈LinOp∧T:ℋ⟶ontoℋ∧∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x