Theorem sn-mulid2

Description: mulid2 without ax-mulcom . (Contributed by SN, 27-May-2024)

	Ref	Expression
Assertion	sn-mulid2	$$⊢A\in ℂ\to 1A=A$$

Proof

Step	Hyp	Ref	Expression
1		cnre	$$⊢A\in ℂ\to \exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y$$
2		1cnd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1\in ℂ$$
3		recn	$$⊢x\in ℝ\to x\in ℂ$$
4	3	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6	5	a1i	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\in ℂ$$
7		recn	$$⊢y\in ℝ\to y\in ℂ$$
8	7	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to y\in ℂ$$
9	6 8	mulcld	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}y\in ℂ$$
10	2 4 9	adddid	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1\left(x+\mathrm{i}y\right)=1x+1\mathrm{i}y$$
11		remulid2	$$⊢x\in ℝ\to 1x=x$$
12	11	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1x=x$$
13	2 6 8	mulassd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1\mathrm{i}y=1\mathrm{i}y$$
14		sn-1ticom	$$⊢1\mathrm{i}=\mathrm{i}\cdot 1$$
15	14	oveq1i	$$⊢1\mathrm{i}y=\mathrm{i}\cdot 1y$$
16	15	a1i	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1\mathrm{i}y=\mathrm{i}\cdot 1y$$
17	6 2 8	mulassd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}\cdot 1y=\mathrm{i}1y$$
18		remulid2	$$⊢y\in ℝ\to 1y=y$$
19	18	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1y=y$$
20	19	oveq2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \mathrm{i}1y=\mathrm{i}y$$
21	16 17 20	3eqtrd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1\mathrm{i}y=\mathrm{i}y$$
22	13 21	eqtr3d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1\mathrm{i}y=\mathrm{i}y$$
23	12 22	oveq12d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1x+1\mathrm{i}y=x+\mathrm{i}y$$
24	10 23	eqtrd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to 1\left(x+\mathrm{i}y\right)=x+\mathrm{i}y$$
25		oveq2	$$⊢A=x+\mathrm{i}y\to 1A=1\left(x+\mathrm{i}y\right)$$
26		id	$$⊢A=x+\mathrm{i}y\to A=x+\mathrm{i}y$$
27	25 26	eqeq12d	$$⊢A=x+\mathrm{i}y\to \left(1A=A\leftrightarrow 1\left(x+\mathrm{i}y\right)=x+\mathrm{i}y\right)$$
28	24 27	syl5ibrcom	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(A=x+\mathrm{i}y\to 1A=A\right)$$
29	28	rexlimivv	$$⊢\exists x\in ℝ\exists y\in ℝA=x+\mathrm{i}y\to 1A=A$$
30	1 29	syl	$$⊢A\in ℂ\to 1A=A$$