Metamath Proof Explorer

Theorem nvsid

Description: Identity element for the scalar product of a normed complex vector space. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nvscl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
		nvscl.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
	Assertion	nvsid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nvscl.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvscl.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
3		eqid	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
4	3	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
5		eqid	⊢ ( +_𝑣 ‘ 𝑈 ) = ( +_𝑣 ‘ 𝑈 )
6	5	vafval	⊢ ( +_𝑣 ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
7	2	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
8	1 5	bafval	⊢ 𝑋 = ran ( +_𝑣 ‘ 𝑈 )
9	6 7 8	vcidOLD	⊢ ( ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )
10	4 9	sylan	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 𝑆 𝐴 ) = 𝐴 )