Theorem nvop

Description: A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvop.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	nvop.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	nvop.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion	nvop	⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		nvop.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
2		nvop.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3		nvop.6	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		nvrel	⊢ Rel NrmCVec
5		1st2nd	⊢ ( ( Rel NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ )
6	4 5	mpan	⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ )
7	3	nmcvfval	⊢ 𝑁 = ( 2nd ‘ 𝑈 )
8	7	opeq2i	⊢ ⟨ ( 1st ‘ 𝑈 ) , 𝑁 ⟩ = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩
9		eqid	⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 𝑈 )
10	9 1 2	nvvop	⊢ ( 𝑈 ∈ NrmCVec → ( 1st ‘ 𝑈 ) = ⟨ 𝐺 , 𝑆 ⟩ )
11	10	opeq1d	⊢ ( 𝑈 ∈ NrmCVec → ⟨ ( 1st ‘ 𝑈 ) , 𝑁 ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
12	8 11	eqtr3id	⊢ ( 𝑈 ∈ NrmCVec → ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
13	6 12	eqtrd	⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )