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

Theorem isirred 20401
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 6938 . . . 4 (𝑋 ∈ (Irred‘𝑅) → 𝑅 ∈ dom Irred)
2 irred.3 . . . 4 𝐼 = (Irred‘𝑅)
31, 2eleq2s 2844 . . 3 (𝑋𝐼𝑅 ∈ dom Irred)
43elexd 3485 . 2 (𝑋𝐼𝑅 ∈ V)
5 eldifi 4126 . . . . . 6 (𝑋 ∈ (𝐵𝑈) → 𝑋𝐵)
6 irred.4 . . . . . 6 𝑁 = (𝐵𝑈)
75, 6eleq2s 2844 . . . . 5 (𝑋𝑁𝑋𝐵)
8 irred.1 . . . . 5 𝐵 = (Base‘𝑅)
97, 8eleqtrdi 2836 . . . 4 (𝑋𝑁𝑋 ∈ (Base‘𝑅))
109elfvexd 6940 . . 3 (𝑋𝑁𝑅 ∈ V)
1110adantr 479 . 2 ((𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋) → 𝑅 ∈ V)
12 fvex 6914 . . . . . . . 8 (Base‘𝑟) ∈ V
13 difexg 5334 . . . . . . . 8 ((Base‘𝑟) ∈ V → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V)
1412, 13mp1i 13 . . . . . . 7 (𝑟 = 𝑅 → ((Base‘𝑟) ∖ (Unit‘𝑟)) ∈ V)
15 simpr 483 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟)))
16 simpl 481 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑟 = 𝑅)
1716fveq2d 6905 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = (Base‘𝑅))
1817, 8eqtr4di 2784 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Base‘𝑟) = 𝐵)
1916fveq2d 6905 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = (Unit‘𝑅))
20 irred.2 . . . . . . . . . . . 12 𝑈 = (Unit‘𝑅)
2119, 20eqtr4di 2784 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (Unit‘𝑟) = 𝑈)
2218, 21difeq12d 4122 . . . . . . . . . 10 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = (𝐵𝑈))
2322, 6eqtr4di 2784 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((Base‘𝑟) ∖ (Unit‘𝑟)) = 𝑁)
2415, 23eqtrd 2766 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → 𝑏 = 𝑁)
2516fveq2d 6905 . . . . . . . . . . . . 13 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r𝑟) = (.r𝑅))
26 irred.5 . . . . . . . . . . . . 13 · = (.r𝑅)
2725, 26eqtr4di 2784 . . . . . . . . . . . 12 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (.r𝑟) = · )
2827oveqd 7441 . . . . . . . . . . 11 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (𝑥(.r𝑟)𝑦) = (𝑥 · 𝑦))
2928neeq1d 2990 . . . . . . . . . 10 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → ((𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑧))
3024, 29raleqbidv 3330 . . . . . . . . 9 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧))
3124, 30raleqbidv 3330 . . . . . . . 8 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → (∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧 ↔ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧))
3224, 31rabeqbidv 3437 . . . . . . 7 ((𝑟 = 𝑅𝑏 = ((Base‘𝑟) ∖ (Unit‘𝑟))) → {𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧} = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
3314, 32csbied 3930 . . . . . 6 (𝑟 = 𝑅((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧} = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
34 df-irred 20341 . . . . . 6 Irred = (𝑟 ∈ V ↦ ((Base‘𝑟) ∖ (Unit‘𝑟)) / 𝑏{𝑧𝑏 ∣ ∀𝑥𝑏𝑦𝑏 (𝑥(.r𝑟)𝑦) ≠ 𝑧})
35 fvex 6914 . . . . . . . . . 10 (Base‘𝑅) ∈ V
368, 35eqeltri 2822 . . . . . . . . 9 𝐵 ∈ V
3736difexi 5335 . . . . . . . 8 (𝐵𝑈) ∈ V
386, 37eqeltri 2822 . . . . . . 7 𝑁 ∈ V
3938rabex 5339 . . . . . 6 {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧} ∈ V
4033, 34, 39fvmpt 7009 . . . . 5 (𝑅 ∈ V → (Irred‘𝑅) = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
412, 40eqtrid 2778 . . . 4 (𝑅 ∈ V → 𝐼 = {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧})
4241eleq2d 2812 . . 3 (𝑅 ∈ V → (𝑋𝐼𝑋 ∈ {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧}))
43 neeq2 2994 . . . . 5 (𝑧 = 𝑋 → ((𝑥 · 𝑦) ≠ 𝑧 ↔ (𝑥 · 𝑦) ≠ 𝑋))
44432ralbidv 3209 . . . 4 (𝑧 = 𝑋 → (∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧 ↔ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
4544elrab 3681 . . 3 (𝑋 ∈ {𝑧𝑁 ∣ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑧} ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
4642, 45bitrdi 286 . 2 (𝑅 ∈ V → (𝑋𝐼 ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋)))
474, 11, 46pm5.21nii 377 1 (𝑋𝐼 ↔ (𝑋𝑁 ∧ ∀𝑥𝑁𝑦𝑁 (𝑥 · 𝑦) ≠ 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1534  wcel 2099  wne 2930  wral 3051  {crab 3419  Vcvv 3462  csb 3892  cdif 3944  dom cdm 5682  cfv 6554  (class class class)co 7424  Basecbs 17213  .rcmulr 17267  Unitcui 20337  Irredcir 20338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-iota 6506  df-fun 6556  df-fv 6562  df-ov 7427  df-irred 20341
This theorem is referenced by:  isnirred  20402  isirred2  20403  opprirred  20404  mxidlirredi  33346  rprmirred  33406  ply1dg3rt0irred  33454
  Copyright terms: Public domain W3C validator