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

Metamath Proof Explorer

Theorem drngmgp

Description: A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011)

Ref Expression
Hypotheses drngmgp.b ⊢ B = Base R
drngmgp.z ⊢ 0 ˙ = 0 R
drngmgp.g ⊢ G = mulGrp R ↾ 𝑠 B ∖ 0 ˙
Assertion drngmgp ⊢ R ∈ DivRing → G ∈ Grp

Proof

Step Hyp Ref Expression
1 drngmgp.b ⊢ B = Base R
2 drngmgp.z ⊢ 0 ˙ = 0 R
3 drngmgp.g ⊢ G = mulGrp R ↾ 𝑠 B ∖ 0 ˙
4 1 2 3 isdrng2 ⊢ R ∈ DivRing ↔ R ∈ Ring ∧ G ∈ Grp
5 4 simprbi ⊢ R ∈ DivRing → G ∈ Grp