# 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 𝐵 = ( Base ‘ 𝑅 )
zrhker.1 𝐿 = ( ℤRHom ‘ 𝑅 )
zrhker.2 0 = ( 0g𝑅 )
Assertion zrhunitpreima ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( ℤ ∖ { 0 } ) )

### Proof

Step Hyp Ref Expression
1 zrhker.0 𝐵 = ( Base ‘ 𝑅 )
2 zrhker.1 𝐿 = ( ℤRHom ‘ 𝑅 )
3 zrhker.2 0 = ( 0g𝑅 )
4 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
5 eqid ( 0g𝑅 ) = ( 0g𝑅 )
6 1 4 5 isdrng ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { ( 0g𝑅 ) } ) ) )
7 6 simprbi ( 𝑅 ∈ DivRing → ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { ( 0g𝑅 ) } ) )
8 7 imaeq2d ( 𝑅 ∈ DivRing → ( 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( 𝐿 “ ( 𝐵 ∖ { ( 0g𝑅 ) } ) ) )
9 8 adantr ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( 𝐿 “ ( 𝐵 ∖ { ( 0g𝑅 ) } ) ) )
10 drngring ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
11 2 zrhrhm ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
12 zringbas ℤ = ( Base ‘ ℤring )
13 12 1 rhmf ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 : ℤ ⟶ 𝐵 )
14 ffun ( 𝐿 : ℤ ⟶ 𝐵 → Fun 𝐿 )
15 11 13 14 3syl ( 𝑅 ∈ Ring → Fun 𝐿 )
16 difpreima ( Fun 𝐿 → ( 𝐿 “ ( 𝐵 ∖ { ( 0g𝑅 ) } ) ) = ( ( 𝐿𝐵 ) ∖ ( 𝐿 “ { ( 0g𝑅 ) } ) ) )
17 10 15 16 3syl ( 𝑅 ∈ DivRing → ( 𝐿 “ ( 𝐵 ∖ { ( 0g𝑅 ) } ) ) = ( ( 𝐿𝐵 ) ∖ ( 𝐿 “ { ( 0g𝑅 ) } ) ) )
18 17 adantr ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝐿 “ ( 𝐵 ∖ { ( 0g𝑅 ) } ) ) = ( ( 𝐿𝐵 ) ∖ ( 𝐿 “ { ( 0g𝑅 ) } ) ) )
19 fimacnv ( 𝐿 : ℤ ⟶ 𝐵 → ( 𝐿𝐵 ) = ℤ )
20 10 11 13 19 4syl ( 𝑅 ∈ DivRing → ( 𝐿𝐵 ) = ℤ )
21 20 adantr ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝐿𝐵 ) = ℤ )
22 1 2 5 zrhker ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ ( 𝐿 “ { ( 0g𝑅 ) } ) = { 0 } ) )
23 22 biimpa ( ( 𝑅 ∈ Ring ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝐿 “ { ( 0g𝑅 ) } ) = { 0 } )
24 10 23 sylan ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝐿 “ { ( 0g𝑅 ) } ) = { 0 } )
25 21 24 difeq12d ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( 𝐿𝐵 ) ∖ ( 𝐿 “ { ( 0g𝑅 ) } ) ) = ( ℤ ∖ { 0 } ) )
26 9 18 25 3eqtrd ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( ℤ ∖ { 0 } ) )