This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isdomn4

Description: A ring is a domain iff it is nonzero and the left cancellation law for multiplication holds. (Contributed by SN, 15-Sep-2024)

Ref Expression
Hypotheses isdomn4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdomn4.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isdomn4.x ⊢ · = ( .r ‘ 𝑅 )
Assertion isdomn4 ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) )

Proof

Step Hyp Ref Expression
1 isdomn4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdomn4.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 isdomn4.x ⊢ · = ( .r ‘ 𝑅 )
4 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
5 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
6 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
7 6 adantr ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
8 eldifi ⊢ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → 𝑎 ∈ 𝐵 )
9 8 3ad2ant1 ⊢ ( ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → 𝑎 ∈ 𝐵 )
10 9 adantl ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
11 simpr2 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
12 simpr3 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ 𝐵 )
13 1 3 5 7 10 11 12 ringsubdi ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) = ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) )
14 13 eqeq1d ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) = 0 ↔ ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 ) )
15 simpll ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → 𝑅 ∈ Domn )
16 10 adantr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → 𝑎 ∈ 𝐵 )
17 eldifsni ⊢ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) → 𝑎 ≠ 0 )
18 17 3ad2ant1 ⊢ ( ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → 𝑎 ≠ 0 )
19 18 ad2antlr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → 𝑎 ≠ 0 )
20 6 ringgrpd ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Grp )
21 1 5 grpsubcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
22 20 21 syl3an1 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
23 22 3adant3r1 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
24 23 adantr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 )
25 simpr ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 )
26 1 3 2 domnmuln0 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑎 ≠ 0 ) ∧ ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ∈ 𝐵 ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) ) → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) ≠ 0 )
27 15 16 19 24 25 26 syl122anc ⊢ ( ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) ∧ ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 ) → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) ≠ 0 )
28 27 ex ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ≠ 0 → ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) ≠ 0 ) )
29 28 necon4d ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 · ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) ) = 0 → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ) )
30 14 29 sylbird ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 → ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ) )
31 20 adantr ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑅 ∈ Grp )
32 id ⊢ ( 𝑏 ∈ 𝐵 → 𝑏 ∈ 𝐵 )
33 1 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
34 6 8 32 33 syl3an ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
35 34 3adant3r3 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐵 )
36 id ⊢ ( 𝑐 ∈ 𝐵 → 𝑐 ∈ 𝐵 )
37 1 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 · 𝑐 ) ∈ 𝐵 )
38 6 8 36 37 syl3an ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑐 ∈ 𝐵 ) → ( 𝑎 · 𝑐 ) ∈ 𝐵 )
39 38 3adant3r2 ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( 𝑎 · 𝑐 ) ∈ 𝐵 )
40 1 2 5 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑎 · 𝑏 ) ∈ 𝐵 ∧ ( 𝑎 · 𝑐 ) ∈ 𝐵 ) → ( ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 ↔ ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) ) )
41 31 35 39 40 syl3anc ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( ( 𝑎 · 𝑏 ) ( -g ‘ 𝑅 ) ( 𝑎 · 𝑐 ) ) = 0 ↔ ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) ) )
42 1 2 5 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) → ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ↔ 𝑏 = 𝑐 ) )
43 31 11 12 42 syl3anc ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑏 ( -g ‘ 𝑅 ) 𝑐 ) = 0 ↔ 𝑏 = 𝑐 ) )
44 30 41 43 3imtr3d ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵 ) ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) )
45 44 ralrimivvva ⊢ ( 𝑅 ∈ Domn → ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) )
46 4 45 jca ⊢ ( 𝑅 ∈ Domn → ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) )
47 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
48 47 ringgrpd ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Grp )
49 1 2 grpidcl ⊢ ( 𝑅 ∈ Grp → 0 ∈ 𝐵 )
50 48 49 syl ⊢ ( 𝑅 ∈ NzRing → 0 ∈ 𝐵 )
51 50 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → 0 ∈ 𝐵 )
52 oveq2 ⊢ ( 𝑐 = 0 → ( 𝑎 · 𝑐 ) = ( 𝑎 · 0 ) )
53 52 eqeq2d ⊢ ( 𝑐 = 0 → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) ↔ ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) ) )
54 eqeq2 ⊢ ( 𝑐 = 0 → ( 𝑏 = 𝑐 ↔ 𝑏 = 0 ) )
55 53 54 imbi12d ⊢ ( 𝑐 = 0 → ( ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ↔ ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ) )
56 55 rspcv ⊢ ( 0 ∈ 𝐵 → ( ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ) )
57 51 56 syl ⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ) )
58 1 3 2 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 · 0 ) = 0 )
59 47 8 58 syl2an ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑎 · 0 ) = 0 )
60 59 adantrr ⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 · 0 ) = 0 )
61 60 eqeq2d ⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) ↔ ( 𝑎 · 𝑏 ) = 0 ) )
62 61 imbi1d ⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 0 ) → 𝑏 = 0 ) ↔ ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
63 57 62 sylibd ⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
64 63 ralimdvva ⊢ ( 𝑅 ∈ NzRing → ( ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) ) )
65 isdomn5 ⊢ ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ↔ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → 𝑏 = 0 ) )
66 64 65 imbitrrdi ⊢ ( 𝑅 ∈ NzRing → ( ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
67 66 imdistani ⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) → ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
68 1 3 2 isdomn ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = 0 → ( 𝑎 = 0 ∨ 𝑏 = 0 ) ) ) )
69 67 68 sylibr ⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) → 𝑅 ∈ Domn )
70 46 69 impbii ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑎 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑐 ) → 𝑏 = 𝑐 ) ) )