# Metamath Proof Explorer

## Theorem dvrcl

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

Ref Expression
Hypotheses dvrcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
dvrcl.o ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
dvrcl.d
Assertion dvrcl

### Proof

Step Hyp Ref Expression
1 dvrcl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 dvrcl.o ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
3 dvrcl.d
4 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
5 eqid ${⊢}{inv}_{r}\left({R}\right)={inv}_{r}\left({R}\right)$
6 1 4 2 5 3 dvrval
7 6 3adant1
8 2 5 1 ringinvcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {Y}\in {U}\right)\to {inv}_{r}\left({R}\right)\left({Y}\right)\in {B}$
9 8 3adant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {B}\wedge {Y}\in {U}\right)\to {inv}_{r}\left({R}\right)\left({Y}\right)\in {B}$
10 1 4 ringcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {B}\wedge {inv}_{r}\left({R}\right)\left({Y}\right)\in {B}\right)\to {X}{\cdot }_{{R}}{inv}_{r}\left({R}\right)\left({Y}\right)\in {B}$
11 9 10 syld3an3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {B}\wedge {Y}\in {U}\right)\to {X}{\cdot }_{{R}}{inv}_{r}\left({R}\right)\left({Y}\right)\in {B}$
12 7 11 eqeltrd