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

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

Proof of Theorem mulrid
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 11256 . 2 (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
2 recn 11243 . . . . . 6 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
3 ax-icn 11212 . . . . . . 7 i ∈ ℂ
4 recn 11243 . . . . . . 7 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
5 mulcl 11237 . . . . . . 7 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
63, 4, 5sylancr 587 . . . . . 6 (𝑦 ∈ ℝ → (i · 𝑦) ∈ ℂ)
7 ax-1cn 11211 . . . . . . 7 1 ∈ ℂ
8 adddir 11250 . . . . . . 7 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
97, 8mp3an3 1449 . . . . . 6 ((𝑥 ∈ ℂ ∧ (i · 𝑦) ∈ ℂ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
102, 6, 9syl2an 596 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = ((𝑥 · 1) + ((i · 𝑦) · 1)))
11 ax-1rid 11223 . . . . . 6 (𝑥 ∈ ℝ → (𝑥 · 1) = 𝑥)
12 mulass 11241 . . . . . . . . 9 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
133, 7, 12mp3an13 1451 . . . . . . . 8 (𝑦 ∈ ℂ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
144, 13syl 17 . . . . . . 7 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · (𝑦 · 1)))
15 ax-1rid 11223 . . . . . . . 8 (𝑦 ∈ ℝ → (𝑦 · 1) = 𝑦)
1615oveq2d 7447 . . . . . . 7 (𝑦 ∈ ℝ → (i · (𝑦 · 1)) = (i · 𝑦))
1714, 16eqtrd 2775 . . . . . 6 (𝑦 ∈ ℝ → ((i · 𝑦) · 1) = (i · 𝑦))
1811, 17oveqan12d 7450 . . . . 5 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 · 1) + ((i · 𝑦) · 1)) = (𝑥 + (i · 𝑦)))
1910, 18eqtrd 2775 . . . 4 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦)))
20 oveq1 7438 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = ((𝑥 + (i · 𝑦)) · 1))
21 id 22 . . . . 5 (𝐴 = (𝑥 + (i · 𝑦)) → 𝐴 = (𝑥 + (i · 𝑦)))
2220, 21eqeq12d 2751 . . . 4 (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 1) = 𝐴 ↔ ((𝑥 + (i · 𝑦)) · 1) = (𝑥 + (i · 𝑦))))
2319, 22syl5ibrcom 247 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴))
2423rexlimivv 3199 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → (𝐴 · 1) = 𝐴)
251, 24syl 17 1 (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  wrex 3068  (class class class)co 7431  cc 11151  cr 11152  1c1 11154  ici 11155   + caddc 11156   · cmul 11158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-mulcl 11215  ax-mulcom 11217  ax-mulass 11219  ax-distr 11220  ax-1rid 11223  ax-cnre 11226
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434
This theorem is referenced by:  mullid  11258  mulridi  11263  mulridd  11276  muleqadd  11905  divdiv1  11976  conjmul  11982  expmul  14145  binom21  14255  binom2sub1  14257  sq01  14261  bernneq  14265  hashiun  15855  fprodcvg  15963  prodmolem2a  15967  efexp  16134  cncrng  21419  cncrngOLD  21420  cnfld1  21424  cnfld1OLD  21425  0dgr  26299  ecxp  26730  dvcxp1  26797  dvcncxp1  26800  efrlim  27027  efrlimOLD  27028  lgsdilem2  27392  axcontlem7  29000  ipasslem2  30861  addltmulALT  32475  0dp2dp  32876  zrhnm  33930  2even  48083
  Copyright terms: Public domain W3C validator