Theorem nmoofval

Description: The operator norm function. (Contributed by NM, 6-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoofval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nmoofval.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	nmoofval.3	⊢ 𝐿 = ( normCV ‘ 𝑈 )
	nmoofval.4	⊢ 𝑀 = ( normCV ‘ 𝑊 )
	nmoofval.6	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
Assertion	nmoofval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑁 = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmoofval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nmoofval.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		nmoofval.3	⊢ 𝐿 = ( normCV ‘ 𝑈 )
4		nmoofval.4	⊢ 𝑀 = ( normCV ‘ 𝑊 )
5		nmoofval.6	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
6		fveq2	⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
7	6 1	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
8	7	oveq2d	⊢ ( 𝑢 = 𝑈 → ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) = ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) )
9		fveq2	⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = ( normCV ‘ 𝑈 ) )
10	9 3	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = 𝐿 )
11	10	fveq1d	⊢ ( 𝑢 = 𝑈 → ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) = ( 𝐿 ‘ 𝑧 ) )
12	11	breq1d	⊢ ( 𝑢 = 𝑈 → ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ↔ ( 𝐿 ‘ 𝑧 ) ≤ 1 ) )
13	12	anbi1d	⊢ ( 𝑢 = 𝑈 → ( ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
14	7 13	rexeqbidv	⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
15	14	abbidv	⊢ ( 𝑢 = 𝑈 → { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } = { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } )
16	15	supeq1d	⊢ ( 𝑢 = 𝑈 → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
17	8 16	mpteq12dv	⊢ ( 𝑢 = 𝑈 → ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) = ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
18		fveq2	⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = ( BaseSet ‘ 𝑊 ) )
19	18 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = 𝑌 )
20	19	oveq1d	⊢ ( 𝑤 = 𝑊 → ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) = ( 𝑌 ↑m 𝑋 ) )
21		fveq2	⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = ( normCV ‘ 𝑊 ) )
22	21 4	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = 𝑀 )
23	22	fveq1d	⊢ ( 𝑤 = 𝑊 → ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) )
24	23	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) )
25	24	anbi2d	⊢ ( 𝑤 = 𝑊 → ( ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
26	25	rexbidv	⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) ↔ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) ) )
27	26	abbidv	⊢ ( 𝑤 = 𝑊 → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } = { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } )
28	27	supeq1d	⊢ ( 𝑤 = 𝑊 → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) )
29	20 28	mpteq12dv	⊢ ( 𝑤 = 𝑊 → ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
30		df-nmoo	⊢ normOpOLD = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ ( 𝑡 ∈ ( ( BaseSet ‘ 𝑤 ) ↑m ( BaseSet ‘ 𝑢 ) ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ ( BaseSet ‘ 𝑢 ) ( ( ( normCV ‘ 𝑢 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( normCV ‘ 𝑤 ) ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
31		ovex	⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
32	31	mptex	⊢ ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) ∈ V
33	17 29 30 32	ovmpo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 normOpOLD 𝑊 ) = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )
34	5 33	syl5eq	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑁 = ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↦ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝐿 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑀 ‘ ( 𝑡 ‘ 𝑧 ) ) ) } , ℝ* , < ) ) )