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={\mathrm{Base}}_R$$
	drnginvrld.0	$$⊢\underset{\dot{}}{0}=0_R$$
	drnginvrld.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drnginvrld.u	$$⊢\underset{\dot{}}{1}=1_R$$
	drnginvrld.i	$$⊢I={inv}_r\left(R\right)$$
	drnginvrld.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
	drnginvrld.x	$$⊢\phi \to X\in B$$
	drnginvrld.1	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
Assertion	drnginvrld	$$⊢\phi \to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		drnginvrld.b	$$⊢B={\mathrm{Base}}_R$$
2		drnginvrld.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		drnginvrld.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		drnginvrld.u	$$⊢\underset{\dot{}}{1}=1_R$$
5		drnginvrld.i	$$⊢I={inv}_r\left(R\right)$$
6		drnginvrld.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
7		drnginvrld.x	$$⊢\phi \to X\in B$$
8		drnginvrld.1	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
9	1 2 3 4 5	drnginvrl	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
10	6 7 8 9	syl3anc	$$⊢\phi \to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$