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

Metamath Proof Explorer

Theorem mulrid

Description: The number 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mulrid ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 cnre ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
3 ax-icn ⊢ i ∈ ℂ
4 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
5 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) ∈ ℂ )
6 3 4 5 sylancr ⊢ ( 𝑦 ∈ ℝ → ( i · 𝑦 ) ∈ ℂ )
7 ax-1cn ⊢ 1 ∈ ℂ
8 adddir ⊢ ( ( 𝑥 ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) )
9 7 8 mp3an3 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) )
10 2 6 9 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) )
11 ax-1rid ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 · 1 ) = 𝑥 )
12 mulass ⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · 𝑦 ) · 1 ) = ( i · ( 𝑦 · 1 ) ) )
13 3 7 12 mp3an13 ⊢ ( 𝑦 ∈ ℂ → ( ( i · 𝑦 ) · 1 ) = ( i · ( 𝑦 · 1 ) ) )
14 4 13 syl ⊢ ( 𝑦 ∈ ℝ → ( ( i · 𝑦 ) · 1 ) = ( i · ( 𝑦 · 1 ) ) )
15 ax-1rid ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 · 1 ) = 𝑦 )
16 15 oveq2d ⊢ ( 𝑦 ∈ ℝ → ( i · ( 𝑦 · 1 ) ) = ( i · 𝑦 ) )
17 14 16 eqtrd ⊢ ( 𝑦 ∈ ℝ → ( ( i · 𝑦 ) · 1 ) = ( i · 𝑦 ) )
18 11 17 oveqan12d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
19 10 18 eqtrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( 𝑥 + ( i · 𝑦 ) ) )
20 oveq1 ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 · 1 ) = ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) )
21 id ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
22 20 21 eqeq12d ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝐴 · 1 ) = 𝐴 ↔ ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( 𝑥 + ( i · 𝑦 ) ) ) )
23 19 22 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 · 1 ) = 𝐴 ) )
24 23 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 · 1 ) = 𝐴 )
25 1 24 syl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )