Theorem sn-mul02

Description: mul02 without ax-mulcom . See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md for an outline. (Contributed by SN, 30-Jun-2024)

	Ref	Expression
Assertion	sn-mul02	⊢ ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		cnre	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2		0cnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 0 ∈ ℂ )
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	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( 0 · 𝑥 ) + ( 0 · ( i · 𝑦 ) ) ) )
11		remul02	⊢ ( 𝑥 ∈ ℝ → ( 0 · 𝑥 ) = 0 )
12	11	adantr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · 𝑥 ) = 0 )
13		sn-0tie0	⊢ ( 0 · i ) = 0
14	13	oveq1i	⊢ ( ( 0 · i ) · 𝑦 ) = ( 0 · 𝑦 )
15	2 6 8	mulassd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 · i ) · 𝑦 ) = ( 0 · ( i · 𝑦 ) ) )
16		remul02	⊢ ( 𝑦 ∈ ℝ → ( 0 · 𝑦 ) = 0 )
17	16	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · 𝑦 ) = 0 )
18	14 15 17	3eqtr3a	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · ( i · 𝑦 ) ) = 0 )
19	12 18	oveq12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 · 𝑥 ) + ( 0 · ( i · 𝑦 ) ) ) = ( 0 + 0 ) )
20		sn-00id	⊢ ( 0 + 0 ) = 0
21	19 20	eqtrdi	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 · 𝑥 ) + ( 0 · ( i · 𝑦 ) ) ) = 0 )
22	10 21	eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = 0 )
23		oveq2	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 𝐴 ) = ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) )
24	23	eqeq1d	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 0 · 𝐴 ) = 0 ↔ ( 0 · ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) )
25	22 24	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 𝐴 ) = 0 ) )
26	25	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 0 · 𝐴 ) = 0 )
27	1 26	syl	⊢ ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 )