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

Metamath Proof Explorer

Theorem irredcl

Description: An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i ⊢ I = Irred ⁡ R
irredcl.b ⊢ B = Base R
Assertion irredcl ⊢ X ∈ I → X ∈ B

Proof

Step Hyp Ref Expression
1 irredn0.i ⊢ I = Irred ⁡ R
2 irredcl.b ⊢ B = Base R
3 eqid ⊢ Unit ⁡ R = Unit ⁡ R
4 eqid ⊢ ⋅ R = ⋅ R
5 2 3 1 4 isirred2 ⊢ X ∈ I ↔ X ∈ B ∧ ¬ X ∈ Unit ⁡ R ∧ ∀ x ∈ B ∀ y ∈ B x ⋅ R y = X → x ∈ Unit ⁡ R ∨ y ∈ Unit ⁡ R
6 5 simp1bi ⊢ X ∈ I → X ∈ B