Theorem domnrrg

Description: In a domain, any nonzero element is a nonzero-divisor. (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 ) → 𝑋 ∈ 𝐸 )