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