Theorem bloval

Description: The class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bloval.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	bloval.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
	bloval.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
Assertion	bloval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐵 = { 𝑡 ∈ 𝐿 ∣ ( 𝑁 ‘ 𝑡 ) < +∞ } )

Proof

Step	Hyp	Ref	Expression
1		bloval.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
2		bloval.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
3		bloval.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
4		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 LnOp 𝑤 ) = ( 𝑈 LnOp 𝑤 ) )
5		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 normOpOLD 𝑤 ) = ( 𝑈 normOpOLD 𝑤 ) )
6	5	fveq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) = ( ( 𝑈 normOpOLD 𝑤 ) ‘ 𝑡 ) )
7	6	breq1d	⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ ↔ ( ( 𝑈 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ ) )
8	4 7	rabeqbidv	⊢ ( 𝑢 = 𝑈 → { 𝑡 ∈ ( 𝑢 LnOp 𝑤 ) ∣ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ } = { 𝑡 ∈ ( 𝑈 LnOp 𝑤 ) ∣ ( ( 𝑈 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ } )
9		oveq2	⊢ ( 𝑤 = 𝑊 → ( 𝑈 LnOp 𝑤 ) = ( 𝑈 LnOp 𝑊 ) )
10	9 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( 𝑈 LnOp 𝑤 ) = 𝐿 )
11		oveq2	⊢ ( 𝑤 = 𝑊 → ( 𝑈 normOpOLD 𝑤 ) = ( 𝑈 normOpOLD 𝑊 ) )
12	11 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( 𝑈 normOpOLD 𝑤 ) = 𝑁 )
13	12	fveq1d	⊢ ( 𝑤 = 𝑊 → ( ( 𝑈 normOpOLD 𝑤 ) ‘ 𝑡 ) = ( 𝑁 ‘ 𝑡 ) )
14	13	breq1d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑈 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ ↔ ( 𝑁 ‘ 𝑡 ) < +∞ ) )
15	10 14	rabeqbidv	⊢ ( 𝑤 = 𝑊 → { 𝑡 ∈ ( 𝑈 LnOp 𝑤 ) ∣ ( ( 𝑈 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ } = { 𝑡 ∈ 𝐿 ∣ ( 𝑁 ‘ 𝑡 ) < +∞ } )
16		df-blo	⊢ BLnOp = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { 𝑡 ∈ ( 𝑢 LnOp 𝑤 ) ∣ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ } )
17	2	ovexi	⊢ 𝐿 ∈ V
18	17	rabex	⊢ { 𝑡 ∈ 𝐿 ∣ ( 𝑁 ‘ 𝑡 ) < +∞ } ∈ V
19	8 15 16 18	ovmpo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 BLnOp 𝑊 ) = { 𝑡 ∈ 𝐿 ∣ ( 𝑁 ‘ 𝑡 ) < +∞ } )
20	3 19	syl5eq	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐵 = { 𝑡 ∈ 𝐿 ∣ ( 𝑁 ‘ 𝑡 ) < +∞ } )