Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elzrhunit Structured version   Visualization version   GIF version

Theorem elzrhunit 31438
 Description: Condition for the image by ℤRHom to be a unit. (Contributed by Thierry Arnoux, 30-Oct-2017.)
Hypotheses
Ref Expression
zrhker.0 𝐵 = (Base‘𝑅)
zrhker.1 𝐿 = (ℤRHom‘𝑅)
zrhker.2 0 = (0g𝑅)
Assertion
Ref Expression
elzrhunit (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝐿𝑀) ∈ (Unit‘𝑅))

Proof of Theorem elzrhunit
StepHypRef Expression
1 simpll 767 . . 3 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → 𝑅 ∈ DivRing)
2 drngring 19567 . . 3 (𝑅 ∈ DivRing → 𝑅 ∈ Ring)
3 zrhker.1 . . . . 5 𝐿 = (ℤRHom‘𝑅)
43zrhrhm 20271 . . . 4 (𝑅 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑅))
5 zringbas 20234 . . . . 5 ℤ = (Base‘ℤring)
6 zrhker.0 . . . . 5 𝐵 = (Base‘𝑅)
75, 6rhmf 19539 . . . 4 (𝐿 ∈ (ℤring RingHom 𝑅) → 𝐿:ℤ⟶𝐵)
8 ffn 6496 . . . 4 (𝐿:ℤ⟶𝐵𝐿 Fn ℤ)
94, 7, 83syl 18 . . 3 (𝑅 ∈ Ring → 𝐿 Fn ℤ)
101, 2, 93syl 18 . 2 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → 𝐿 Fn ℤ)
11 simprl 771 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → 𝑀 ∈ ℤ)
12 elsng 4534 . . . . . . 7 (𝑀 ∈ ℤ → (𝑀 ∈ {0} ↔ 𝑀 = 0))
1312necon3bbid 2989 . . . . . 6 (𝑀 ∈ ℤ → (¬ 𝑀 ∈ {0} ↔ 𝑀 ≠ 0))
1413biimpar 482 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → ¬ 𝑀 ∈ {0})
1514adantl 486 . . . 4 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ¬ 𝑀 ∈ {0})
1611, 15eldifd 3870 . . 3 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → 𝑀 ∈ (ℤ ∖ {0}))
17 zrhker.2 . . . . 5 0 = (0g𝑅)
186, 3, 17zrhunitpreima 31437 . . . 4 ((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) → (𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0}))
1918adantr 485 . . 3 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝐿 “ (Unit‘𝑅)) = (ℤ ∖ {0}))
2016, 19eleqtrrd 2856 . 2 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → 𝑀 ∈ (𝐿 “ (Unit‘𝑅)))
21 elpreima 6817 . . 3 (𝐿 Fn ℤ → (𝑀 ∈ (𝐿 “ (Unit‘𝑅)) ↔ (𝑀 ∈ ℤ ∧ (𝐿𝑀) ∈ (Unit‘𝑅))))
2221simplbda 504 . 2 ((𝐿 Fn ℤ ∧ 𝑀 ∈ (𝐿 “ (Unit‘𝑅))) → (𝐿𝑀) ∈ (Unit‘𝑅))
2310, 20, 22syl2anc 588 1 (((𝑅 ∈ DivRing ∧ (chr‘𝑅) = 0) ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → (𝐿𝑀) ∈ (Unit‘𝑅))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112   ≠ wne 2952   ∖ cdif 3856  {csn 4520  ◡ccnv 5521   “ cima 5525   Fn wfn 6328  ⟶wf 6329  ‘cfv 6333  (class class class)co 7148  0cc0 10565  ℤcz 12010  Basecbs 16531  0gc0g 16761  Ringcrg 19355  Unitcui 19450   RingHom crh 19525  DivRingcdr 19560  ℤringzring 20228  ℤRHomczrh 20259  chrcchr 20261 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642  ax-pre-sup 10643  ax-addf 10644  ax-mulf 10645 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-tp 4525  df-op 4527  df-uni 4797  df-int 4837  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5428  df-eprel 5433  df-po 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7578  df-1st 7691  df-2nd 7692  df-wrecs 7955  df-recs 8016  df-rdg 8054  df-1o 8110  df-oadd 8114  df-er 8297  df-map 8416  df-en 8526  df-dom 8527  df-sdom 8528  df-fin 8529  df-sup 8929  df-inf 8930  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-div 11326  df-nn 11665  df-2 11727  df-3 11728  df-4 11729  df-5 11730  df-6 11731  df-7 11732  df-8 11733  df-9 11734  df-n0 11925  df-z 12011  df-dec 12128  df-uz 12273  df-rp 12421  df-fz 12930  df-fl 13201  df-mod 13277  df-seq 13409  df-exp 13470  df-cj 14496  df-re 14497  df-im 14498  df-sqrt 14632  df-abs 14633  df-dvds 15646  df-struct 16533  df-ndx 16534  df-slot 16535  df-base 16537  df-sets 16538  df-ress 16539  df-plusg 16626  df-mulr 16627  df-starv 16628  df-tset 16632  df-ple 16633  df-ds 16635  df-unif 16636  df-0g 16763  df-mgm 17908  df-sgrp 17957  df-mnd 17968  df-mhm 18012  df-grp 18162  df-minusg 18163  df-sbg 18164  df-mulg 18282  df-subg 18333  df-ghm 18413  df-od 18713  df-cmn 18965  df-mgp 19298  df-ur 19310  df-ring 19357  df-cring 19358  df-rnghom 19528  df-drng 19562  df-subrg 19591  df-cnfld 20157  df-zring 20229  df-zrh 20263  df-chr 20265 This theorem is referenced by:  qqhghm  31447  qqhrhm  31448  qqhnm  31449
 Copyright terms: Public domain W3C validator