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

Theorem 0idsr 10954
Description: The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.)
Assertion
Ref Expression
0idsr (𝐴R → (𝐴 +R 0R) = 𝐴)

Proof of Theorem 0idsr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nr 10913 . 2 R = ((P × P) / ~R )
2 oveq1 7344 . . 3 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → ([⟨𝑥, 𝑦⟩] ~R +R 0R) = (𝐴 +R 0R))
3 id 22 . . 3 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → [⟨𝑥, 𝑦⟩] ~R = 𝐴)
42, 3eqeq12d 2752 . 2 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → (([⟨𝑥, 𝑦⟩] ~R +R 0R) = [⟨𝑥, 𝑦⟩] ~R ↔ (𝐴 +R 0R) = 𝐴))
5 df-0r 10917 . . . 4 0R = [⟨1P, 1P⟩] ~R
65oveq2i 7348 . . 3 ([⟨𝑥, 𝑦⟩] ~R +R 0R) = ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R )
7 1pr 10872 . . . . 5 1PP
8 addsrpr 10932 . . . . 5 (((𝑥P𝑦P) ∧ (1PP ∧ 1PP)) → ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R ) = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R )
97, 7, 8mpanr12 702 . . . 4 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R ) = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R )
10 addclpr 10875 . . . . . . 7 ((𝑥P ∧ 1PP) → (𝑥 +P 1P) ∈ P)
117, 10mpan2 688 . . . . . 6 (𝑥P → (𝑥 +P 1P) ∈ P)
12 addclpr 10875 . . . . . . 7 ((𝑦P ∧ 1PP) → (𝑦 +P 1P) ∈ P)
137, 12mpan2 688 . . . . . 6 (𝑦P → (𝑦 +P 1P) ∈ P)
1411, 13anim12i 613 . . . . 5 ((𝑥P𝑦P) → ((𝑥 +P 1P) ∈ P ∧ (𝑦 +P 1P) ∈ P))
15 vex 3445 . . . . . . 7 𝑥 ∈ V
16 vex 3445 . . . . . . 7 𝑦 ∈ V
177elexi 3460 . . . . . . 7 1P ∈ V
18 addcompr 10878 . . . . . . 7 (𝑧 +P 𝑤) = (𝑤 +P 𝑧)
19 addasspr 10879 . . . . . . 7 ((𝑧 +P 𝑤) +P 𝑣) = (𝑧 +P (𝑤 +P 𝑣))
2015, 16, 17, 18, 19caov12 7562 . . . . . 6 (𝑥 +P (𝑦 +P 1P)) = (𝑦 +P (𝑥 +P 1P))
21 enreceq 10923 . . . . . 6 (((𝑥P𝑦P) ∧ ((𝑥 +P 1P) ∈ P ∧ (𝑦 +P 1P) ∈ P)) → ([⟨𝑥, 𝑦⟩] ~R = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R ↔ (𝑥 +P (𝑦 +P 1P)) = (𝑦 +P (𝑥 +P 1P))))
2220, 21mpbiri 257 . . . . 5 (((𝑥P𝑦P) ∧ ((𝑥 +P 1P) ∈ P ∧ (𝑦 +P 1P) ∈ P)) → [⟨𝑥, 𝑦⟩] ~R = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R )
2314, 22mpdan 684 . . . 4 ((𝑥P𝑦P) → [⟨𝑥, 𝑦⟩] ~R = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R )
249, 23eqtr4d 2779 . . 3 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R ) = [⟨𝑥, 𝑦⟩] ~R )
256, 24eqtrid 2788 . 2 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R +R 0R) = [⟨𝑥, 𝑦⟩] ~R )
261, 4, 25ecoptocl 8667 1 (𝐴R → (𝐴 +R 0R) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  cop 4579  (class class class)co 7337  [cec 8567  Pcnp 10716  1Pc1p 10717   +P cpp 10718   ~R cer 10721  Rcnr 10722  0Rc0r 10723   +R cplr 10726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-ov 7340  df-oprab 7341  df-mpo 7342  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-oadd 8371  df-omul 8372  df-er 8569  df-ec 8571  df-qs 8575  df-ni 10729  df-pli 10730  df-mi 10731  df-lti 10732  df-plpq 10765  df-mpq 10766  df-ltpq 10767  df-enq 10768  df-nq 10769  df-erq 10770  df-plq 10771  df-mq 10772  df-1nq 10773  df-rq 10774  df-ltnq 10775  df-np 10838  df-1p 10839  df-plp 10840  df-ltp 10842  df-enr 10912  df-nr 10913  df-plr 10914  df-0r 10917
This theorem is referenced by:  addgt0sr  10961  sqgt0sr  10963  map2psrpr  10967  supsrlem  10968  addresr  10995  mulresr  10996  axi2m1  11016  axcnre  11021
  Copyright terms: Public domain W3C validator