# Metamath Proof Explorer

## Theorem zrhunitpreima

Description: The preimage by ZRHom of the unit of a division ring is ( ZZ \ { 0 } ) . (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Hypotheses zrhker.0 ${⊢}{B}={\mathrm{Base}}_{{R}}$
zrhker.1 ${⊢}{L}=\mathrm{ℤRHom}\left({R}\right)$
zrhker.2
Assertion 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\}$

### 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 eqid ${⊢}\mathrm{Unit}\left({R}\right)=\mathrm{Unit}\left({R}\right)$
5 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
6 1 4 5 isdrng ${⊢}{R}\in \mathrm{DivRing}↔\left({R}\in \mathrm{Ring}\wedge \mathrm{Unit}\left({R}\right)={B}\setminus \left\{{0}_{{R}}\right\}\right)$
7 6 simprbi ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{Unit}\left({R}\right)={B}\setminus \left\{{0}_{{R}}\right\}$
8 7 imaeq2d ${⊢}{R}\in \mathrm{DivRing}\to {{L}}^{-1}\left[\mathrm{Unit}\left({R}\right)\right]={{L}}^{-1}\left[{B}\setminus \left\{{0}_{{R}}\right\}\right]$
9 8 adantr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\to {{L}}^{-1}\left[\mathrm{Unit}\left({R}\right)\right]={{L}}^{-1}\left[{B}\setminus \left\{{0}_{{R}}\right\}\right]$
10 drngring ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{Ring}$
11 2 zrhrhm ${⊢}{R}\in \mathrm{Ring}\to {L}\in \left({ℤ}_{\mathrm{ring}}\mathrm{RingHom}{R}\right)$
12 zringbas ${⊢}ℤ={\mathrm{Base}}_{{ℤ}_{\mathrm{ring}}}$
13 12 1 rhmf ${⊢}{L}\in \left({ℤ}_{\mathrm{ring}}\mathrm{RingHom}{R}\right)\to {L}:ℤ⟶{B}$
14 ffun ${⊢}{L}:ℤ⟶{B}\to \mathrm{Fun}{L}$
15 11 13 14 3syl ${⊢}{R}\in \mathrm{Ring}\to \mathrm{Fun}{L}$
16 difpreima ${⊢}\mathrm{Fun}{L}\to {{L}}^{-1}\left[{B}\setminus \left\{{0}_{{R}}\right\}\right]={{L}}^{-1}\left[{B}\right]\setminus {{L}}^{-1}\left[\left\{{0}_{{R}}\right\}\right]$
17 10 15 16 3syl ${⊢}{R}\in \mathrm{DivRing}\to {{L}}^{-1}\left[{B}\setminus \left\{{0}_{{R}}\right\}\right]={{L}}^{-1}\left[{B}\right]\setminus {{L}}^{-1}\left[\left\{{0}_{{R}}\right\}\right]$
18 17 adantr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\to {{L}}^{-1}\left[{B}\setminus \left\{{0}_{{R}}\right\}\right]={{L}}^{-1}\left[{B}\right]\setminus {{L}}^{-1}\left[\left\{{0}_{{R}}\right\}\right]$
19 fimacnv ${⊢}{L}:ℤ⟶{B}\to {{L}}^{-1}\left[{B}\right]=ℤ$
20 10 11 13 19 4syl ${⊢}{R}\in \mathrm{DivRing}\to {{L}}^{-1}\left[{B}\right]=ℤ$
21 20 adantr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\to {{L}}^{-1}\left[{B}\right]=ℤ$
22 1 2 5 zrhker ${⊢}{R}\in \mathrm{Ring}\to \left(\mathrm{chr}\left({R}\right)=0↔{{L}}^{-1}\left[\left\{{0}_{{R}}\right\}\right]=\left\{0\right\}\right)$
23 22 biimpa ${⊢}\left({R}\in \mathrm{Ring}\wedge \mathrm{chr}\left({R}\right)=0\right)\to {{L}}^{-1}\left[\left\{{0}_{{R}}\right\}\right]=\left\{0\right\}$
24 10 23 sylan ${⊢}\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\to {{L}}^{-1}\left[\left\{{0}_{{R}}\right\}\right]=\left\{0\right\}$
25 21 24 difeq12d ${⊢}\left({R}\in \mathrm{DivRing}\wedge \mathrm{chr}\left({R}\right)=0\right)\to {{L}}^{-1}\left[{B}\right]\setminus {{L}}^{-1}\left[\left\{{0}_{{R}}\right\}\right]=ℤ\setminus \left\{0\right\}$
26 9 18 25 3eqtrd ${⊢}\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\}$