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 ⁡ R
dmncan.2 ⊢ H = 2 nd ⁡ R
dmncan.3 ⊢ X = ran ⁡ G
dmncan.4 ⊢ Z = GId ⁡ G
Assertion dmncan2 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C ≠ Z → A H C = B H C → A = B

Proof

Step Hyp Ref Expression
1 dmncan.1 ⊢ G = 1 st ⁡ R
2 dmncan.2 ⊢ H = 2 nd ⁡ 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 → A H C = C H A
7 6 3adant3r2 ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C = C H A
8 1 2 3 crngocom ⊢ R ∈ CRingOps ∧ B ∈ X ∧ C ∈ X → B H C = C H B
9 8 3adant3r1 ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B H C = C H B
10 7 9 eqeq12d ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C = B H C ↔ C H A = C H B
11 5 10 sylan ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C = B H C ↔ C H A = C H B
12 11 adantr ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C ≠ Z → A H C = B H C ↔ C H A = C H B
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 → C H A = C H B → A = B
16 14 15 sylanl2 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C ≠ Z → C H A = C H B → A = B
17 12 16 sylbid ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C ≠ Z → A H C = B H C → A = B