Description: Right-cancellation law for domains. (Contributed by SN, 21-Jun-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | domnrcan.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| domnrcan.0 | ⊢ 0 = ( 0g ‘ 𝑅 ) | ||
| domnrcan.m | ⊢ · = ( .r ‘ 𝑅 ) | ||
| domnrcan.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | ||
| domnrcan.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) | ||
| domnrcan.z | ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ∖ { 0 } ) ) | ||
| domnrcan.r | ⊢ ( 𝜑 → 𝑅 ∈ Domn ) | ||
| domnrcan.1 | ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) | ||
| Assertion | domnrcan | ⊢ ( 𝜑 → 𝑋 = 𝑌 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | domnrcan.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| 2 | domnrcan.0 | ⊢ 0 = ( 0g ‘ 𝑅 ) | |
| 3 | domnrcan.m | ⊢ · = ( .r ‘ 𝑅 ) | |
| 4 | domnrcan.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | |
| 5 | domnrcan.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) | |
| 6 | domnrcan.z | ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ∖ { 0 } ) ) | |
| 7 | domnrcan.r | ⊢ ( 𝜑 → 𝑅 ∈ Domn ) | |
| 8 | domnrcan.1 | ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ) | |
| 9 | 1 2 3 4 5 6 7 | domnrcanb | ⊢ ( 𝜑 → ( ( 𝑋 · 𝑍 ) = ( 𝑌 · 𝑍 ) ↔ 𝑋 = 𝑌 ) ) |
| 10 | 8 9 | mpbid | ⊢ ( 𝜑 → 𝑋 = 𝑌 ) |