Theorem drngmcl

Description: The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010) (Revised by NM, 7-Sep-2011) (Proof shortened by SN, 25-Jun-2025)

	Ref	Expression
Hypotheses	drngmcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngmcl.t	⊢ · = ( .r ‘ 𝑅 )
	drngmcl.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	drngmcl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐵 ∖ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		drngmcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngmcl.t	⊢ · = ( .r ‘ 𝑅 )
3		drngmcl.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
5		eldifi	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) → 𝑋 ∈ 𝐵 )
6		eldifi	⊢ ( 𝑌 ∈ ( 𝐵 ∖ { 0 } ) → 𝑌 ∈ 𝐵 )
7	1 2	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
8	4 5 6 7	syl3an	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
9		drngdomn	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )
10		eldifsn	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) )
11	10	biimpi	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) )
12		eldifsn	⊢ ( 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) )
13	12	biimpi	⊢ ( 𝑌 ∈ ( 𝐵 ∖ { 0 } ) → ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) )
14	1 2 3	domnmuln0	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 )
15	9 11 13 14	syl3an	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ≠ 0 )
16	8 15	eldifsnd	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐵 ∖ { 0 } ) )