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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drnginvrn0d.0	⊢ 0 = ( 0g ‘ 𝑅 )
	drnginvrn0d.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
	drnginvrn0d.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	drnginvrn0d.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	drnginvrn0d.1	⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion	drnginvrn0d	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		drnginvrn0d.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drnginvrn0d.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		drnginvrn0d.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
4		drnginvrn0d.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5		drnginvrn0d.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		drnginvrn0d.1	⊢ ( 𝜑 → 𝑋 ≠ 0 )
7	1 2 3	drnginvrn0	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐼 ‘ 𝑋 ) ≠ 0 )
8	4 5 6 7	syl3anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ≠ 0 )