Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isrnghm Structured version   Unicode version

Theorem isrnghm 39477
 Description: A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020.)
Hypotheses
Ref Expression
isrnghm.b
isrnghm.t
isrnghm.m
Assertion
Ref Expression
isrnghm RngHomo Rng Rng
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem isrnghm
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rnghmrcl 39474 . 2 RngHomo Rng Rng
2 isrnghm.b . . . . 5
3 isrnghm.t . . . . 5
4 isrnghm.m . . . . 5
5 eqid 2422 . . . . 5
6 eqid 2422 . . . . 5
7 eqid 2422 . . . . 5
82, 3, 4, 5, 6, 7rnghmval 39476 . . . 4 Rng Rng RngHomo
98eleq2d 2485 . . 3 Rng Rng RngHomo
10 fveq1 5817 . . . . . . . 8
11 fveq1 5817 . . . . . . . . 9
12 fveq1 5817 . . . . . . . . 9
1311, 12oveq12d 6260 . . . . . . . 8
1410, 13eqeq12d 2437 . . . . . . 7
15 fveq1 5817 . . . . . . . 8
1611, 12oveq12d 6260 . . . . . . . 8
1715, 16eqeq12d 2437 . . . . . . 7
1814, 17anbi12d 715 . . . . . 6
19182ralbidv 2803 . . . . 5
2019elrab 3164 . . . 4
21 r19.26-2 2889 . . . . . . 7
2221anbi2i 698 . . . . . 6
23 anass 653 . . . . . 6
2422, 23bitr4i 255 . . . . 5
252, 5, 6, 7isghm 16819 . . . . . . 7
26 fvex 5828 . . . . . . . . . . 11
27 fvex 5828 . . . . . . . . . . . 12
282, 27eqeltri 2496 . . . . . . . . . . 11
2926, 28pm3.2i 456 . . . . . . . . . 10
30 elmapg 7433 . . . . . . . . . 10
3129, 30mp1i 13 . . . . . . . . 9 Rng Rng
3231anbi1d 709 . . . . . . . 8 Rng Rng
33 rngabl 39462 . . . . . . . . . 10 Rng
34 ablgrp 17371 . . . . . . . . . 10
3533, 34syl 17 . . . . . . . . 9 Rng
36 rngabl 39462 . . . . . . . . . 10 Rng
37 ablgrp 17371 . . . . . . . . . 10
3836, 37syl 17 . . . . . . . . 9 Rng
39 ibar 506 . . . . . . . . 9
4035, 38, 39syl2an 479 . . . . . . . 8 Rng Rng
4132, 40bitr2d 257 . . . . . . 7 Rng Rng
4225, 41syl5rbb 261 . . . . . 6 Rng Rng
4342anbi1d 709 . . . . 5 Rng Rng
4424, 43syl5bb 260 . . . 4 Rng Rng
4520, 44syl5bb 260 . . 3 Rng Rng
469, 45bitrd 256 . 2 Rng Rng RngHomo
471, 46biadan2 646 1 RngHomo Rng Rng
 Colors of variables: wff setvar class Syntax hints:   wb 187   wa 370   wceq 1437   wcel 1872  wral 2708  crab 2712  cvv 3016  wf 5533  cfv 5537  (class class class)co 6242   cmap 7420  cbs 15057   cplusg 15126  cmulr 15127  cgrp 16605   cghm 16816  cabl 17367  Rngcrng 39459   RngHomo crngh 39470 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 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-reu 2715  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-op 3941  df-uni 4156  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-id 4704  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-map 7422  df-ghm 16817  df-abl 17369  df-rng0 39460  df-rnghomo 39472 This theorem is referenced by:  isrnghmmul  39478  rnghmghm  39483  rnghmmul  39485  isrnghm2d  39486  zrrnghm  39502
 Copyright terms: Public domain W3C validator