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

Theorem abvrcl 20968
Description: Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.)
Hypothesis
Ref Expression
abvf.a 𝐴 = (AbsVal‘𝑅)
Assertion
Ref Expression
abvrcl (𝐹𝐴𝑅 ∈ Ring)

Proof of Theorem abvrcl
Dummy variables 𝑥 𝑦 𝑓 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-abv 20964 . . 3 AbsVal = (𝑟 ∈ Ring ↦ {𝑓 ∈ ((0[,)+∞) ↑m (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)(((𝑓𝑥) = 0 ↔ 𝑥 = (0g𝑟)) ∧ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(.r𝑟)𝑦)) = ((𝑓𝑥) · (𝑓𝑦)) ∧ (𝑓‘(𝑥(+g𝑟)𝑦)) ≤ ((𝑓𝑥) + (𝑓𝑦))))})
21mptrcl 7003 . 2 (𝐹 ∈ (AbsVal‘𝑅) → 𝑅 ∈ Ring)
3 abvf.a . 2 𝐴 = (AbsVal‘𝑅)
42, 3eleq2s 2883 1 (𝐹𝐴𝑅 ∈ Ring)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wi 4  wb 209  wa 401   = wceq 1570  wcel 2146  wral 3081  {crab 3418   class class class wbr 5111  cfv 6540  (class class class)co 7419  m cmap 8830  0cc0 11117   + caddc 11120   · cmul 11122  +∞cpnf 11257  cle 11261  [,)cico 13392  Basecbs 17293  +gcplusg 17334  .rcmulr 17335  0gc0g 17516  Ringcrg 20361  AbsValcabv 20963
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-xp 5669  df-rel 5670  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fv 6548  df-abv 20964
This theorem is used by:  abvfge0  20969  abveq0  20973  abvmul  20976  abvtri  20977  abv0  20978  abv1z  20979  abvneg  20981  abvsubtri  20982  abvpropd  20990  abvmet  24785  nrgring  24873  tngnrg  24884  abvcxp  27832
  Copyright terms: Public domain W3C validator