Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  srgi Structured version   Unicode version

Theorem srgi 16736
 Description: Properties of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.)
Hypotheses
Ref Expression
srgi.b
srgi.p
srgi.t
Assertion
Ref Expression
srgi SRing

Proof of Theorem srgi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 srgi.b . . . . . . . . . . . . 13
2 eqid 2454 . . . . . . . . . . . . 13 mulGrp mulGrp
3 srgi.p . . . . . . . . . . . . 13
4 srgi.t . . . . . . . . . . . . 13
5 eqid 2454 . . . . . . . . . . . . 13
61, 2, 3, 4, 5issrg 16732 . . . . . . . . . . . 12 SRing CMnd mulGrp
76simp3bi 1005 . . . . . . . . . . 11 SRing
87r19.21bi 2920 . . . . . . . . . 10 SRing
98simpld 459 . . . . . . . . 9 SRing
109ralrimiva 2830 . . . . . . . 8 SRing
1110adantr 465 . . . . . . 7 SRing
12 simpr1 994 . . . . . . 7 SRing
13 rsp 2894 . . . . . . 7
1411, 12, 13sylc 60 . . . . . 6 SRing
15 simpr2 995 . . . . . 6 SRing
16 rsp 2894 . . . . . 6
1714, 15, 16sylc 60 . . . . 5 SRing
18 simpr3 996 . . . . 5 SRing
19 rsp 2894 . . . . 5
2017, 18, 19sylc 60 . . . 4 SRing
2120simpld 459 . . 3 SRing
2221caovdig 6388 . 2 SRing
2320simprd 463 . . 3 SRing
2423caovdirg 6391 . 2 SRing
2522, 24jca 532 1 SRing
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 965   wceq 1370   wcel 1758  wral 2799  cfv 5527  (class class class)co 6201  cbs 14293   cplusg 14358  cmulr 14359  c0g 14498  cmnd 15529  CMndccmn 16399  mulGrpcmgp 16714  SRingcsrg 16730 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4530 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-iota 5490  df-fv 5535  df-ov 6204  df-srg 16731 This theorem is referenced by:  srgdi  16740  srgdir  16741
 Copyright terms: Public domain W3C validator