Metamath Proof Explorer


Theorem drngid

Description: A division ring's unit is the identity element of its multiplicative group. (Contributed by NM, 7-Sep-2011)

Ref Expression
Hypotheses drngid.b B = Base R
drngid.z 0 ˙ = 0 R
drngid.u 1 ˙ = 1 R
drngid.g G = mulGrp R 𝑠 B 0 ˙
Assertion drngid R DivRing 1 ˙ = 0 G

Proof

Step Hyp Ref Expression
1 drngid.b B = Base R
2 drngid.z 0 ˙ = 0 R
3 drngid.u 1 ˙ = 1 R
4 drngid.g G = mulGrp R 𝑠 B 0 ˙
5 drngring R DivRing R Ring
6 eqid Unit R = Unit R
7 eqid mulGrp R 𝑠 Unit R = mulGrp R 𝑠 Unit R
8 6 7 3 unitgrpid R Ring 1 ˙ = 0 mulGrp R 𝑠 Unit R
9 5 8 syl R DivRing 1 ˙ = 0 mulGrp R 𝑠 Unit R
10 1 6 2 isdrng R DivRing R Ring Unit R = B 0 ˙
11 10 simprbi R DivRing Unit R = B 0 ˙
12 11 oveq2d R DivRing mulGrp R 𝑠 Unit R = mulGrp R 𝑠 B 0 ˙
13 12 4 eqtr4di R DivRing mulGrp R 𝑠 Unit R = G
14 13 fveq2d R DivRing 0 mulGrp R 𝑠 Unit R = 0 G
15 9 14 eqtrd R DivRing 1 ˙ = 0 G