This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 ∈ BndLinOp
Assertion nmopadjlei ( 𝐴 ∈ ℋ → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nmopadjle.1 ⊢ 𝑇 ∈ BndLinOp
2 bdopssadj ⊢ BndLinOp ⊆ dom adjℎ
3 2 1 sselii ⊢ 𝑇 ∈ dom adjℎ
4 adjvalval ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) = ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) = ( 𝑣 ·ih 𝑓 ) ) )
5 3 4 mpan ⊢ ( 𝐴 ∈ ℋ → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) = ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) = ( 𝑣 ·ih 𝑓 ) ) )
6 oveq2 ⊢ ( 𝑧 = 𝐴 → ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) )
7 6 eqeq1d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ↔ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) = ( 𝑣 ·ih 𝑓 ) ) )
8 7 ralbidv ⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ↔ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) = ( 𝑣 ·ih 𝑓 ) ) )
9 8 riotabidv ⊢ ( 𝑧 = 𝐴 → ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) = ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) = ( 𝑣 ·ih 𝑓 ) ) )
10 eqid ⊢ ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) ) = ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) )
11 riotaex ⊢ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) = ( 𝑣 ·ih 𝑓 ) ) ∈ V
12 9 10 11 fvmpt ⊢ ( 𝐴 ∈ ℋ → ( ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) ) ‘ 𝐴 ) = ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝐴 ) = ( 𝑣 ·ih 𝑓 ) ) )
13 5 12 eqtr4d ⊢ ( 𝐴 ∈ ℋ → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) = ( ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) ) ‘ 𝐴 ) )
14 13 fveq2d ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) = ( normℎ ‘ ( ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) ) ‘ 𝐴 ) ) )
15 inss1 ⊢ ( LinOp ∩ ContOp ) ⊆ LinOp
16 lncnbd ⊢ ( LinOp ∩ ContOp ) = BndLinOp
17 1 16 eleqtrri ⊢ 𝑇 ∈ ( LinOp ∩ ContOp )
18 15 17 sselii ⊢ 𝑇 ∈ LinOp
19 inss2 ⊢ ( LinOp ∩ ContOp ) ⊆ ContOp
20 19 17 sselii ⊢ 𝑇 ∈ ContOp
21 eqid ⊢ ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑧 ) ) = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑧 ) )
22 oveq2 ⊢ ( 𝑓 = 𝑤 → ( 𝑣 ·ih 𝑓 ) = ( 𝑣 ·ih 𝑤 ) )
23 22 eqeq2d ⊢ ( 𝑓 = 𝑤 → ( ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ↔ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑤 ) ) )
24 23 ralbidv ⊢ ( 𝑓 = 𝑤 → ( ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ↔ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑤 ) ) )
25 24 cbvriotavw ⊢ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑤 ) )
26 18 20 21 25 10 cnlnadjlem7 ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑧 ) = ( 𝑣 ·ih 𝑓 ) ) ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )
27 14 26 eqbrtrd ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )