# 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 ( 𝑇 ∈ UniOp ↔ ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) )

### Proof

Step Hyp Ref Expression
1 unoplin ( 𝑇 ∈ UniOp → 𝑇 ∈ LinOp )
2 elunop ( 𝑇 ∈ UniOp ↔ ( 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih ( 𝑇𝑦 ) ) = ( 𝑥 ·ih 𝑦 ) ) )
3 2 simplbi ( 𝑇 ∈ UniOp → 𝑇 : ℋ –onto→ ℋ )
4 unopnorm ( ( 𝑇 ∈ UniOp ∧ 𝑥 ∈ ℋ ) → ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) )
5 4 ralrimiva ( 𝑇 ∈ UniOp → ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) )
6 1 3 5 3jca ( 𝑇 ∈ UniOp → ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) )
7 eleq1 ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 ∈ UniOp ↔ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ UniOp ) )
8 eleq1 ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 ∈ LinOp ↔ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ) )
9 foeq1 ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 : ℋ –onto→ ℋ ↔ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) : ℋ –onto→ ℋ ) )
10 2fveq3 ( 𝑥 = 𝑦 → ( norm ‘ ( 𝑇𝑥 ) ) = ( norm ‘ ( 𝑇𝑦 ) ) )
11 fveq2 ( 𝑥 = 𝑦 → ( norm𝑥 ) = ( norm𝑦 ) )
12 10 11 eqeq12d ( 𝑥 = 𝑦 → ( ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ↔ ( norm ‘ ( 𝑇𝑦 ) ) = ( norm𝑦 ) ) )
13 12 cbvralvw ( ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ↔ ∀ 𝑦 ∈ ℋ ( norm ‘ ( 𝑇𝑦 ) ) = ( norm𝑦 ) )
14 fveq1 ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇𝑦 ) = ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) )
15 14 fveqeq2d ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( norm ‘ ( 𝑇𝑦 ) ) = ( norm𝑦 ) ↔ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) )
16 15 ralbidv ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ∀ 𝑦 ∈ ℋ ( norm ‘ ( 𝑇𝑦 ) ) = ( norm𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) )
17 13 16 syl5bb ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ↔ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) )
18 8 9 17 3anbi123d ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) ↔ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) : ℋ –onto→ ℋ ∧ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) ) )
19 eleq1 ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( I ↾ ℋ ) ∈ LinOp ↔ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ) )
20 foeq1 ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( I ↾ ℋ ) : ℋ –onto→ ℋ ↔ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) : ℋ –onto→ ℋ ) )
21 fveq1 ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( I ↾ ℋ ) ‘ 𝑦 ) = ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) )
22 21 fveqeq2d ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( norm ‘ ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( norm𝑦 ) ↔ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) )
23 22 ralbidv ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ∀ 𝑦 ∈ ℋ ( norm ‘ ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( norm𝑦 ) ↔ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) )
24 19 20 23 3anbi123d ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( ( I ↾ ℋ ) ∈ LinOp ∧ ( I ↾ ℋ ) : ℋ –onto→ ℋ ∧ ∀ 𝑦 ∈ ℋ ( norm ‘ ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) ↔ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) : ℋ –onto→ ℋ ∧ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) ) ) )
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 ( 𝑦 ∈ ℋ → ( ( I ↾ ℋ ) ‘ 𝑦 ) = 𝑦 )
30 29 fveq2d ( 𝑦 ∈ ℋ → ( norm ‘ ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( norm𝑦 ) )
31 30 rgen 𝑦 ∈ ℋ ( norm ‘ ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( norm𝑦 )
32 25 28 31 3pm3.2i ( ( I ↾ ℋ ) ∈ LinOp ∧ ( I ↾ ℋ ) : ℋ –onto→ ℋ ∧ ∀ 𝑦 ∈ ℋ ( norm ‘ ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( norm𝑦 ) )
33 18 24 32 elimhyp ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) : ℋ –onto→ ℋ ∧ ∀ 𝑦 ∈ ℋ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 ) )
34 33 simp1i if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp
35 33 simp2i if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) : ℋ –onto→ ℋ
36 33 simp3i 𝑦 ∈ ℋ ( norm ‘ ( if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) = ( norm𝑦 )
37 34 35 36 lnopunii if ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) , 𝑇 , ( I ↾ ℋ ) ) ∈ UniOp
38 7 37 dedth ( ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) → 𝑇 ∈ UniOp )
39 6 38 impbii ( 𝑇 ∈ UniOp ↔ ( 𝑇 ∈ LinOp ∧ 𝑇 : ℋ –onto→ ℋ ∧ ∀ 𝑥 ∈ ℋ ( norm ‘ ( 𝑇𝑥 ) ) = ( norm𝑥 ) ) )