Theorem it1ei

Description: 1 is a multiplicative identity for _i (see sn-mulid2 for commuted version). (Contributed by SN, 1-Jun-2024)

	Ref	Expression
Assertion	it1ei	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$

Proof

Step	Hyp	Ref	Expression
1		sn-1ticom	$$⊢1\mathrm{i}=\mathrm{i}\cdot 1$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		sn-mulid2	$$⊢\mathrm{i}\in ℂ\to 1\mathrm{i}=\mathrm{i}$$
4	2 3	ax-mp	$$⊢1\mathrm{i}=\mathrm{i}$$
5	1 4	eqtr3i	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$