Metamath Proof Explorer


Theorem drnginvrld

Description: Property of the multiplicative inverse in a division ring. ( recid2d analog). (Contributed by SN, 14-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 drnginvrld.b B = Base R
2 drnginvrld.0 0 ˙ = 0 R
3 drnginvrld.t · ˙ = R
4 drnginvrld.u 1 ˙ = 1 R
5 drnginvrld.i I = inv r R
6 drnginvrld.r φ R DivRing
7 drnginvrld.x φ X B
8 drnginvrld.1 φ X 0 ˙
9 1 2 3 4 5 drnginvrl R DivRing X B X 0 ˙ I X · ˙ X = 1 ˙
10 6 7 8 9 syl3anc φ I X · ˙ X = 1 ˙