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

Metamath Proof Explorer

Theorem isdomn6

Description: A ring is a domain iff the regular elements are the nonzero elements. Compare isdomn2 , domnrrg . (Contributed by Thierry Arnoux, 6-May-2025)

Ref Expression
Hypotheses isdomn6.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdomn6.t ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
isdomn6.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion isdomn6 ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )

Proof

Step Hyp Ref Expression
1 isdomn6.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdomn6.t ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
3 isdomn6.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 1 2 3 isdomn2 ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ) )
5 2 1 rrgss ⊢ 𝐸 ⊆ 𝐵
6 5 a1i ⊢ ( 𝑅 ∈ NzRing → 𝐸 ⊆ 𝐵 )
7 2 3 rrgnz ⊢ ( 𝑅 ∈ NzRing → ¬ 0 ∈ 𝐸 )
8 ssdifsn ⊢ ( 𝐸 ⊆ ( 𝐵 ∖ { 0 } ) ↔ ( 𝐸 ⊆ 𝐵 ∧ ¬ 0 ∈ 𝐸 ) )
9 6 7 8 sylanbrc ⊢ ( 𝑅 ∈ NzRing → 𝐸 ⊆ ( 𝐵 ∖ { 0 } ) )
10 sssseq ⊢ ( 𝐸 ⊆ ( 𝐵 ∖ { 0 } ) → ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ↔ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )
11 9 10 syl ⊢ ( 𝑅 ∈ NzRing → ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ↔ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )
12 11 pm5.32i ⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ) ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )
13 4 12 bitri ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )