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