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

Theorem isirred 18522
 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 6130 . . . 4 (𝑋 ∈ (Irred‘𝑅) → 𝑅 ∈ dom Irred)
2 irred.3 . . . 4 𝐼 = (Irred‘𝑅)
31, 2eleq2s 2706 . . 3 (𝑋𝐼𝑅 ∈ dom Irred)
4 elex 3185 . . 3 (𝑅 ∈ dom Irred → 𝑅 ∈ V)
53, 4syl 17 . 2 (𝑋𝐼𝑅 ∈ V)
6 eldifi 3694 . . . . . 6 (𝑋 ∈ (𝐵𝑈) → 𝑋𝐵)
7 irred.4 . . . . . 6 𝑁 = (𝐵𝑈)
86, 7eleq2s 2706 . . . . 5 (𝑋𝑁𝑋𝐵)
9 irred.1 . . . . 5 𝐵 = (Base‘𝑅)
108, 9syl6eleq 2698 . . . 4 (𝑋𝑁𝑋 ∈ (Base‘𝑅))
1110elfvexd 6132 . . 3 (𝑋𝑁𝑅 ∈ V)
1211adantr 480 . 2 ((𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋) → 𝑅 ∈ V)
13 fvex 6113 . . . . . . . 8 (Base‘𝑟) ∈ V
14 difexg 4735 . . . . . . . 8 ((Base‘𝑟) ∈ V → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V)
1513, 14mp1i 13 . . . . . . 7 (𝑟 = 𝑅 → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V)
16 simpr 476 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟)))
17 simpl 472 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑟 = 𝑅)
1817fveq2d 6107 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = (Base‘𝑅))
1918, 9syl6eqr 2662 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = 𝐵)
2017fveq2d 6107 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = (Unit‘𝑅))
21 irred.2 . . . . . . . . . . . 12 𝑈 = (Unit‘𝑅)
2220, 21syl6eqr 2662 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = 𝑈)
2319, 22difeq12d 3691 . . . . . . . . . 10 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = (𝐵𝑈))
2423, 7syl6eqr 2662 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = 𝑁)
2516, 24eqtrd 2644 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = 𝑁)
2617fveq2d 6107 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r𝑟) = (.r𝑅))
27 irred.5 . . . . . . . . . . . . 13 · = (.r𝑅)
2826, 27syl6eqr 2662 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r𝑟) = · )
2928oveqd 6566 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (𝑥(.r𝑟)𝑦) = (𝑥 · 𝑦))
3029neeq1d 2841 . . . . . . . . . 10 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑧))
3125, 30raleqbidv 3129 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧))
3225, 31raleqbidv 3129 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧))
3325, 32rabeqbidv 3168 . . . . . . 7 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → {𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧} = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
3415, 33csbied 3526 . . . . . 6 (𝑟 = 𝑅((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧} = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
35 df-irred 18466 . . . . . 6 Irred = (𝑟 ∈ V ↦ ((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧})
36 fvex 6113 . . . . . . . . . 10 (Base‘𝑅) ∈ V
379, 36eqeltri 2684 . . . . . . . . 9 𝐵 ∈ V
38 difexg 4735 . . . . . . . . 9 (𝐵 ∈ V → (𝐵𝑈) ∈ V)
3937, 38ax-mp 5 . . . . . . . 8 (𝐵𝑈) ∈ V
407, 39eqeltri 2684 . . . . . . 7 𝑁 ∈ V
4140rabex 4740 . . . . . 6 {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧} ∈ V
4234, 35, 41fvmpt 6191 . . . . 5 (𝑅 ∈ V → (Irred‘𝑅) = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
432, 42syl5eq 2656 . . . 4 (𝑅 ∈ V → 𝐼 = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
4443eleq2d 2673 . . 3 (𝑅 ∈ V → (𝑋𝐼𝑋 ∈ {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧}))
45 neeq2 2845 . . . . 5 (𝑧 = 𝑋 → ((𝑥 · 𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑋))
46452ralbidv 2972 . . . 4 (𝑧 = 𝑋 → (∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧 ↔ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
4746elrab 3331 . . 3 (𝑋 ∈ {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧} ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
4844, 47syl6bb 275 . 2 (𝑅 ∈ V → (𝑋𝐼 ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋)))
495, 12, 48pm5.21nii 367 1 (𝑋𝐼 ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  {crab 2900  Vcvv 3173  ⦋csb 3499   ∖ cdif 3537  dom cdm 5038  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  .rcmulr 15769  Unitcui 18462  Irredcir 18463 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552  df-irred 18466 This theorem is referenced by:  isnirred  18523  isirred2  18524  opprirred  18525
 Copyright terms: Public domain W3C validator