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 | ⊢ 𝑊 = ( 1^{st} ‘ 𝑈 ) | |
nvop2.6 | ⊢ 𝑁 = ( norm_{CV} ‘ 𝑈 ) | ||
Assertion | nvop2 | ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ 𝑊 , 𝑁 ⟩ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvop2.1 | ⊢ 𝑊 = ( 1^{st} ‘ 𝑈 ) | |
2 | nvop2.6 | ⊢ 𝑁 = ( norm_{CV} ‘ 𝑈 ) | |
3 | nvrel | ⊢ Rel NrmCVec | |
4 | 1st2nd | ⊢ ( ( Rel NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝑈 = ⟨ ( 1^{st} ‘ 𝑈 ) , ( 2^{nd} ‘ 𝑈 ) ⟩ ) | |
5 | 3 4 | mpan | ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ( 1^{st} ‘ 𝑈 ) , ( 2^{nd} ‘ 𝑈 ) ⟩ ) |
6 | 2 | nmcvfval | ⊢ 𝑁 = ( 2^{nd} ‘ 𝑈 ) |
7 | 1 6 | opeq12i | ⊢ ⟨ 𝑊 , 𝑁 ⟩ = ⟨ ( 1^{st} ‘ 𝑈 ) , ( 2^{nd} ‘ 𝑈 ) ⟩ |
8 | 5 7 | eqtr4di | ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ 𝑊 , 𝑁 ⟩ ) |