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

Metamath Proof Explorer

Theorem drngmulrcan

Description: Cancellation of a nonzero factor on the right for multiplication. ( mulcan2ad analog). (Contributed by SN, 14-Aug-2024) (Proof shortened by SN, 25-Jun-2025)

Ref Expression
Hypotheses drngmullcan.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngmullcan.0 ⊢ 0 = ( 0g ‘ 𝑅 )
drngmullcan.t ⊢ · = ( .r ‘ 𝑅 )
drngmullcan.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
drngmullcan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
drngmullcan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
drngmullcan.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
drngmullcan.1 ⊢ ( 𝜑 → 𝑍 ≠ 0 )
drngmulrcan.2 ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
Assertion drngmulrcan ( 𝜑 → 𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 drngmullcan.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 drngmullcan.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 drngmullcan.t ⊢ · = ( .r ‘ 𝑅 )
4 drngmullcan.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5 drngmullcan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 drngmullcan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 drngmullcan.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 drngmullcan.1 ⊢ ( 𝜑 → 𝑍 ≠ 0 )
9 drngmulrcan.2 ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) )
10 7 8 eldifsnd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ∖ { 0 } ) )
11 drngdomn ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )
12 4 11 syl ⊢ ( 𝜑 → 𝑅 ∈ Domn )
13 1 2 3 5 6 10 12 9 domnrcan ⊢ ( 𝜑 → 𝑋 = 𝑌 )