Metamath Proof Explorer

Theorem lnopunii

Description: If a linear operator (whose range is ~H ) is idempotent in the norm, the operator is unitary. Similar to theorem in AkhiezerGlazman p. 73. (Contributed by NM, 23-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnopuni.1 ⊢T∈LinOp
lnopuni.2 ⊢T:ℋ⟶ontoℋ
lnopuni.3 ⊢∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x
Assertion lnopunii ⊢T∈UniOp

Proof

Step Hyp Ref Expression
1 lnopuni.1 ⊢T∈LinOp
2 lnopuni.2 ⊢T:ℋ⟶ontoℋ
3 lnopuni.3 ⊢∀x∈ℋnormℎ⁡T⁡x=normℎ⁡x
4 fveq2 ⊢x=ifx∈ℋx0ℎ→T⁡x=T⁡ifx∈ℋx0ℎ
5 4 oveq1d ⊢x=ifx∈ℋx0ℎ→T⁡x⋅ihT⁡y=T⁡ifx∈ℋx0ℎ⋅ihT⁡y
6 oveq1 ⊢x=ifx∈ℋx0ℎ→x⋅ihy=ifx∈ℋx0ℎ⋅ihy
7 5 6 eqeq12d ⊢x=ifx∈ℋx0ℎ→T⁡x⋅ihT⁡y=x⋅ihy↔T⁡ifx∈ℋx0ℎ⋅ihT⁡y=ifx∈ℋx0ℎ⋅ihy
8 fveq2 ⊢y=ify∈ℋy0ℎ→T⁡y=T⁡ify∈ℋy0ℎ
9 8 oveq2d ⊢y=ify∈ℋy0ℎ→T⁡ifx∈ℋx0ℎ⋅ihT⁡y=T⁡ifx∈ℋx0ℎ⋅ihT⁡ify∈ℋy0ℎ
10 oveq2 ⊢y=ify∈ℋy0ℎ→ifx∈ℋx0ℎ⋅ihy=ifx∈ℋx0ℎ⋅ihify∈ℋy0ℎ
11 9 10 eqeq12d ⊢y=ify∈ℋy0ℎ→T⁡ifx∈ℋx0ℎ⋅ihT⁡y=ifx∈ℋx0ℎ⋅ihy↔T⁡ifx∈ℋx0ℎ⋅ihT⁡ify∈ℋy0ℎ=ifx∈ℋx0ℎ⋅ihify∈ℋy0ℎ
12 ifhvhv0 ⊢ifx∈ℋx0ℎ∈ℋ
13 ifhvhv0 ⊢ify∈ℋy0ℎ∈ℋ
14 1 3 12 13 lnopunilem2 ⊢T⁡ifx∈ℋx0ℎ⋅ihT⁡ify∈ℋy0ℎ=ifx∈ℋx0ℎ⋅ihify∈ℋy0ℎ
15 7 11 14 dedth2h ⊢x∈ℋ∧y∈ℋ→T⁡x⋅ihT⁡y=x⋅ihy
16 15 rgen2 ⊢∀x∈ℋ∀y∈ℋT⁡x⋅ihT⁡y=x⋅ihy
17 elunop ⊢T∈UniOp↔T:ℋ⟶ontoℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihT⁡y=x⋅ihy
18 2 16 17 mpbir2an ⊢T∈UniOp