# 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 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇𝑦 ) ) ) } )