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 = ( Base ` R )
	drnginvrn0d.0	|- .0. = ( 0g ` R )
	drnginvrn0d.i	|- I = ( invr ` R )
	drnginvrn0d.r	|- ( ph -> R e. DivRing )
	drnginvrn0d.x	|- ( ph -> X e. B )
	drnginvrn0d.1	|- ( ph -> X =/= .0. )
Assertion	drnginvrn0d	|- ( ph -> ( I ` X ) =/= .0. )

Proof

Step	Hyp	Ref	Expression
1		drnginvrn0d.b	|- B = ( Base ` R )
2		drnginvrn0d.0	|- .0. = ( 0g ` R )
3		drnginvrn0d.i	|- I = ( invr ` R )
4		drnginvrn0d.r	|- ( ph -> R e. DivRing )
5		drnginvrn0d.x	|- ( ph -> X e. B )
6		drnginvrn0d.1	|- ( ph -> X =/= .0. )
7	1 2 3	drnginvrn0	|- ( ( R e. DivRing /\ X e. B /\ X =/= .0. ) -> ( I ` X ) =/= .0. )
8	4 5 6 7	syl3anc	|- ( ph -> ( I ` X ) =/= .0. )