Metamath Proof Explorer

Theorem idomcanl

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 13-Jul-2026)

Ref Expression
Hypotheses isidom3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isidom3.t ⊢ · = ( .r ‘ 𝑅 )
isidom3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion idomcanl ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) → 𝑌 = 𝑍 ) )

Proof

Step Hyp Ref Expression
1 isidom3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isidom3.t ⊢ · = ( .r ‘ 𝑅 )
3 isidom3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
5 isidom ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
6 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
7 6 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) → 𝑅 ∈ Ring )
8 5 7 sylbi ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Ring )
9 8 adantr ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
10 simpr1 ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11 simpr2 ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
12 simpr3 ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
13 1 2 4 9 10 11 12 ringsubdi ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) )
14 13 adantr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) )
15 14 eqeq1d ⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 ↔ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = 0 ) )
16 8 ringgrpd ⊢ ( 𝑅 ∈ IDomn → 𝑅 ∈ Grp )
17 1 4 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ∈ 𝐵 )
18 17 3expb ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ∈ 𝐵 )
19 16 18 sylan ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ∈ 𝐵 )
20 19 adantlr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ∈ 𝐵 )
21 1 2 3 idomnzd ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ∈ 𝐵 ∧ ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 ) ) → ( 𝑋 = 0 ∨ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
22 21 3exp2 ⊢ ( 𝑅 ∈ IDomn → ( 𝑋 ∈ 𝐵 → ( ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ∈ 𝐵 → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑋 = 0 ∨ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ) ) ) )
23 22 imp31 ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑋 = 0 ∨ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ) )
24 20 23 syldan ⊢ ( ( ( 𝑅 ∈ IDomn ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑋 = 0 ∨ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ) )
25 24 exp43 ⊢ ( 𝑅 ∈ IDomn → ( 𝑋 ∈ 𝐵 → ( 𝑌 ∈ 𝐵 → ( 𝑍 ∈ 𝐵 → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑋 = 0 ∨ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ) ) ) ) )
26 25 3imp2 ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑋 = 0 ∨ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ) )
27 neor ⊢ ( ( 𝑋 = 0 ∨ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ↔ ( 𝑋 ≠ 0 → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
28 26 27 imbitrdi ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑋 ≠ 0 → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ) )
29 28 com23 ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ≠ 0 → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) ) )
30 29 imp ⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑋 · ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) ) = 0 → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
31 15 30 sylbird ⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = 0 → ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
32 16 adantr ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑅 ∈ Grp )
33 1 2 9 10 11 ringcld ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
34 1 2 9 10 12 ringcld ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 · 𝑍 ) ∈ 𝐵 )
35 1 3 4 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ) → ( ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = 0 ↔ ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ) )
36 35 bicomd ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 · 𝑍 ) ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ↔ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = 0 ) )
37 32 33 34 36 syl3anc ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ↔ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = 0 ) )
38 37 adantr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) ↔ ( ( 𝑋 · 𝑌 ) ( -g ‘ 𝑅 ) ( 𝑋 · 𝑍 ) ) = 0 ) )
39 1 3 4 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ↔ 𝑌 = 𝑍 ) )
40 39 bicomd ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 = 𝑍 ↔ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
41 40 3expb ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 = 𝑍 ↔ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
42 16 41 sylan ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 = 𝑍 ↔ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
43 42 3adantr1 ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 = 𝑍 ↔ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
44 43 adantr ⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( 𝑌 = 𝑍 ↔ ( 𝑌 ( -g ‘ 𝑅 ) 𝑍 ) = 0 ) )
45 31 38 44 3imtr4d ⊢ ( ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 ≠ 0 ) → ( ( 𝑋 · 𝑌 ) = ( 𝑋 · 𝑍 ) → 𝑌 = 𝑍 ) )