Metamath Proof Explorer

Theorem dmncan2

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

Ref Expression
Hypotheses dmncan.1 ⊢G=1st⁡R
dmncan.2 ⊢H=2nd⁡R
dmncan.3 ⊢X=ran⁡G
dmncan.4 ⊢Z=GId⁡G
Assertion dmncan2 ⊢R∈Dmn∧A∈X∧B∈X∧C∈X∧C≠Z→AHC=BHC→A=B

Proof

Step Hyp Ref Expression
1 dmncan.1 ⊢G=1st⁡R
2 dmncan.2 ⊢H=2nd⁡R
3 dmncan.3 ⊢X=ran⁡G
4 dmncan.4 ⊢Z=GId⁡G
5 dmncrng ⊢R∈Dmn→R∈CRingOps
6 1 2 3 crngocom ⊢R∈CRingOps∧A∈X∧C∈X→AHC=CHA
7 6 3adant3r2 ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X→AHC=CHA
8 1 2 3 crngocom ⊢R∈CRingOps∧B∈X∧C∈X→BHC=CHB
9 8 3adant3r1 ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X→BHC=CHB
10 7 9 eqeq12d ⊢R∈CRingOps∧A∈X∧B∈X∧C∈X→AHC=BHC↔CHA=CHB
11 5 10 sylan ⊢R∈Dmn∧A∈X∧B∈X∧C∈X→AHC=BHC↔CHA=CHB
12 11 adantr ⊢R∈Dmn∧A∈X∧B∈X∧C∈X∧C≠Z→AHC=BHC↔CHA=CHB
13 3anrot ⊢C∈X∧A∈X∧B∈X↔A∈X∧B∈X∧C∈X
14 13 biimpri ⊢A∈X∧B∈X∧C∈X→C∈X∧A∈X∧B∈X
15 1 2 3 4 dmncan1 ⊢R∈Dmn∧C∈X∧A∈X∧B∈X∧C≠Z→CHA=CHB→A=B
16 14 15 sylanl2 ⊢R∈Dmn∧A∈X∧B∈X∧C∈X∧C≠Z→CHA=CHB→A=B
17 12 16 sylbid ⊢R∈Dmn∧A∈X∧B∈X∧C∈X∧C≠Z→AHC=BHC→A=B