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

Metamath Proof Explorer

Theorem pridln1

Description: A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024)

Ref Expression
Hypotheses pridln1.1 ⊢ B = Base R
pridln1.2 ⊢ 1 ˙ = 1 R
Assertion pridln1 ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R ∧ I ≠ B → ¬ 1 ˙ ∈ I

Proof

Step Hyp Ref Expression
1 pridln1.1 ⊢ B = Base R
2 pridln1.2 ⊢ 1 ˙ = 1 R
3 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
4 3 1 2 lidl1el ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R → 1 ˙ ∈ I ↔ I = B
5 4 necon3bbid ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R → ¬ 1 ˙ ∈ I ↔ I ≠ B
6 5 biimp3ar ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R ∧ I ≠ B → ¬ 1 ˙ ∈ I