Theorem unitdvcl

Description: The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		unitdvcl.o	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitdvcl.d	⊢ / = ( /r ‘ 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3 1	unitcl	⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
5		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
7	3 5 1 6 2	dvrval	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
8	4 7	sylan	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
9	8	3adant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
10	1 6	unitinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝑈 )
11	10	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝑈 )
12	1 5	unitmulcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ∈ 𝑈 )
13	11 12	syld3an3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ∈ 𝑈 )
14	9 13	eqeltrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) ∈ 𝑈 )