Theorem sn-1ticom

Description: Lemma for sn-mullid and sn-it1ei . (Contributed by SN, 27-May-2024)

	Ref	Expression
Assertion	sn-1ticom	$$⊢1\mathrm{i}=\mathrm{i}\cdot 1$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2	1 1	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
3	2 2 1	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
4	1 2	mulcli	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\in ℂ$$
5	1 1 4	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
6	1 1 1	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}$$
7	6	oveq2i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
8	1 1 2	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
9	8	oveq2i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
10	5 7 9	3eqtr4i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
11	3 10	eqtri	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
12		rei4	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$
13	12	oveq1i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1\mathrm{i}$$
14	12	oveq2i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\cdot 1$$
15	11 13 14	3eqtr3i	$$⊢1\mathrm{i}=\mathrm{i}\cdot 1$$