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

Metamath Proof Explorer

Theorem dvreq1

Description: Equality in terms of ratio equal to ring unity. ( diveq1 analog.) (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dvreq1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvreq1.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dvreq1.d ⊢ / = ( /r ‘ 𝑅 )
dvreq1.t ⊢ 1 = ( 1r ‘ 𝑅 )
Assertion dvreq1 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) = 1 ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dvreq1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dvreq1.o ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dvreq1.d ⊢ / = ( /r ‘ 𝑅 )
4 dvreq1.t ⊢ 1 = ( 1r ‘ 𝑅 )
5 oveq1 ⊢ ( ( 𝑋 / 𝑌 ) = 1 → ( ( 𝑋 / 𝑌 ) ( .r ‘ 𝑅 ) 𝑌 ) = ( 1 ( .r ‘ 𝑅 ) 𝑌 ) )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 1 2 3 6 dvrcan1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) ( .r ‘ 𝑅 ) 𝑌 ) = 𝑋 )
8 1 2 unitcl ⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ 𝐵 )
9 1 6 4 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
10 8 9 sylan2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
11 10 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 1 ( .r ‘ 𝑅 ) 𝑌 ) = 𝑌 )
12 7 11 eqeq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( 𝑋 / 𝑌 ) ( .r ‘ 𝑅 ) 𝑌 ) = ( 1 ( .r ‘ 𝑅 ) 𝑌 ) ↔ 𝑋 = 𝑌 ) )
13 5 12 imbitrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) = 1 → 𝑋 = 𝑌 ) )
14 2 3 4 dvrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 / 𝑌 ) = 1 )
15 14 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑌 / 𝑌 ) = 1 )
16 oveq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 / 𝑌 ) = ( 𝑌 / 𝑌 ) )
17 16 eqeq1d ⊢ ( 𝑋 = 𝑌 → ( ( 𝑋 / 𝑌 ) = 1 ↔ ( 𝑌 / 𝑌 ) = 1 ) )
18 15 17 syl5ibrcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 = 𝑌 → ( 𝑋 / 𝑌 ) = 1 ) )
19 13 18 impbid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 / 𝑌 ) = 1 ↔ 𝑋 = 𝑌 ) )