This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chrnzr

Description: Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion chrnzr ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ( chr ‘ 𝑅 ) ≠ 1 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
2 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
3 1 2 isnzr ⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
4 3 baib ⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
5 1z ⊢ 1 ∈ ℤ
6 eqid ⊢ ( chr ‘ 𝑅 ) = ( chr ‘ 𝑅 )
7 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
8 6 7 2 chrdvds ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ∈ ℤ ) → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 0g ‘ 𝑅 ) ) )
9 5 8 mpan2 ⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 0g ‘ 𝑅 ) ) )
10 6 chrcl ⊢ ( 𝑅 ∈ Ring → ( chr ‘ 𝑅 ) ∈ ℕ0 )
11 dvds1 ⊢ ( ( chr ‘ 𝑅 ) ∈ ℕ0 → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( chr ‘ 𝑅 ) = 1 ) )
12 10 11 syl ⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) ∥ 1 ↔ ( chr ‘ 𝑅 ) = 1 ) )
13 7 1 zrh1 ⊢ ( 𝑅 ∈ Ring → ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
14 13 eqeq1d ⊢ ( 𝑅 ∈ Ring → ( ( ( ℤRHom ‘ 𝑅 ) ‘ 1 ) = ( 0g ‘ 𝑅 ) ↔ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) )
15 9 12 14 3bitr3d ⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 1 ↔ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) ) )
16 15 necon3bid ⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) ≠ 1 ↔ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
17 4 16 bitr4d ⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ( chr ‘ 𝑅 ) ≠ 1 ) )