This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 / 𝑋 ) )