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

Metamath Proof Explorer

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