Theorem drnginvrn0d

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

	Ref	Expression
Hypotheses	drnginvrcld.b	$$⊢B={\mathrm{Base}}_R$$
	drnginvrcld.0	$$⊢\underset{\dot{}}{0}=0_R$$
	drnginvrcld.i	$$⊢I={inv}_r\left(R\right)$$
	drnginvrcld.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
	drnginvrcld.x	$$⊢\phi \to X\in B$$
	drnginvrcld.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		drnginvrcld.b	$$⊢B={\mathrm{Base}}_R$$
2		drnginvrcld.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		drnginvrcld.i	$$⊢I={inv}_r\left(R\right)$$
4		drnginvrcld.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
5		drnginvrcld.x	$$⊢\phi \to X\in B$$
6		drnginvrcld.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}$$