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

Metamath Proof Explorer

Theorem domnrrg

Description: In a domain, a nonzero element is a regular element. (Contributed by Mario Carneiro, 28-Mar-2015)

Ref Expression
Hypotheses isdomn2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdomn2.t ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
isdomn2.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion domnrrg ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 isdomn2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdomn2.t ⊢ 𝐸 = ( RLReg ‘ 𝑅 )
3 isdomn2.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 1 2 3 isdomn2 ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ) )
5 4 simprbi ⊢ ( 𝑅 ∈ Domn → ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 )
6 5 3ad2ant1 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 )
7 simp2 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐵 )
8 simp3 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
9 eldifsn ⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) )
10 7 8 9 sylanbrc ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
11 6 10 sseldd ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐸 )