MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulid1 Structured version   Visualization version   GIF version

Theorem mulid1 9725
Description: 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
mulid1 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)

Proof of Theorem mulid1
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 9724 . 2 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
2 recn 9714 . . . . . 6 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
3 ax-icn 9683 . . . . . . 7 i ∈ ℂ
4 recn 9714 . . . . . . 7 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
5 mulcl 9708 . . . . . . 7 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
63, 4, 5sylancr 685 . . . . . 6 (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
7 ax-1cn 9682 . . . . . . 7 1 ∈ ℂ
8 adddir 9719 . . . . . . 7 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
97, 8mp3an3 1395 . . . . . 6 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
102, 6, 9syl2an 487 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
11 ax-1rid 9694 . . . . . 6 (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥)
12 mulass 9712 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
133, 7, 12mp3an13 1397 . . . . . . . 8 (𝑦 ∈ ℂ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
144, 13syl 17 . . . . . . 7 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
15 ax-1rid 9694 . . . . . . . 8 (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦)
1615oveq2d 6379 . . . . . . 7 (𝑦 ∈ ℝ → (i · (𝑦 · 1)) = (i · 𝑦))
1714, 16eqtrd 2539 . . . . . 6 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · 𝑦))
1811, 17oveqan12d 6382 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i · 𝑦) · 1)) = (𝑥 + (i · 𝑦)))
1910, 18eqtrd 2539 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))
20 oveq1 6370 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1))
21 id 22 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦)))
2220, 21eqeq12d 2520 . . . 4 (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))))
2319, 22syl5ibrcom 232 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴))
2423rexlimivv 2911 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)
251, 24syl 17 1 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 378   = wceq 1468  wcel 1937  wrex 2792  (class class class)co 6363  cc 9622  cr 9623  1c1 9625  ici 9626   + caddc 9627   · cmul 9629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-resscn 9681  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-mulcl 9686  ax-mulcom 9688  ax-mulass 9690  ax-distr 9691  ax-1rid 9694  ax-cnre 9697
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-iota 5597  df-fv 5641  df-ov 6366
This theorem is referenced by:  mulid2  9726  mulid1i  9730  mulid1d  9745  muleqadd  10345  divdiv1  10407  conjmul  10413  nnmulcl  10721  expmul  12431  binom21  12504  sq01  12508  bernneq  12512  hashiun  14042  fprodcvg  14144  prodmolem2a  14148  efexp  14315  cncrng  19147  cnfld1  19151  0dgr  23360  ecxp  23779  dvcxp1  23841  dvcncxp1  23844  efrlim  24056  lgsdilem2  24420  axcontlem7  25161  gxnn0mul  26168  cnrngo  26294  ipasslem2  26636  addltmulALT  28262  zrhnm  28928  2even  41123
  Copyright terms: Public domain W3C validator