Metamath Proof Explorer

Theorem smfval

Description: Value of the function for the scalar multiplication operation on a normed complex vector space. (Contributed by NM, 24-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	smfval.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
	Assertion	smfval	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		smfval.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
2		df-sm	⊢ ·_𝑠OLD = ( 2^nd ∘ 1^st )
3	2	fveq1i	⊢ ( ·_𝑠OLD ‘ 𝑈 ) = ( ( 2^nd ∘ 1^st ) ‘ 𝑈 )
4		fo1st	⊢ 1^st : V –onto→ V
5		fof	⊢ ( 1^st : V –onto→ V → 1^st : V ⟶ V )
6	4 5	ax-mp	⊢ 1^st : V ⟶ V
7		fvco3	⊢ ( ( 1^st : V ⟶ V ∧ 𝑈 ∈ V ) → ( ( 2^nd ∘ 1^st ) ‘ 𝑈 ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
8	6 7	mpan	⊢ ( 𝑈 ∈ V → ( ( 2^nd ∘ 1^st ) ‘ 𝑈 ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
9	3 8	syl5eq	⊢ ( 𝑈 ∈ V → ( ·_𝑠OLD ‘ 𝑈 ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
10		fvprc	⊢ ( ¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘ 𝑈 ) = ∅ )
11		fvprc	⊢ ( ¬ 𝑈 ∈ V → ( 1^st ‘ 𝑈 ) = ∅ )
12	11	fveq2d	⊢ ( ¬ 𝑈 ∈ V → ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) = ( 2^nd ‘ ∅ ) )
13		2nd0	⊢ ( 2^nd ‘ ∅ ) = ∅
14	12 13	eqtr2di	⊢ ( ¬ 𝑈 ∈ V → ∅ = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
15	10 14	eqtrd	⊢ ( ¬ 𝑈 ∈ V → ( ·_𝑠OLD ‘ 𝑈 ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
16	9 15	pm2.61i	⊢ ( ·_𝑠OLD ‘ 𝑈 ) = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )
17	1 16	eqtri	⊢ 𝑆 = ( 2^nd ‘ ( 1^st ‘ 𝑈 ) )