MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isirred Structured version   Visualization version   GIF version

Theorem isirred 19139
Description: An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014.)
Hypotheses
Ref Expression
irred.1 𝐵 = (Base‘𝑅)
irred.2 𝑈 = (Unit‘𝑅)
irred.3 𝐼 = (Irred‘𝑅)
irred.4 𝑁 = (𝐵𝑈)
irred.5 · = (.r𝑅)
Assertion
Ref Expression
isirred (𝑋𝐼 ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
Distinct variable groups:   𝑥,𝑦,𝑁   𝑥,𝑅,𝑦   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)   · (𝑥,𝑦)   𝑈(𝑥,𝑦)   𝐼(𝑥,𝑦)

Proof of Theorem isirred
Dummy variables 𝑟 𝑏 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvdm 6570 . . . 4 (𝑋 ∈ (Irred‘𝑅) → 𝑅 ∈ dom Irred)
2 irred.3 . . . 4 𝐼 = (Irred‘𝑅)
31, 2eleq2s 2901 . . 3 (𝑋𝐼𝑅 ∈ dom Irred)
43elexd 3457 . 2 (𝑋𝐼𝑅 ∈ V)
5 eldifi 4024 . . . . . 6 (𝑋 ∈ (𝐵𝑈) → 𝑋𝐵)
6 irred.4 . . . . . 6 𝑁 = (𝐵𝑈)
75, 6eleq2s 2901 . . . . 5 (𝑋𝑁𝑋𝐵)
8 irred.1 . . . . 5 𝐵 = (Base‘𝑅)
97, 8syl6eleq 2893 . . . 4 (𝑋𝑁𝑋 ∈ (Base‘𝑅))
109elfvexd 6572 . . 3 (𝑋𝑁𝑅 ∈ V)
1110adantr 481 . 2 ((𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋) → 𝑅 ∈ V)
12 fvex 6551 . . . . . . . 8 (Base‘𝑟) ∈ V
13 difexg 5122 . . . . . . . 8 ((Base‘𝑟) ∈ V → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V)
1412, 13mp1i 13 . . . . . . 7 (𝑟 = 𝑅 → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V)
15 simpr 485 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟)))
16 simpl 483 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑟 = 𝑅)
1716fveq2d 6542 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = (Base‘𝑅))
1817, 8syl6eqr 2849 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = 𝐵)
1916fveq2d 6542 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = (Unit‘𝑅))
20 irred.2 . . . . . . . . . . . 12 𝑈 = (Unit‘𝑅)
2119, 20syl6eqr 2849 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = 𝑈)
2218, 21difeq12d 4021 . . . . . . . . . 10 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = (𝐵𝑈))
2322, 6syl6eqr 2849 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = 𝑁)
2415, 23eqtrd 2831 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = 𝑁)
2516fveq2d 6542 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r𝑟) = (.r𝑅))
26 irred.5 . . . . . . . . . . . . 13 · = (.r𝑅)
2725, 26syl6eqr 2849 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r𝑟) = · )
2827oveqd 7033 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (𝑥(.r𝑟)𝑦) = (𝑥 · 𝑦))
2928neeq1d 3043 . . . . . . . . . 10 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑧))
3024, 29raleqbidv 3361 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧))
3124, 30raleqbidv 3361 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧))
3224, 31rabeqbidv 3430 . . . . . . 7 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → {𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧} = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
3314, 32csbied 3844 . . . . . 6 (𝑟 = 𝑅((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧} = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
34 df-irred 19083 . . . . . 6 Irred = (𝑟 ∈ V ↦ ((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧})
35 fvex 6551 . . . . . . . . . 10 (Base‘𝑅) ∈ V
368, 35eqeltri 2879 . . . . . . . . 9 𝐵 ∈ V
3736difexi 5123 . . . . . . . 8 (𝐵𝑈) ∈ V
386, 37eqeltri 2879 . . . . . . 7 𝑁 ∈ V
3938rabex 5126 . . . . . 6 {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧} ∈ V
4033, 34, 39fvmpt 6635 . . . . 5 (𝑅 ∈ V → (Irred‘𝑅) = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
412, 40syl5eq 2843 . . . 4 (𝑅 ∈ V → 𝐼 = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
4241eleq2d 2868 . . 3 (𝑅 ∈ V → (𝑋𝐼𝑋 ∈ {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧}))
43 neeq2 3047 . . . . 5 (𝑧 = 𝑋 → ((𝑥 · 𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑋))
44432ralbidv 3166 . . . 4 (𝑧 = 𝑋 → (∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧 ↔ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
4544elrab 3618 . . 3 (𝑋 ∈ {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧} ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
4642, 45syl6bb 288 . 2 (𝑅 ∈ V → (𝑋𝐼 ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋)))
474, 11, 46pm5.21nii 380 1 (𝑋𝐼 ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1522  wcel 2081  wne 2984  wral 3105  {crab 3109  Vcvv 3437  csb 3811  cdif 3856  dom cdm 5443  cfv 6225  (class class class)co 7016  Basecbs 16312  .rcmulr 16395  Unitcui 19079  Irredcir 19080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-iota 6189  df-fun 6227  df-fv 6233  df-ov 7019  df-irred 19083
This theorem is referenced by:  isnirred  19140  isirred2  19141  opprirred  19142
  Copyright terms: Public domain W3C validator