This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-mullid

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

Ref Expression
Assertion sn-mullid ( 𝐴 ∈ ℂ → ( 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 remullid ⊢ ( 𝑥 ∈ ℝ → ( 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 remullid ⊢ ( 𝑦 ∈ ℝ → ( 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 · 𝐴 ) = 𝐴 )