Metamath Proof Explorer

Theorem nmosetn0

Description: The set in the supremum of the operator norm definition df-nmoo is nonempty. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmosetn0.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nmosetn0.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
nmosetn0.4 ⊢ 𝑀 = ( normCV ‘ 𝑈 )
Assertion nmosetn0 ( 𝑈 ∈ NrmCVec → ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } )

Proof

Step Hyp Ref Expression
1 nmosetn0.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nmosetn0.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3 nmosetn0.4 ⊢ 𝑀 = ( normCV ‘ 𝑈 )
4 1 2 nvzcl ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 )
5 2 3 nvz0 ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑀 ‘ 𝑍 ) = 0 )
6 0le1 ⊢ 0 ≤ 1
7 5 6 eqbrtrdi ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑀 ‘ 𝑍 ) ≤ 1 )
8 eqid ⊢ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) )
9 7 8 jctir ⊢ ( 𝑈 ∈ NrmCVec → ( ( 𝑀 ‘ 𝑍 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ) )
10 fveq2 ⊢ ( 𝑦 = 𝑍 → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑍 ) )
11 10 breq1d ⊢ ( 𝑦 = 𝑍 → ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ↔ ( 𝑀 ‘ 𝑍 ) ≤ 1 ) )
12 2fveq3 ⊢ ( 𝑦 = 𝑍 → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) )
13 12 eqeq2d ⊢ ( 𝑦 = 𝑍 → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ) )
14 11 13 anbi12d ⊢ ( 𝑦 = 𝑍 → ( ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ( ( 𝑀 ‘ 𝑍 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ) ) )
15 14 rspcev ⊢ ( ( 𝑍 ∈ 𝑋 ∧ ( ( 𝑀 ‘ 𝑍 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ) ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
16 4 9 15 syl2anc ⊢ ( 𝑈 ∈ NrmCVec → ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
17 fvex ⊢ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ∈ V
18 eqeq1 ⊢ ( 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) → ( 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
19 18 anbi2d ⊢ ( 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) → ( ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
20 19 rexbidv ⊢ ( 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) → ( ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) )
21 17 20 elab ⊢ ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) )
22 16 21 sylibr ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑁 ‘ ( 𝑇 ‘ 𝑍 ) ) ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 ( ( 𝑀 ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ) } )