Metamath Proof Explorer


Theorem drnginvrl

Description: Property of the multiplicative inverse in a division ring. ( recid2 analog). (Contributed by NM, 19-Apr-2014)

Ref Expression
Hypotheses drnginvrl.b 𝐵 = ( Base ‘ 𝑅 )
drnginvrl.z 0 = ( 0g𝑅 )
drnginvrl.t · = ( .r𝑅 )
drnginvrl.u 1 = ( 1r𝑅 )
drnginvrl.i 𝐼 = ( invr𝑅 )
Assertion drnginvrl ( ( 𝑅 ∈ DivRing ∧ 𝑋𝐵𝑋0 ) → ( ( 𝐼𝑋 ) · 𝑋 ) = 1 )

Proof

Step Hyp Ref Expression
1 drnginvrl.b 𝐵 = ( Base ‘ 𝑅 )
2 drnginvrl.z 0 = ( 0g𝑅 )
3 drnginvrl.t · = ( .r𝑅 )
4 drnginvrl.u 1 = ( 1r𝑅 )
5 drnginvrl.i 𝐼 = ( invr𝑅 )
6 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
7 1 6 2 drngunit ( 𝑅 ∈ DivRing → ( 𝑋 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑋𝐵𝑋0 ) ) )
8 drngring ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
9 6 5 3 4 unitlinv ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐼𝑋 ) · 𝑋 ) = 1 )
10 9 ex ( 𝑅 ∈ Ring → ( 𝑋 ∈ ( Unit ‘ 𝑅 ) → ( ( 𝐼𝑋 ) · 𝑋 ) = 1 ) )
11 8 10 syl ( 𝑅 ∈ DivRing → ( 𝑋 ∈ ( Unit ‘ 𝑅 ) → ( ( 𝐼𝑋 ) · 𝑋 ) = 1 ) )
12 7 11 sylbird ( 𝑅 ∈ DivRing → ( ( 𝑋𝐵𝑋0 ) → ( ( 𝐼𝑋 ) · 𝑋 ) = 1 ) )
13 12 3impib ( ( 𝑅 ∈ DivRing ∧ 𝑋𝐵𝑋0 ) → ( ( 𝐼𝑋 ) · 𝑋 ) = 1 )