Theorem drngmcl

Description: The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011)

	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		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
5	1 3 4	drngmgp	⊢ ( 𝑅 ∈ DivRing → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )
6		difss	⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
7		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
8	7 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
9	4 8	ressbas2	⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
10	6 9	ax-mp	⊢ ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
11	1	fvexi	⊢ 𝐵 ∈ V
12		difexg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V )
13	7 2	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
14	4 13	ressplusg	⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
15	11 12 14	mp2b	⊢ · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) )
16	10 15	grpcl	⊢ ( ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐵 ∖ { 0 } ) )
17	5 16	syl3an1	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑌 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑋 · 𝑌 ) ∈ ( 𝐵 ∖ { 0 } ) )