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 ⋅ ih T ⁡ y = x ⋅ ih y
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 = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → T ∈ UniOp ↔ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ UniOp
8 eleq1 ⊢ T = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → T ∈ LinOp ↔ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ LinOp
9 foeq1 ⊢ T = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → T : ℋ ⟶ onto ℋ ↔ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ : ℋ ⟶ 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 = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → T ⁡ y = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y
15 14 fveqeq2d ⊢ T = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ y ↔ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
16 15 ralbidv ⊢ T = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → ∀ y ∈ ℋ norm ℎ ⁡ T ⁡ y = norm ℎ ⁡ y ↔ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
17 13 16 bitrid ⊢ T = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x ↔ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
18 8 9 17 3anbi123d ⊢ T = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x ↔ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ LinOp ∧ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ : ℋ ⟶ onto ℋ ∧ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
19 eleq1 ⊢ I ↾ ℋ = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → I ↾ ℋ ∈ LinOp ↔ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ LinOp
20 foeq1 ⊢ I ↾ ℋ = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → I ↾ ℋ : ℋ ⟶ onto ℋ ↔ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ : ℋ ⟶ onto ℋ
21 fveq1 ⊢ I ↾ ℋ = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → I ↾ ℋ ⁡ y = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y
22 21 fveqeq2d ⊢ I ↾ ℋ = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → norm ℎ ⁡ I ↾ ℋ ⁡ y = norm ℎ ⁡ y ↔ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
23 22 ralbidv ⊢ I ↾ ℋ = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → ∀ y ∈ ℋ norm ℎ ⁡ I ↾ ℋ ⁡ y = norm ℎ ⁡ y ↔ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
24 19 20 23 3anbi123d ⊢ I ↾ ℋ = if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ → I ↾ ℋ ∈ LinOp ∧ I ↾ ℋ : ℋ ⟶ onto ℋ ∧ ∀ y ∈ ℋ norm ℎ ⁡ I ↾ ℋ ⁡ y = norm ℎ ⁡ y ↔ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ LinOp ∧ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ : ℋ ⟶ onto ℋ ∧ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ 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 ⊢ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ LinOp ∧ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ : ℋ ⟶ onto ℋ ∧ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
34 33 simp1i ⊢ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ LinOp
35 33 simp2i ⊢ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ : ℋ ⟶ onto ℋ
36 33 simp3i ⊢ ∀ y ∈ ℋ norm ℎ ⁡ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ⁡ y = norm ℎ ⁡ y
37 34 35 36 lnopunii ⊢ if T ∈ LinOp ∧ T : ℋ ⟶ onto ℋ ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x = norm ℎ ⁡ x T I ↾ ℋ ∈ 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