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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	zrhker.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrhker.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	elzrhunit	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( 𝐿 ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		zrhker.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
3		zrhker.2	⊢ 0 = ( 0g ‘ 𝑅 )
4		simpll	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → 𝑅 ∈ DivRing )
5		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
6	2	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
7		zringbas	⊢ ℤ = ( Base ‘ ℤring )
8	7 1	rhmf	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 : ℤ ⟶ 𝐵 )
9		ffn	⊢ ( 𝐿 : ℤ ⟶ 𝐵 → 𝐿 Fn ℤ )
10	6 8 9	3syl	⊢ ( 𝑅 ∈ Ring → 𝐿 Fn ℤ )
11	4 5 10	3syl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → 𝐿 Fn ℤ )
12		simprl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → 𝑀 ∈ ℤ )
13		elsng	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ { 0 } ↔ 𝑀 = 0 ) )
14	13	necon3bbid	⊢ ( 𝑀 ∈ ℤ → ( ¬ 𝑀 ∈ { 0 } ↔ 𝑀 ≠ 0 ) )
15	14	biimpar	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) → ¬ 𝑀 ∈ { 0 } )
16	15	adantl	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ¬ 𝑀 ∈ { 0 } )
17	12 16	eldifd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → 𝑀 ∈ ( ℤ ∖ { 0 } ) )
18	1 2 3	zrhunitpreima	⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( ℤ ∖ { 0 } ) )
19	18	adantr	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) = ( ℤ ∖ { 0 } ) )
20	17 19	eleqtrrd	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → 𝑀 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) )
21		elpreima	⊢ ( 𝐿 Fn ℤ → ( 𝑀 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝐿 ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ) ) )
22	21	simplbda	⊢ ( ( 𝐿 Fn ℤ ∧ 𝑀 ∈ ( ◡ 𝐿 “ ( Unit ‘ 𝑅 ) ) ) → ( 𝐿 ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) )
23	11 20 22	syl2anc	⊢ ( ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( 𝐿 ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) )