Metamath Proof Explorer


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 ∧ 𝑋𝐵𝑌𝑈 ) → ( 𝑋 / 𝑌 ) ∈ 𝐵 )