Metamath Proof Explorer


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 } ) )