nvvop

Description: The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvvop.1	⊢ 𝑊 = ( 1^st ‘ 𝑈 )
	nvvop.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
	nvvop.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
Assertion	nvvop	⊢ ( 𝑈 ∈ NrmCVec → 𝑊 = ⟨ 𝐺 , 𝑆 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		nvvop.1	⊢ 𝑊 = ( 1^st ‘ 𝑈 )
2		nvvop.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
3		nvvop.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
4		vcrel	⊢ Rel CVec_OLD
5		nvss	⊢ NrmCVec ⊆ ( CVec_OLD × V )
6		eqid	⊢ ( norm_CV ‘ 𝑈 ) = ( norm_CV ‘ 𝑈 )
7	1 6	nvop2	⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ 𝑊 , ( norm_CV ‘ 𝑈 ) ⟩ )
8	7	eleq1d	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑈 ∈ NrmCVec ↔ ⟨ 𝑊 , ( norm_CV ‘ 𝑈 ) ⟩ ∈ NrmCVec ) )
9	8	ibi	⊢ ( 𝑈 ∈ NrmCVec → ⟨ 𝑊 , ( norm_CV ‘ 𝑈 ) ⟩ ∈ NrmCVec )
10	5 9	sselid	⊢ ( 𝑈 ∈ NrmCVec → ⟨ 𝑊 , ( norm_CV ‘ 𝑈 ) ⟩ ∈ ( CVec_OLD × V ) )
11		opelxp1	⊢ ( ⟨ 𝑊 , ( norm_CV ‘ 𝑈 ) ⟩ ∈ ( CVec_OLD × V ) → 𝑊 ∈ CVec_OLD )
12	10 11	syl	⊢ ( 𝑈 ∈ NrmCVec → 𝑊 ∈ CVec_OLD )
13		1st2nd	⊢ ( ( Rel CVec_OLD ∧ 𝑊 ∈ CVec_OLD ) → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
14	4 12 13	sylancr	⊢ ( 𝑈 ∈ NrmCVec → 𝑊 = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩ )
15	2	vafval	⊢ 𝐺 = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
16	1	fveq2i	⊢ ( 1^st ‘ 𝑊 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
17	15 16	eqtr4i	⊢ 𝐺 = ( 1^st ‘ 𝑊 )
18	3	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
19	1	fveq2i	⊢ ( 2^nd ‘ 𝑊 ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
20	18 19	eqtr4i	⊢ 𝑆 = ( 2^nd ‘ 𝑊 )
21	17 20	opeq12i	⊢ ⟨ 𝐺 , 𝑆 ⟩ = ⟨ ( 1^st ‘ 𝑊 ) , ( 2^nd ‘ 𝑊 ) ⟩
22	14 21	eqtr4di	⊢ ( 𝑈 ∈ NrmCVec → 𝑊 = ⟨ 𝐺 , 𝑆 ⟩ )

Metamath Proof Explorer

Theorem nvvop

Proof