Metamath Proof Explorer


Theorem drnginvrn0d

Description: A multiplicative inverse in a division ring is nonzero. ( recne0d analog). (Contributed by SN, 14-Aug-2024)

Ref Expression
Hypotheses drnginvrn0d.b B = Base R
drnginvrn0d.0 0 ˙ = 0 R
drnginvrn0d.i I = inv r R
drnginvrn0d.r φ R DivRing
drnginvrn0d.x φ X B
drnginvrn0d.1 φ X 0 ˙
Assertion drnginvrn0d φ I X 0 ˙

Proof

Step Hyp Ref Expression
1 drnginvrn0d.b B = Base R
2 drnginvrn0d.0 0 ˙ = 0 R
3 drnginvrn0d.i I = inv r R
4 drnginvrn0d.r φ R DivRing
5 drnginvrn0d.x φ X B
6 drnginvrn0d.1 φ X 0 ˙
7 1 2 3 drnginvrn0 R DivRing X B X 0 ˙ I X 0 ˙
8 4 5 6 7 syl3anc φ I X 0 ˙