Metamath Proof Explorer


Theorem drnginvrr

Description: Property of the multiplicative inverse in a division ring. ( recid analog). (Contributed by NM, 19-Apr-2014)

Ref Expression
Hypotheses drnginvrl.b B = Base R
drnginvrl.z 0 ˙ = 0 R
drnginvrl.t · ˙ = R
drnginvrl.u 1 ˙ = 1 R
drnginvrl.i I = inv r R
Assertion drnginvrr R DivRing X B X 0 ˙ X · ˙ I X = 1 ˙

Proof

Step Hyp Ref Expression
1 drnginvrl.b B = Base R
2 drnginvrl.z 0 ˙ = 0 R
3 drnginvrl.t · ˙ = R
4 drnginvrl.u 1 ˙ = 1 R
5 drnginvrl.i I = inv r R
6 eqid Unit R = Unit R
7 1 6 2 drngunit R DivRing X Unit R X B X 0 ˙
8 drngring R DivRing R Ring
9 6 5 3 4 unitrinv R Ring X Unit R X · ˙ I X = 1 ˙
10 9 ex R Ring X Unit R X · ˙ I X = 1 ˙
11 8 10 syl R DivRing X Unit R X · ˙ I X = 1 ˙
12 7 11 sylbird R DivRing X B X 0 ˙ X · ˙ I X = 1 ˙
13 12 3impib R DivRing X B X 0 ˙ X · ˙ I X = 1 ˙