Metamath Proof Explorer

Theorem elzrhunit

Description: Condition for the image by ZRHom to be a unit. (Contributed by Thierry Arnoux, 30-Oct-2017)

Ref Expression
Hypotheses zrhker.0 ${⊢}{B}={\mathrm{Base}}_{{R}}$
zrhker.1 ${⊢}{L}=\mathrm{ℤRHom}\left({R}\right)$
zrhker.2
Assertion elzrhunit ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {L}\left({M}\right)\in \mathrm{Unit}\left({R}\right)$

Proof

Step Hyp Ref Expression
1 zrhker.0 ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 zrhker.1 ${⊢}{L}=\mathrm{ℤRHom}\left({R}\right)$
3 zrhker.2
4 simpll ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {R}\in \mathrm{DivRing}$
5 drngring ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{Ring}$
6 2 zrhrhm ${⊢}{R}\in \mathrm{Ring}\to {L}\in \left({ℤ}_{\mathrm{ring}}\mathrm{RingHom}{R}\right)$
7 zringbas ${⊢}ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
8 7 1 rhmf ${⊢}{L}\in \left({ℤ}_{\mathrm{ring}}\mathrm{RingHom}{R}\right)\to {L}:ℤ⟶{B}$
9 ffn ${⊢}{L}:ℤ⟶{B}\to {L}Fnℤ$
10 6 8 9 3syl ${⊢}{R}\in \mathrm{Ring}\to {L}Fnℤ$
11 4 5 10 3syl ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {L}Fnℤ$
12 simprl ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {M}\in ℤ$
13 elsng ${⊢}{M}\in ℤ\to \left({M}\in \left\{0\right\}↔{M}=0\right)$
14 13 necon3bbid ${⊢}{M}\in ℤ\to \left(¬{M}\in \left\{0\right\}↔{M}\ne 0\right)$
15 14 biimpar ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\right)\to ¬{M}\in \left\{0\right\}$
16 15 adantl ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to ¬{M}\in \left\{0\right\}$
17 12 16 eldifd ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {M}\in \left(ℤ\setminus \left\{0\right\}\right)$
18 1 2 3 zrhunitpreima ${⊢}\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\to {{L}}^{-1}\left[\mathrm{Unit}\left({R}\right)\right]=ℤ\setminus \left\{0\right\}$
19 18 adantr ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {{L}}^{-1}\left[\mathrm{Unit}\left({R}\right)\right]=ℤ\setminus \left\{0\right\}$
20 17 19 eleqtrrd ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {M}\in {{L}}^{-1}\left[\mathrm{Unit}\left({R}\right)\right]$
21 elpreima ${⊢}{L}Fnℤ\to \left({M}\in {{L}}^{-1}\left[\mathrm{Unit}\left({R}\right)\right]↔\left({M}\in ℤ\wedge {L}\left({M}\right)\in \mathrm{Unit}\left({R}\right)\right)\right)$
22 21 simplbda ${⊢}\left({L}Fnℤ\wedge {M}\in {{L}}^{-1}\left[\mathrm{Unit}\left({R}\right)\right]\right)\to {L}\left({M}\right)\in \mathrm{Unit}\left({R}\right)$
23 11 20 22 syl2anc ${⊢}\left(\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\wedge \left({M}\in ℤ\wedge {M}\ne 0\right)\right)\to {L}\left({M}\right)\in \mathrm{Unit}\left({R}\right)$