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

Metamath Proof Explorer

Definition df-nzr

Description: A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Assertion df-nzr NzRing = { 𝑟 ∈ Ring ∣ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnzr ⊢ NzRing
1 vr ⊢ 𝑟
2 crg ⊢ Ring
3 cur ⊢ 1r
4 1 cv ⊢ 𝑟
5 4 3 cfv ⊢ ( 1r ‘ 𝑟 )
6 c0g ⊢ 0g
7 4 6 cfv ⊢ ( 0g ‘ 𝑟 )
8 5 7 wne ⊢ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 )
9 8 1 2 crab ⊢ { 𝑟 ∈ Ring ∣ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 ) }
10 0 9 wceq ⊢ NzRing = { 𝑟 ∈ Ring ∣ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 ) }