# 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 = if x ∈ ℋ x 0 ℎ → T ⁡ x = T ⁡ if x ∈ ℋ x 0 ℎ$
5 4 oveq1d $⊢ x = if x ∈ ℋ x 0 ℎ → T ⁡ x ⋅ ih T ⁡ y = T ⁡ if x ∈ ℋ x 0 ℎ ⋅ ih T ⁡ y$
6 oveq1 $⊢ x = if x ∈ ℋ x 0 ℎ → x ⋅ ih y = if x ∈ ℋ x 0 ℎ ⋅ ih y$
7 5 6 eqeq12d $⊢ x = if x ∈ ℋ x 0 ℎ → T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y ↔ T ⁡ if x ∈ ℋ x 0 ℎ ⋅ ih T ⁡ y = if x ∈ ℋ x 0 ℎ ⋅ ih y$
8 fveq2 $⊢ y = if y ∈ ℋ y 0 ℎ → T ⁡ y = T ⁡ if y ∈ ℋ y 0 ℎ$
9 8 oveq2d $⊢ y = if y ∈ ℋ y 0 ℎ → T ⁡ if x ∈ ℋ x 0 ℎ ⋅ ih T ⁡ y = T ⁡ if x ∈ ℋ x 0 ℎ ⋅ ih T ⁡ if y ∈ ℋ y 0 ℎ$
10 oveq2 $⊢ y = if y ∈ ℋ y 0 ℎ → if x ∈ ℋ x 0 ℎ ⋅ ih y = if x ∈ ℋ x 0 ℎ ⋅ ih if y ∈ ℋ y 0 ℎ$
11 9 10 eqeq12d $⊢ y = if y ∈ ℋ y 0 ℎ → T ⁡ if x ∈ ℋ x 0 ℎ ⋅ ih T ⁡ y = if x ∈ ℋ x 0 ℎ ⋅ ih y ↔ T ⁡ if x ∈ ℋ x 0 ℎ ⋅ ih T ⁡ if y ∈ ℋ y 0 ℎ = if x ∈ ℋ x 0 ℎ ⋅ ih if y ∈ ℋ y 0 ℎ$
12 ifhvhv0 $⊢ if x ∈ ℋ x 0 ℎ ∈ ℋ$
13 ifhvhv0 $⊢ if y ∈ ℋ y 0 ℎ ∈ ℋ$
14 1 3 12 13 lnopunilem2 $⊢ T ⁡ if x ∈ ℋ x 0 ℎ ⋅ ih T ⁡ if y ∈ ℋ y 0 ℎ = if x ∈ ℋ x 0 ℎ ⋅ ih if y ∈ ℋ y 0 ℎ$
15 7 11 14 dedth2h $⊢ x ∈ ℋ ∧ y ∈ ℋ → T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$
16 15 rgen2 $⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$
17 elunop $⊢ T ∈ UniOp ↔ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih T ⁡ y = x ⋅ ih y$
18 2 16 17 mpbir2an $⊢ T ∈ UniOp$