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

Metamath Proof Explorer

Theorem dvr1

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

Ref Expression
Hypotheses dvr1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvr1.d ⊢ / = ( /r ‘ 𝑅 )
dvr1.o ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion dvr1 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 / 1 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 dvr1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvr1.d ⊢ / = ( /r ‘ 𝑅 )
3 dvr1.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 id ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝐵 )
5 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
6 5 3 1unit ⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Unit ‘ 𝑅 ) )
7 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
9 1 7 5 8 2 dvrval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 1 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝑋 / 1 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 1 ) ) )
10 4 6 9 syl2anr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 / 1 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 1 ) ) )
11 8 3 1rinv ⊢ ( 𝑅 ∈ Ring → ( ( invr ‘ 𝑅 ) ‘ 1 ) = 1 )
12 11 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( invr ‘ 𝑅 ) ‘ 1 ) = 1 )
13 12 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( ( invr ‘ 𝑅 ) ‘ 1 ) ) = ( 𝑋 ( .r ‘ 𝑅 ) 1 ) )
14 1 7 3 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( .r ‘ 𝑅 ) 1 ) = 𝑋 )
15 10 13 14 3eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 / 1 ) = 𝑋 )