Theorem dvrid

Description: A cancellation law for division. ( divid analog.) (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	unitdvcl.o	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitdvcl.d	⊢ / = ( /r ‘ 𝑅 )
	dvrid.o	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	dvrid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		unitdvcl.o	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitdvcl.d	⊢ / = ( /r ‘ 𝑅 )
3		dvrid.o	⊢ 1 = ( 1r ‘ 𝑅 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	4 1	unitcl	⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
6	5	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
9	4 7 1 8 2	dvrval	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) )
10	6 9	sylancom	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) )
11	1 8 7 3	unitrinv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) = 1 )
12	10 11	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = 1 )