Description: A normed complex vector space is an ordered pair of a vector space and a norm operation. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nvop2.1 | ⊢ 𝑊 = ( 1st ‘ 𝑈 ) | |
| nvop2.6 | ⊢ 𝑁 = ( normCV ‘ 𝑈 ) | ||
| Assertion | nvop2 | ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ 𝑊 , 𝑁 ⟩ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nvop2.1 | ⊢ 𝑊 = ( 1st ‘ 𝑈 ) | |
| 2 | nvop2.6 | ⊢ 𝑁 = ( normCV ‘ 𝑈 ) | |
| 3 | nvrel | ⊢ Rel NrmCVec | |
| 4 | 1st2nd | ⊢ ( ( Rel NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ ) | |
| 5 | 3 4 | mpan | ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ ) |
| 6 | 2 | nmcvfval | ⊢ 𝑁 = ( 2nd ‘ 𝑈 ) |
| 7 | 1 6 | opeq12i | ⊢ ⟨ 𝑊 , 𝑁 ⟩ = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ |
| 8 | 5 7 | eqtr4di | ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ 𝑊 , 𝑁 ⟩ ) |