Metamath Proof Explorer

Theorem dmncan1

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 dmncan1 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → A H B = A H C → B = C

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 dmnrngo ⊢ R ∈ Dmn → R ∈ RingOps
6 eqid ⊢ / g ⁡ G = / g ⁡ G
7 1 2 3 6 rngosubdi ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B / g ⁡ G C = A H B / g ⁡ G A H C
8 5 7 sylan ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B / g ⁡ G C = A H B / g ⁡ G A H C
9 8 adantr ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → A H B / g ⁡ G C = A H B / g ⁡ G A H C
10 9 eqeq1d ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → A H B / g ⁡ G C = Z ↔ A H B / g ⁡ G A H C = Z
11 1 rngogrpo ⊢ R ∈ RingOps → G ∈ GrpOp
12 5 11 syl ⊢ R ∈ Dmn → G ∈ GrpOp
13 3 6 grpodivcl ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B / g ⁡ G C ∈ X
14 13 3expb ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B / g ⁡ G C ∈ X
15 12 14 sylan ⊢ R ∈ Dmn ∧ B ∈ X ∧ C ∈ X → B / g ⁡ G C ∈ X
16 15 adantlr ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B / g ⁡ G C ∈ X
17 1 2 3 4 dmnnzd ⊢ R ∈ Dmn ∧ A ∈ X ∧ B / g ⁡ G C ∈ X ∧ A H B / g ⁡ G C = Z → A = Z ∨ B / g ⁡ G C = Z
18 17 3exp2 ⊢ R ∈ Dmn → A ∈ X → B / g ⁡ G C ∈ X → A H B / g ⁡ G C = Z → A = Z ∨ B / g ⁡ G C = Z
19 18 imp31 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B / g ⁡ G C ∈ X → A H B / g ⁡ G C = Z → A = Z ∨ B / g ⁡ G C = Z
20 16 19 syldan ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B / g ⁡ G C = Z → A = Z ∨ B / g ⁡ G C = Z
21 20 exp43 ⊢ R ∈ Dmn → A ∈ X → B ∈ X → C ∈ X → A H B / g ⁡ G C = Z → A = Z ∨ B / g ⁡ G C = Z
22 21 3imp2 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B / g ⁡ G C = Z → A = Z ∨ B / g ⁡ G C = Z
23 neor ⊢ A = Z ∨ B / g ⁡ G C = Z ↔ A ≠ Z → B / g ⁡ G C = Z
24 22 23 imbitrdi ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B / g ⁡ G C = Z → A ≠ Z → B / g ⁡ G C = Z
25 24 com23 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ≠ Z → A H B / g ⁡ G C = Z → B / g ⁡ G C = Z
26 25 imp ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → A H B / g ⁡ G C = Z → B / g ⁡ G C = Z
27 10 26 sylbird ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → A H B / g ⁡ G A H C = Z → B / g ⁡ G C = Z
28 12 adantr ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → G ∈ GrpOp
29 1 2 3 rngocl ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H B ∈ X
30 29 3adant3r3 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B ∈ X
31 5 30 sylan ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B ∈ X
32 1 2 3 rngocl ⊢ R ∈ RingOps ∧ A ∈ X ∧ C ∈ X → A H C ∈ X
33 32 3adant3r2 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C ∈ X
34 5 33 sylan ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H C ∈ X
35 3 4 6 grpoeqdivid ⊢ G ∈ GrpOp ∧ A H B ∈ X ∧ A H C ∈ X → A H B = A H C ↔ A H B / g ⁡ G A H C = Z
36 28 31 34 35 syl3anc ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A H B = A H C ↔ A H B / g ⁡ G A H C = Z
37 36 adantr ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → A H B = A H C ↔ A H B / g ⁡ G A H C = Z
38 3 4 6 grpoeqdivid ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B = C ↔ B / g ⁡ G C = Z
39 38 3expb ⊢ G ∈ GrpOp ∧ B ∈ X ∧ C ∈ X → B = C ↔ B / g ⁡ G C = Z
40 12 39 sylan ⊢ R ∈ Dmn ∧ B ∈ X ∧ C ∈ X → B = C ↔ B / g ⁡ G C = Z
41 40 3adantr1 ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B = C ↔ B / g ⁡ G C = Z
42 41 adantr ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → B = C ↔ B / g ⁡ G C = Z
43 27 37 42 3imtr4d ⊢ R ∈ Dmn ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A ≠ Z → A H B = A H C → B = C