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

Theorem ax1rid 9835
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, derived from ZF set theory. Weakened from the original axiom in the form of statement in mulid1 9890, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 9859. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ax1rid (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Proof of Theorem ax1rid
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-r 9799 . 2 ℝ = (R × {0R})
2 oveq1 6531 . . 3 (⟨𝑥, 𝑦⟩ = 𝐴 → (⟨𝑥, 𝑦⟩ · 1) = (𝐴 · 1))
3 id 22 . . 3 (⟨𝑥, 𝑦⟩ = 𝐴 → ⟨𝑥, 𝑦⟩ = 𝐴)
42, 3eqeq12d 2621 . 2 (⟨𝑥, 𝑦⟩ = 𝐴 → ((⟨𝑥, 𝑦⟩ · 1) = ⟨𝑥, 𝑦⟩ ↔ (𝐴 · 1) = 𝐴))
5 elsni 4138 . . 3 (𝑦 ∈ {0R} → 𝑦 = 0R)
6 df-1 9797 . . . . . . 7 1 = ⟨1R, 0R
76oveq2i 6535 . . . . . 6 (⟨𝑥, 0R⟩ · 1) = (⟨𝑥, 0R⟩ · ⟨1R, 0R⟩)
8 1sr 9755 . . . . . . . 8 1RR
9 mulresr 9813 . . . . . . . 8 ((𝑥R ∧ 1RR) → (⟨𝑥, 0R⟩ · ⟨1R, 0R⟩) = ⟨(𝑥 ·R 1R), 0R⟩)
108, 9mpan2 702 . . . . . . 7 (𝑥R → (⟨𝑥, 0R⟩ · ⟨1R, 0R⟩) = ⟨(𝑥 ·R 1R), 0R⟩)
11 1idsr 9772 . . . . . . . 8 (𝑥R → (𝑥 ·R 1R) = 𝑥)
1211opeq1d 4337 . . . . . . 7 (𝑥R → ⟨(𝑥 ·R 1R), 0R⟩ = ⟨𝑥, 0R⟩)
1310, 12eqtrd 2640 . . . . . 6 (𝑥R → (⟨𝑥, 0R⟩ · ⟨1R, 0R⟩) = ⟨𝑥, 0R⟩)
147, 13syl5eq 2652 . . . . 5 (𝑥R → (⟨𝑥, 0R⟩ · 1) = ⟨𝑥, 0R⟩)
15 opeq2 4332 . . . . . . 7 (𝑦 = 0R → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 0R⟩)
1615oveq1d 6539 . . . . . 6 (𝑦 = 0R → (⟨𝑥, 𝑦⟩ · 1) = (⟨𝑥, 0R⟩ · 1))
1716, 15eqeq12d 2621 . . . . 5 (𝑦 = 0R → ((⟨𝑥, 𝑦⟩ · 1) = ⟨𝑥, 𝑦⟩ ↔ (⟨𝑥, 0R⟩ · 1) = ⟨𝑥, 0R⟩))
1814, 17syl5ibr 234 . . . 4 (𝑦 = 0R → (𝑥R → (⟨𝑥, 𝑦⟩ · 1) = ⟨𝑥, 𝑦⟩))
1918impcom 444 . . 3 ((𝑥R𝑦 = 0R) → (⟨𝑥, 𝑦⟩ · 1) = ⟨𝑥, 𝑦⟩)
205, 19sylan2 489 . 2 ((𝑥R𝑦 ∈ {0R}) → (⟨𝑥, 𝑦⟩ · 1) = ⟨𝑥, 𝑦⟩)
211, 4, 20optocl 5105 1 (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  {csn 4121  cop 4127  (class class class)co 6524  Rcnr 9540  0Rc0r 9541  1Rc1r 9542   ·R cmr 9545  cr 9788  1c1 9790   · cmul 9794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-omul 7426  df-er 7603  df-ec 7605  df-qs 7609  df-ni 9547  df-pli 9548  df-mi 9549  df-lti 9550  df-plpq 9583  df-mpq 9584  df-ltpq 9585  df-enq 9586  df-nq 9587  df-erq 9588  df-plq 9589  df-mq 9590  df-1nq 9591  df-rq 9592  df-ltnq 9593  df-np 9656  df-1p 9657  df-plp 9658  df-mp 9659  df-ltp 9660  df-enr 9730  df-nr 9731  df-plr 9732  df-mr 9733  df-0r 9735  df-1r 9736  df-m1r 9737  df-c 9795  df-1 9797  df-r 9799  df-mul 9801
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator