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

Metamath Proof Explorer

Theorem drngmclOLD

Description: Obsolete version of drngmcl as of 25-Jun-2025. The product of two nonzero elements of a division ring is nonzero. (Contributed by NM, 7-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses drngmcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngmcl.t ⊢ · = ( .r ‘ 𝑅 )
drngmcl.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion drngmclOLD ( ( 𝑅 ∈ 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 } ) )