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 bitrid ⊢ ( 𝑇 = 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ℎ ‘ 𝑥 ) ) )