Metamath Proof Explorer

Theorem dmncan1

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

Ref Expression
Hypotheses dmncan.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
dmncan.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
dmncan.3 ⊢ 𝑋 = ran 𝐺
dmncan.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion dmncan1 ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐻 𝐶 ) → 𝐵 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 dmncan.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 dmncan.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 dmncan.3 ⊢ 𝑋 = ran 𝐺
4 dmncan.4 ⊢ 𝑍 = ( GId ‘ 𝐺 )
5 dmnrngo ⊢ ( 𝑅 ∈ Dmn → 𝑅 ∈ RingOps )
6 eqid ⊢ ( /𝑔 ‘ 𝐺 ) = ( /𝑔 ‘ 𝐺 )
7 1 2 3 6 rngosubdi ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) )
8 5 7 sylan ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) )
9 8 adantr ⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) )
10 9 eqeq1d ⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 ↔ ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) = 𝑍 ) )
11 1 rngogrpo ⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
12 5 11 syl ⊢ ( 𝑅 ∈ Dmn → 𝐺 ∈ GrpOp )
13 3 6 grpodivcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 )
14 13 3expb ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 )
15 12 14 sylan ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 )
16 15 adantlr ⊢ ( ( ( 𝑅 ∈ Dmn ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 )
17 1 2 3 4 dmnnzd ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 ∧ ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 ) ) → ( 𝐴 = 𝑍 ∨ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
18 17 3exp2 ⊢ ( 𝑅 ∈ Dmn → ( 𝐴 ∈ 𝑋 → ( ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐴 = 𝑍 ∨ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ) ) ) )
19 18 imp31 ⊢ ( ( ( 𝑅 ∈ Dmn ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐴 = 𝑍 ∨ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ) )
20 16 19 syldan ⊢ ( ( ( 𝑅 ∈ Dmn ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐴 = 𝑍 ∨ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ) )
21 20 exp43 ⊢ ( 𝑅 ∈ Dmn → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐶 ∈ 𝑋 → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐴 = 𝑍 ∨ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ) ) ) ) )
22 21 3imp2 ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐴 = 𝑍 ∨ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ) )
23 neor ⊢ ( ( 𝐴 = 𝑍 ∨ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ↔ ( 𝐴 ≠ 𝑍 → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
24 22 23 syl6ib ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐴 ≠ 𝑍 → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ) )
25 24 com23 ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 ≠ 𝑍 → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) ) )
26 25 imp ⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( ( 𝐴 𝐻 ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) ) = 𝑍 → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
27 10 26 sylbird ⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) = 𝑍 → ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
28 12 adantr ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐺 ∈ GrpOp )
29 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
30 29 3adant3r3 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
31 5 30 sylan ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
32 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 )
33 32 3adant3r2 ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 )
34 5 33 sylan ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 )
35 3 4 6 grpoeqdivid ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 ∧ ( 𝐴 𝐻 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐻 𝐶 ) ↔ ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) = 𝑍 ) )
36 28 31 34 35 syl3anc ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐻 𝐶 ) ↔ ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) = 𝑍 ) )
37 36 adantr ⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐻 𝐶 ) ↔ ( ( 𝐴 𝐻 𝐵 ) ( /𝑔 ‘ 𝐺 ) ( 𝐴 𝐻 𝐶 ) ) = 𝑍 ) )
38 3 4 6 grpoeqdivid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 = 𝐶 ↔ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
39 38 3expb ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
40 12 39 sylan ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
41 40 3adantr1 ⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
42 41 adantr ⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( 𝐵 = 𝐶 ↔ ( 𝐵 ( /𝑔 ‘ 𝐺 ) 𝐶 ) = 𝑍 ) )
43 27 37 42 3imtr4d ⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 ≠ 𝑍 ) → ( ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐻 𝐶 ) → 𝐵 = 𝐶 ) )