Theorem adjbdln

Description: The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adjbdln	⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ BndLinOp )

Proof

Step	Hyp	Ref	Expression
1		bdopadj	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ dom adjℎ )
2		adjval	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) = ( ℩ 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
3	1 2	syl	⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) = ( ℩ 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
4		cnlnadj	⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) → ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) )
5		lncnopbd	⊢ ( 𝑇 ∈ ( LinOp ∩ ContOp ) ↔ 𝑇 ∈ BndLinOp )
6		lncnbd	⊢ ( LinOp ∩ ContOp ) = BndLinOp
7	6	rexeqi	⊢ ( ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) )
8	4 5 7	3imtr3i	⊢ ( 𝑇 ∈ BndLinOp → ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) )
9		bdopf	⊢ ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
10		bdopf	⊢ ( 𝑡 ∈ BndLinOp → 𝑡 : ℋ ⟶ ℋ )
11		adjsym	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) )
12	9 10 11	syl2an	⊢ ( ( 𝑇 ∈ BndLinOp ∧ 𝑡 ∈ BndLinOp ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) )
13		eqcom	⊢ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
14	13	2ralbii	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) )
15	12 14	syl6bbr	⊢ ( ( 𝑇 ∈ BndLinOp ∧ 𝑡 ∈ BndLinOp ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
16	15	rexbidva	⊢ ( 𝑇 ∈ BndLinOp → ( ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑦 ) ) ) )
17	8 16	mpbird	⊢ ( 𝑇 ∈ BndLinOp → ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
18		adjeu	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 ∈ dom adjℎ ↔ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
19	9 18	syl	⊢ ( 𝑇 ∈ BndLinOp → ( 𝑇 ∈ dom adjℎ ↔ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
20	1 19	mpbid	⊢ ( 𝑇 ∈ BndLinOp → ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
21		ax-hilex	⊢ ℋ ∈ V
22	21 21	elmap	⊢ ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↔ 𝑡 : ℋ ⟶ ℋ )
23	10 22	sylibr	⊢ ( 𝑡 ∈ BndLinOp → 𝑡 ∈ ( ℋ ↑m ℋ ) )
24	23	ssriv	⊢ BndLinOp ⊆ ( ℋ ↑m ℋ )
25		id	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
26	25	rgenw	⊢ ∀ 𝑡 ∈ BndLinOp ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
27		riotass2	⊢ ( ( ( BndLinOp ⊆ ( ℋ ↑m ℋ ) ∧ ∀ 𝑡 ∈ BndLinOp ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) ∧ ( ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ) → ( ℩ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) = ( ℩ 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
28	24 26 27	mpanl12	⊢ ( ( ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) → ( ℩ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) = ( ℩ 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
29	17 20 28	syl2anc	⊢ ( 𝑇 ∈ BndLinOp → ( ℩ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) = ( ℩ 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
30	3 29	eqtr4d	⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) = ( ℩ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) )
31	24	a1i	⊢ ( 𝑇 ∈ BndLinOp → BndLinOp ⊆ ( ℋ ↑m ℋ ) )
32		reuss	⊢ ( ( BndLinOp ⊆ ( ℋ ↑m ℋ ) ∧ ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ∧ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) → ∃! 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
33	31 17 20 32	syl3anc	⊢ ( 𝑇 ∈ BndLinOp → ∃! 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) )
34		riotacl	⊢ ( ∃! 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) → ( ℩ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ∈ BndLinOp )
35	33 34	syl	⊢ ( 𝑇 ∈ BndLinOp → ( ℩ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑡 ‘ 𝑥 ) ·ih 𝑦 ) ) ∈ BndLinOp )
36	30 35	eqeltrd	⊢ ( 𝑇 ∈ BndLinOp → ( adjℎ ‘ 𝑇 ) ∈ BndLinOp )