Metamath Proof Explorer

Theorem nmopadjlei

Description: Property of the norm of an adjoint. Part of proof of Theorem 3.10 of Beran p. 104. (Contributed by NM, 22-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypothesis nmopadjle.1 ⊢ T ∈ BndLinOp
Assertion nmopadjlei ⊢ A ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 nmopadjle.1 ⊢ T ∈ BndLinOp
2 bdopssadj ⊢ BndLinOp ⊆ dom ⁡ adj h
3 2 1 sselii ⊢ T ∈ dom ⁡ adj h
4 adjvalval ⊢ T ∈ dom ⁡ adj h ∧ A ∈ ℋ → adj h ⁡ T ⁡ A = ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih A = v ⋅ ih f
5 3 4 mpan ⊢ A ∈ ℋ → adj h ⁡ T ⁡ A = ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih A = v ⋅ ih f
6 oveq2 ⊢ z = A → T ⁡ v ⋅ ih z = T ⁡ v ⋅ ih A
7 6 eqeq1d ⊢ z = A → T ⁡ v ⋅ ih z = v ⋅ ih f ↔ T ⁡ v ⋅ ih A = v ⋅ ih f
8 7 ralbidv ⊢ z = A → ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f ↔ ∀ v ∈ ℋ T ⁡ v ⋅ ih A = v ⋅ ih f
9 8 riotabidv ⊢ z = A → ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f = ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih A = v ⋅ ih f
10 eqid ⊢ z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f = z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f
11 riotaex ⊢ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih A = v ⋅ ih f ∈ V
12 9 10 11 fvmpt ⊢ A ∈ ℋ → z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f ⁡ A = ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih A = v ⋅ ih f
13 5 12 eqtr4d ⊢ A ∈ ℋ → adj h ⁡ T ⁡ A = z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f ⁡ A
14 13 fveq2d ⊢ A ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ A = norm ℎ ⁡ z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f ⁡ A
15 inss1 ⊢ LinOp ∩ ContOp ⊆ LinOp
16 lncnbd ⊢ LinOp ∩ ContOp = BndLinOp
17 1 16 eleqtrri ⊢ T ∈ LinOp ∩ ContOp
18 15 17 sselii ⊢ T ∈ LinOp
19 inss2 ⊢ LinOp ∩ ContOp ⊆ ContOp
20 19 17 sselii ⊢ T ∈ ContOp
21 eqid ⊢ g ∈ ℋ ⟼ T ⁡ g ⋅ ih z = g ∈ ℋ ⟼ T ⁡ g ⋅ ih z
22 oveq2 ⊢ f = w → v ⋅ ih f = v ⋅ ih w
23 22 eqeq2d ⊢ f = w → T ⁡ v ⋅ ih z = v ⋅ ih f ↔ T ⁡ v ⋅ ih z = v ⋅ ih w
24 23 ralbidv ⊢ f = w → ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f ↔ ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih w
25 24 cbvriotavw ⊢ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f = ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih w
26 18 20 21 25 10 cnlnadjlem7 ⊢ A ∈ ℋ → norm ℎ ⁡ z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A
27 14 26 eqbrtrd ⊢ A ∈ ℋ → norm ℎ ⁡ adj h ⁡ T ⁡ A ≤ norm op ⁡ T ⁢ norm ℎ ⁡ A