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

Theorem dfrhm2 17883
 Description: The property of a ring homomorphism can be decomposed into separate homomorphic conditions for addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Assertion
Ref Expression
dfrhm2 RingHom mulGrp MndHom mulGrp
Distinct variable group:   ,

Proof of Theorem dfrhm2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-rnghom 17881 . 2 RingHom
2 ringgrp 17723 . . . . . . . 8
3 ringgrp 17723 . . . . . . . 8
4 eqid 2423 . . . . . . . . 9
5 eqid 2423 . . . . . . . . 9
6 eqid 2423 . . . . . . . . 9
7 eqid 2423 . . . . . . . . 9
84, 5, 6, 7isghm3 16822 . . . . . . . 8
92, 3, 8syl2an 479 . . . . . . 7
109abbi2dv 2542 . . . . . 6
11 df-rab 2718 . . . . . . 7
12 fvex 5830 . . . . . . . . . 10
13 fvex 5830 . . . . . . . . . 10
1412, 13elmap 7450 . . . . . . . . 9
1514anbi1i 699 . . . . . . . 8
1615abbii 2539 . . . . . . 7
1711, 16eqtri 2445 . . . . . 6
1810, 17syl6eqr 2475 . . . . 5
19 eqid 2423 . . . . . . . . 9 mulGrp mulGrp
2019ringmgp 17724 . . . . . . . 8 mulGrp
21 eqid 2423 . . . . . . . . 9 mulGrp mulGrp
2221ringmgp 17724 . . . . . . . 8 mulGrp
2319, 4mgpbas 17667 . . . . . . . . . 10 mulGrp
2421, 5mgpbas 17667 . . . . . . . . . 10 mulGrp
25 eqid 2423 . . . . . . . . . . 11
2619, 25mgpplusg 17665 . . . . . . . . . 10 mulGrp
27 eqid 2423 . . . . . . . . . . 11
2821, 27mgpplusg 17665 . . . . . . . . . 10 mulGrp
29 eqid 2423 . . . . . . . . . . 11
3019, 29ringidval 17675 . . . . . . . . . 10 mulGrp
31 eqid 2423 . . . . . . . . . . 11
3221, 31ringidval 17675 . . . . . . . . . 10 mulGrp
3323, 24, 26, 28, 30, 32ismhm 16522 . . . . . . . . 9 mulGrp MndHom mulGrp mulGrp mulGrp
3433baib 911 . . . . . . . 8 mulGrp mulGrp mulGrp MndHom mulGrp
3520, 22, 34syl2an 479 . . . . . . 7 mulGrp MndHom mulGrp
3635abbi2dv 2542 . . . . . 6 mulGrp MndHom mulGrp
37 df-rab 2718 . . . . . . 7
3814anbi1i 699 . . . . . . . . 9
39 3anass 986 . . . . . . . . 9
4038, 39bitr4i 255 . . . . . . . 8
4140abbii 2539 . . . . . . 7
4237, 41eqtri 2445 . . . . . 6
4336, 42syl6eqr 2475 . . . . 5 mulGrp MndHom mulGrp
4418, 43ineq12d 3603 . . . 4 mulGrp MndHom mulGrp
45 ancom 451 . . . . . . . 8
46 r19.26-2 2890 . . . . . . . . 9
4746anbi1i 699 . . . . . . . 8
48 anass 653 . . . . . . . 8
4945, 47, 483bitri 274 . . . . . . 7
5049a1i 11 . . . . . 6
5150rabbiia 3005 . . . . 5
52 oveq12 6253 . . . . . . . 8
5352ancoms 454 . . . . . . 7
54 raleq 2959 . . . . . . . . . 10
5554raleqbi1dv 2967 . . . . . . . . 9
5655adantr 466 . . . . . . . 8
5756anbi2d 708 . . . . . . 7
5853, 57rabeqbidv 3012 . . . . . 6
5913, 12, 58csbie2 3363 . . . . 5
60 inrab 3683 . . . . 5
6151, 59, 603eqtr4i 2455 . . . 4
6244, 61syl6reqr 2476 . . 3 mulGrp MndHom mulGrp
6362mpt2eq3ia 6309 . 2 mulGrp MndHom mulGrp
641, 63eqtri 2445 1 RingHom mulGrp MndHom mulGrp
 Colors of variables: wff setvar class Syntax hints:   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  cab 2409  wral 2709  crab 2713  csb 3333   cin 3373  wf 5535  cfv 5539  (class class class)co 6244   cmpt2 6246   cmap 7422  cbs 15059   cplusg 15128  cmulr 15129  cmnd 16473   MndHom cmhm 16518  cgrp 16607   cghm 16818  mulGrpcmgp 17661  cur 17673  crg 17718   RingHom crh 17878 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-map 7424  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556  df-2 10614  df-ndx 15062  df-slot 15063  df-base 15064  df-sets 15065  df-plusg 15141  df-0g 15278  df-mhm 16520  df-ghm 16819  df-mgp 17662  df-ur 17674  df-ring 17720  df-rnghom 17881 This theorem is referenced by:  rhmrcl1  17885  rhmrcl2  17886  isrhm  17887  zrhval  19016  rhmfn  39509  rhmval  39510  rhmsubclem1  39679  rhmsubcALTVlem1  39698
 Copyright terms: Public domain W3C validator