phop

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

	Ref	Expression
Hypotheses	phop.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
	phop.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
	phop.6	⊢ 𝑁 = ( norm_CV ‘ 𝑈 )
Assertion	phop	⊢ ( 𝑈 ∈ CPreHil_OLD → 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		phop.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
2		phop.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
3		phop.6	⊢ 𝑁 = ( norm_CV ‘ 𝑈 )
4		phrel	⊢ Rel CPreHil_OLD
5		1st2nd	⊢ ( ( Rel CPreHil_OLD ∧ 𝑈 ∈ CPreHil_OLD ) → 𝑈 = ⟨ ( 1^st ‘ 𝑈 ) , ( 2^nd ‘ 𝑈 ) ⟩ )
6	4 5	mpan	⊢ ( 𝑈 ∈ CPreHil_OLD → 𝑈 = ⟨ ( 1^st ‘ 𝑈 ) , ( 2^nd ‘ 𝑈 ) ⟩ )
7	3	nmcvfval	⊢ 𝑁 = ( 2^nd ‘ 𝑈 )
8	7	opeq2i	⊢ ⟨ ( 1^st ‘ 𝑈 ) , 𝑁 ⟩ = ⟨ ( 1^st ‘ 𝑈 ) , ( 2^nd ‘ 𝑈 ) ⟩
9		phnv	⊢ ( 𝑈 ∈ CPreHil_OLD → 𝑈 ∈ NrmCVec )
10		eqid	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
11	10	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
12		vcrel	⊢ Rel CVec_OLD
13		1st2nd	⊢ ( ( Rel CVec_OLD ∧ ( 1^st ‘ 𝑈 ) ∈ CVec_OLD ) → ( 1^st ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ )
14	12 13	mpan	⊢ ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD → ( 1^st ‘ 𝑈 ) = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ )
15	1	vafval	⊢ 𝐺 = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
16	2	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
17	15 16	opeq12i	⊢ ⟨ 𝐺 , 𝑆 ⟩ = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩
18	14 17	eqtr4di	⊢ ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD → ( 1^st ‘ 𝑈 ) = ⟨ 𝐺 , 𝑆 ⟩ )
19	9 11 18	3syl	⊢ ( 𝑈 ∈ CPreHil_OLD → ( 1^st ‘ 𝑈 ) = ⟨ 𝐺 , 𝑆 ⟩ )
20	19	opeq1d	⊢ ( 𝑈 ∈ CPreHil_OLD → ⟨ ( 1^st ‘ 𝑈 ) , 𝑁 ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
21	8 20	eqtr3id	⊢ ( 𝑈 ∈ CPreHil_OLD → ⟨ ( 1^st ‘ 𝑈 ) , ( 2^nd ‘ 𝑈 ) ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
22	6 21	eqtrd	⊢ ( 𝑈 ∈ CPreHil_OLD → 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )

Metamath Proof Explorer

Theorem phop

Proof