Theorem drnginvrcld

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

	Ref	Expression
Hypotheses	invrcl.b	$$⊢B={\mathrm{Base}}_R$$
	invrcl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	invrcl.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	drnginvrcld	$$⊢\phi \to I\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		invrcl.b	$$⊢B={\mathrm{Base}}_R$$
2		invrcl.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		invrcl.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	drnginvrcl	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to I\left(X\right)\in B$$
8	4 5 6 7	syl3anc	$$⊢\phi \to I\left(X\right)\in B$$