Metamath Proof Explorer


Theorem ringinvdv

Description: Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014)

Ref Expression
Hypotheses ringinvdv.b 𝐵 = ( Base ‘ 𝑅 )
ringinvdv.u 𝑈 = ( Unit ‘ 𝑅 )
ringinvdv.d / = ( /r𝑅 )
ringinvdv.o 1 = ( 1r𝑅 )
ringinvdv.i 𝐼 = ( invr𝑅 )
Assertion ringinvdv ( ( 𝑅 ∈ Ring ∧ 𝑋𝑈 ) → ( 𝐼𝑋 ) = ( 1 / 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ringinvdv.b 𝐵 = ( Base ‘ 𝑅 )
2 ringinvdv.u 𝑈 = ( Unit ‘ 𝑅 )
3 ringinvdv.d / = ( /r𝑅 )
4 ringinvdv.o 1 = ( 1r𝑅 )
5 ringinvdv.i 𝐼 = ( invr𝑅 )
6 1 4 ringidcl ( 𝑅 ∈ Ring → 1𝐵 )
7 eqid ( .r𝑅 ) = ( .r𝑅 )
8 1 7 2 5 3 dvrval ( ( 1𝐵𝑋𝑈 ) → ( 1 / 𝑋 ) = ( 1 ( .r𝑅 ) ( 𝐼𝑋 ) ) )
9 6 8 sylan ( ( 𝑅 ∈ Ring ∧ 𝑋𝑈 ) → ( 1 / 𝑋 ) = ( 1 ( .r𝑅 ) ( 𝐼𝑋 ) ) )
10 2 5 1 ringinvcl ( ( 𝑅 ∈ Ring ∧ 𝑋𝑈 ) → ( 𝐼𝑋 ) ∈ 𝐵 )
11 1 7 4 ringlidm ( ( 𝑅 ∈ Ring ∧ ( 𝐼𝑋 ) ∈ 𝐵 ) → ( 1 ( .r𝑅 ) ( 𝐼𝑋 ) ) = ( 𝐼𝑋 ) )
12 10 11 syldan ( ( 𝑅 ∈ Ring ∧ 𝑋𝑈 ) → ( 1 ( .r𝑅 ) ( 𝐼𝑋 ) ) = ( 𝐼𝑋 ) )
13 9 12 eqtr2d ( ( 𝑅 ∈ Ring ∧ 𝑋𝑈 ) → ( 𝐼𝑋 ) = ( 1 / 𝑋 ) )