# Metamath Proof Explorer

## Theorem dmncan2

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Hypotheses dmncan.1 ${⊢}{G}={1}^{st}\left({R}\right)$
dmncan.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
dmncan.3 ${⊢}{X}=\mathrm{ran}{G}$
dmncan.4 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
Assertion dmncan2 ${⊢}\left(\left({R}\in \mathrm{Dmn}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {C}\ne {Z}\right)\to \left({A}{H}{C}={B}{H}{C}\to {A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 dmncan.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 dmncan.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 dmncan.3 ${⊢}{X}=\mathrm{ran}{G}$
4 dmncan.4 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
5 dmncrng ${⊢}{R}\in \mathrm{Dmn}\to {R}\in \mathrm{CRingOps}$
6 1 2 3 crngocom ${⊢}\left({R}\in \mathrm{CRingOps}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{H}{C}={C}{H}{A}$
7 6 3adant3r2 ${⊢}\left({R}\in \mathrm{CRingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{H}{C}={C}{H}{A}$
8 1 2 3 crngocom ${⊢}\left({R}\in \mathrm{CRingOps}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to {B}{H}{C}={C}{H}{B}$
9 8 3adant3r1 ${⊢}\left({R}\in \mathrm{CRingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{H}{C}={C}{H}{B}$
10 7 9 eqeq12d ${⊢}\left({R}\in \mathrm{CRingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{C}={B}{H}{C}↔{C}{H}{A}={C}{H}{B}\right)$
11 5 10 sylan ${⊢}\left({R}\in \mathrm{Dmn}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{H}{C}={B}{H}{C}↔{C}{H}{A}={C}{H}{B}\right)$
12 11 adantr ${⊢}\left(\left({R}\in \mathrm{Dmn}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {C}\ne {Z}\right)\to \left({A}{H}{C}={B}{H}{C}↔{C}{H}{A}={C}{H}{B}\right)$
13 3anrot ${⊢}\left({C}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)↔\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)$
14 13 biimpri ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \left({C}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)$
15 1 2 3 4 dmncan1 ${⊢}\left(\left({R}\in \mathrm{Dmn}\wedge \left({C}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)\right)\wedge {C}\ne {Z}\right)\to \left({C}{H}{A}={C}{H}{B}\to {A}={B}\right)$
16 14 15 sylanl2 ${⊢}\left(\left({R}\in \mathrm{Dmn}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {C}\ne {Z}\right)\to \left({C}{H}{A}={C}{H}{B}\to {A}={B}\right)$
17 12 16 sylbid ${⊢}\left(\left({R}\in \mathrm{Dmn}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {C}\ne {Z}\right)\to \left({A}{H}{C}={B}{H}{C}\to {A}={B}\right)$