Metamath Proof Explorer


Theorem isdrng

Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses isdrng.b B = Base R
isdrng.u U = Unit R
isdrng.z 0 ˙ = 0 R
Assertion isdrng R DivRing R Ring U = B 0 ˙

Proof

Step Hyp Ref Expression
1 isdrng.b B = Base R
2 isdrng.u U = Unit R
3 isdrng.z 0 ˙ = 0 R
4 fveq2 r = R Unit r = Unit R
5 4 2 syl6eqr r = R Unit r = U
6 fveq2 r = R Base r = Base R
7 6 1 syl6eqr r = R Base r = B
8 fveq2 r = R 0 r = 0 R
9 8 3 syl6eqr r = R 0 r = 0 ˙
10 9 sneqd r = R 0 r = 0 ˙
11 7 10 difeq12d r = R Base r 0 r = B 0 ˙
12 5 11 eqeq12d r = R Unit r = Base r 0 r U = B 0 ˙
13 df-drng DivRing = r Ring | Unit r = Base r 0 r
14 12 13 elrab2 R DivRing R Ring U = B 0 ˙