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ℎ ‘ 𝐴 ) ) )