Theorem dvrcl

Description: Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dvrcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvrcl.o	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		dvrcl.d	⊢ / = ( /r ‘ 𝑅 )
4		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5		eqid	⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
6	1 4 2 5 3	dvrval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
7	6	3adant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) )
8	2 5 1	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
9	8	3adant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 )
10	1 4	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ∈ 𝐵 )
11	9 10	syld3an3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑌 ) ) ∈ 𝐵 )
12	7 11	eqeltrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 / 𝑌 ) ∈ 𝐵 )