Metamath Proof Explorer


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

Proof

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