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

Metamath Proof Explorer

Theorem dvrid

Description: A ring element divided by itself is the ring unity. ( divid analog.) (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypotheses unitdvcl.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
unitdvcl.d ⊢ / = ( /r ‘ 𝑅 )
dvrid.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion dvrid ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = 1 )

Proof

Step Hyp Ref Expression
1 unitdvcl.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 unitdvcl.d ⊢ / = ( /r ‘ 𝑅 )
3 dvrid.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 4 1 unitcl ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
6 5 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
7 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
9 4 7 1 8 2 dvrval ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) )
10 6 9 sylancom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) )
11 1 8 7 3 unitrinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 𝑋 ) ) = 1 )
12 10 11 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 / 𝑋 ) = 1 )