Theorem sn-mulid2

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

	Ref	Expression
Assertion	sn-mulid2	⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cnre	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2		1cnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ )
3		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
4	3	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℂ )
5		ax-icn	⊢ i ∈ ℂ
6	5	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → i ∈ ℂ )
7		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
8	7	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
9	6 8	mulcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · 𝑦 ) ∈ ℂ )
10	2 4 9	adddid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( 1 · 𝑥 ) + ( 1 · ( i · 𝑦 ) ) ) )
11		remulid2	⊢ ( 𝑥 ∈ ℝ → ( 1 · 𝑥 ) = 𝑥 )
12	11	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 · 𝑥 ) = 𝑥 )
13	2 6 8	mulassd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 · i ) · 𝑦 ) = ( 1 · ( i · 𝑦 ) ) )
14		sn-1ticom	⊢ ( 1 · i ) = ( i · 1 )
15	14	oveq1i	⊢ ( ( 1 · i ) · 𝑦 ) = ( ( i · 1 ) · 𝑦 )
16	15	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 · i ) · 𝑦 ) = ( ( i · 1 ) · 𝑦 ) )
17	6 2 8	mulassd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · 1 ) · 𝑦 ) = ( i · ( 1 · 𝑦 ) ) )
18		remulid2	⊢ ( 𝑦 ∈ ℝ → ( 1 · 𝑦 ) = 𝑦 )
19	18	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 · 𝑦 ) = 𝑦 )
20	19	oveq2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · ( 1 · 𝑦 ) ) = ( i · 𝑦 ) )
21	16 17 20	3eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 · i ) · 𝑦 ) = ( i · 𝑦 ) )
22	13 21	eqtr3d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 · ( i · 𝑦 ) ) = ( i · 𝑦 ) )
23	12 22	oveq12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 1 · 𝑥 ) + ( 1 · ( i · 𝑦 ) ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
24	10 23	eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 1 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
25		oveq2	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 1 · 𝐴 ) = ( 1 · ( 𝑥 + ( i · 𝑦 ) ) ) )
26		id	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
27	25 26	eqeq12d	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 1 · 𝐴 ) = 𝐴 ↔ ( 1 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( 𝑥 + ( i · 𝑦 ) ) ) )
28	24 27	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 1 · 𝐴 ) = 𝐴 ) )
29	28	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 1 · 𝐴 ) = 𝐴 )
30	1 29	syl	⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )