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

Metamath Proof Explorer

Theorem lidlunitel

Description: If an ideal I contains a unit J , then it is the whole ring. (Contributed by Thierry Arnoux, 19-Mar-2025)

Ref Expression
Hypotheses lidlunitel.1 ⊢ B = Base R
lidlunitel.2 ⊢ U = Unit ⁡ R
lidlunitel.3 ⊢ φ → J ∈ U
lidlunitel.4 ⊢ φ → J ∈ I
lidlunitel.5 ⊢ φ → R ∈ Ring
lidlunitel.6 ⊢ φ → I ∈ LIdeal ⁡ R
Assertion lidlunitel ⊢ φ → I = B

Proof

Step Hyp Ref Expression
1 lidlunitel.1 ⊢ B = Base R
2 lidlunitel.2 ⊢ U = Unit ⁡ R
3 lidlunitel.3 ⊢ φ → J ∈ U
4 lidlunitel.4 ⊢ φ → J ∈ I
5 lidlunitel.5 ⊢ φ → R ∈ Ring
6 lidlunitel.6 ⊢ φ → I ∈ LIdeal ⁡ R
7 eqid ⊢ inv r ⁡ R = inv r ⁡ R
8 eqid ⊢ ⋅ R = ⋅ R
9 eqid ⊢ 1 R = 1 R
10 2 7 8 9 unitlinv ⊢ R ∈ Ring ∧ J ∈ U → inv r ⁡ R ⁡ J ⋅ R J = 1 R
11 5 3 10 syl2anc ⊢ φ → inv r ⁡ R ⁡ J ⋅ R J = 1 R
12 1 2 unitss ⊢ U ⊆ B
13 2 7 unitinvcl ⊢ R ∈ Ring ∧ J ∈ U → inv r ⁡ R ⁡ J ∈ U
14 5 3 13 syl2anc ⊢ φ → inv r ⁡ R ⁡ J ∈ U
15 12 14 sselid ⊢ φ → inv r ⁡ R ⁡ J ∈ B
16 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
17 16 1 8 lidlmcl ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R ∧ inv r ⁡ R ⁡ J ∈ B ∧ J ∈ I → inv r ⁡ R ⁡ J ⋅ R J ∈ I
18 5 6 15 4 17 syl22anc ⊢ φ → inv r ⁡ R ⁡ J ⋅ R J ∈ I
19 11 18 eqeltrrd ⊢ φ → 1 R ∈ I
20 16 1 9 lidl1el ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R → 1 R ∈ I ↔ I = B
21 20 biimpa ⊢ R ∈ Ring ∧ I ∈ LIdeal ⁡ R ∧ 1 R ∈ I → I = B
22 5 6 19 21 syl21anc ⊢ φ → I = B