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	⊢ ( i · 1 ) = i

Proof

Step	Hyp	Ref	Expression
1		sn-1ticom	⊢ ( 1 · i ) = ( i · 1 )
2		ax-icn	⊢ i ∈ ℂ
3		sn-mulid2	⊢ ( i ∈ ℂ → ( 1 · i ) = i )
4	2 3	ax-mp	⊢ ( 1 · i ) = i
5	1 4	eqtr3i	⊢ ( i · 1 ) = i