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

Proof

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