Theorem sinhval-named

Description: Value of the named sinh function. Here we show the simple conversion to the conventional form used in set.mm, using the definition given by df-sinh . See sinhval for a theorem to convert this further. See sinh-conventional for a justification that our definition is the same as the conventional definition of sinh used in other sources. (Contributed by David A. Wheeler, 20-Apr-2015)

	Ref	Expression
Assertion	sinhval-named	$$⊢A\in ℂ\to \sinh \left(A\right)=\frac{\sin \mathrm{i}A}{\mathrm{i}}$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \mathrm{i}x=\mathrm{i}A$$
2	1	fveq2d	$$⊢x=A\to \sin \mathrm{i}x=\sin \mathrm{i}A$$
3	2	oveq1d	$$⊢x=A\to \frac{\sin \mathrm{i}x}{\mathrm{i}}=\frac{\sin \mathrm{i}A}{\mathrm{i}}$$
4		df-sinh	$$⊢\sinh =\left(x\in ℂ⟼\frac{\sin \mathrm{i}x}{\mathrm{i}}\right)$$
5		ovex	$$⊢\frac{\sin \mathrm{i}A}{\mathrm{i}}\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢A\in ℂ\to \sinh \left(A\right)=\frac{\sin \mathrm{i}A}{\mathrm{i}}$$