| Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > isufd | Structured version Visualization version GIF version | ||
| Description: The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| Ref | Expression |
|---|---|
| isufd.i | ⊢ 𝐼 = (PrmIdeal‘𝑅) |
| isufd.3 | ⊢ 𝑃 = (RPrime‘𝑅) |
| isufd.0 | ⊢ 0 = (0g‘𝑅) |
| Ref | Expression |
|---|---|
| isufd | ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 6904 | . . . . 5 ⊢ (𝑟 = 𝑅 → (PrmIdeal‘𝑟) = (PrmIdeal‘𝑅)) | |
| 2 | isufd.i | . . . . 5 ⊢ 𝐼 = (PrmIdeal‘𝑅) | |
| 3 | 1, 2 | eqtr4di 2794 | . . . 4 ⊢ (𝑟 = 𝑅 → (PrmIdeal‘𝑟) = 𝐼) |
| 4 | fveq2 6904 | . . . . . . 7 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) | |
| 5 | isufd.0 | . . . . . . 7 ⊢ 0 = (0g‘𝑅) | |
| 6 | 4, 5 | eqtr4di 2794 | . . . . . 6 ⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
| 7 | 6 | sneqd 4636 | . . . . 5 ⊢ (𝑟 = 𝑅 → {(0g‘𝑟)} = { 0 }) |
| 8 | 7 | sneqd 4636 | . . . 4 ⊢ (𝑟 = 𝑅 → {{(0g‘𝑟)}} = {{ 0 }}) |
| 9 | 3, 8 | difeq12d 4126 | . . 3 ⊢ (𝑟 = 𝑅 → ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}}) = (𝐼 ∖ {{ 0 }})) |
| 10 | fveq2 6904 | . . . . . 6 ⊢ (𝑟 = 𝑅 → (RPrime‘𝑟) = (RPrime‘𝑅)) | |
| 11 | isufd.3 | . . . . . 6 ⊢ 𝑃 = (RPrime‘𝑅) | |
| 12 | 10, 11 | eqtr4di 2794 | . . . . 5 ⊢ (𝑟 = 𝑅 → (RPrime‘𝑟) = 𝑃) |
| 13 | 12 | ineq2d 4219 | . . . 4 ⊢ (𝑟 = 𝑅 → (𝑖 ∩ (RPrime‘𝑟)) = (𝑖 ∩ 𝑃)) |
| 14 | 13 | neeq1d 2999 | . . 3 ⊢ (𝑟 = 𝑅 → ((𝑖 ∩ (RPrime‘𝑟)) ≠ ∅ ↔ (𝑖 ∩ 𝑃) ≠ ∅)) |
| 15 | 9, 14 | raleqbidv 3345 | . 2 ⊢ (𝑟 = 𝑅 → (∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅ ↔ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅)) |
| 16 | df-ufd 33554 | . 2 ⊢ UFD = {𝑟 ∈ IDomn ∣ ∀𝑖 ∈ ((PrmIdeal‘𝑟) ∖ {{(0g‘𝑟)}})(𝑖 ∩ (RPrime‘𝑟)) ≠ ∅} | |
| 17 | 15, 16 | elrab2 3694 | 1 ⊢ (𝑅 ∈ UFD ↔ (𝑅 ∈ IDomn ∧ ∀𝑖 ∈ (𝐼 ∖ {{ 0 }})(𝑖 ∩ 𝑃) ≠ ∅)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2939 ∀wral 3060 ∖ cdif 3947 ∩ cin 3949 ∅c0 4332 {csn 4624 ‘cfv 6559 0gc0g 17480 RPrimecrpm 20424 IDomncidom 20685 PrmIdealcprmidl 33450 UFDcufd 33553 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2707 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2714 df-cleq 2728 df-clel 2815 df-ne 2940 df-ral 3061 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4906 df-br 5142 df-iota 6512 df-fv 6567 df-ufd 33554 |
| This theorem is referenced by: ufdprmidl 33556 ufdidom 33557 pidufd 33558 1arithufdlem4 33562 dfufd2 33565 |
| Copyright terms: Public domain | W3C validator |