This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ S = \cdot_{𝑠OLD} (U)$
	Assertion	smfval	$⊢ S = 2^{nd} (1^{st} (U))$

Proof

Step	Hyp	Ref	Expression
1		smfval.4	$⊢ S = \cdot_{𝑠OLD} (U)$
2		df-sm	$⊢ \cdot_{𝑠OLD} = 2^{nd} \circ 1^{st}$
3	2	fveq1i	$⊢ \cdot_{𝑠OLD} (U) = (2^{nd} \circ 1^{st}) (U)$
4		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
5		fof	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} : V ⟶ V$
6	4 5	ax-mp	$⊢ 1^{st} : V ⟶ V$
7		fvco3	$⊢ (1^{st} : V ⟶ V \land U \in V) \to (2^{nd} \circ 1^{st}) (U) = 2^{nd} (1^{st} (U))$
8	6 7	mpan	$⊢ U \in V \to (2^{nd} \circ 1^{st}) (U) = 2^{nd} (1^{st} (U))$
9	3 8	eqtrid	$⊢ U \in V \to \cdot_{𝑠OLD} (U) = 2^{nd} (1^{st} (U))$
10		fvprc	$⊢ \neg U \in V \to \cdot_{𝑠OLD} (U) = \emptyset$
11		fvprc	$⊢ \neg U \in V \to 1^{st} (U) = \emptyset$
12	11	fveq2d	$⊢ \neg U \in V \to 2^{nd} (1^{st} (U)) = 2^{nd} (\emptyset)$
13		2nd0	$⊢ 2^{nd} (\emptyset) = \emptyset$
14	12 13	eqtr2di	$⊢ \neg U \in V \to \emptyset = 2^{nd} (1^{st} (U))$
15	10 14	eqtrd	$⊢ \neg U \in V \to \cdot_{𝑠OLD} (U) = 2^{nd} (1^{st} (U))$
16	9 15	pm2.61i	$⊢ \cdot_{𝑠OLD} (U) = 2^{nd} (1^{st} (U))$
17	1 16	eqtri	$⊢ S = 2^{nd} (1^{st} (U))$