This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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