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

Metamath Proof Explorer

Theorem lidl1el

Description: An ideal contains 1 iff it is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Wolf Lammen, 6-Sep-2020)

Ref Expression
Hypotheses lidlcl.u ⊢ U = LIdeal ⁡ R
lidlcl.b ⊢ B = Base R
lidl1el.o ⊢ 1 ˙ = 1 R
Assertion lidl1el ⊢ R ∈ Ring ∧ I ∈ U → 1 ˙ ∈ I ↔ I = B

Proof

Step Hyp Ref Expression
1 lidlcl.u ⊢ U = LIdeal ⁡ R
2 lidlcl.b ⊢ B = Base R
3 lidl1el.o ⊢ 1 ˙ = 1 R
4 2 1 lidlss ⊢ I ∈ U → I ⊆ B
5 4 ad2antlr ⊢ R ∈ Ring ∧ I ∈ U ∧ 1 ˙ ∈ I → I ⊆ B
6 eqid ⊢ ⋅ R = ⋅ R
7 2 6 3 ringridm ⊢ R ∈ Ring ∧ a ∈ B → a ⋅ R 1 ˙ = a
8 7 ad2ant2rl ⊢ R ∈ Ring ∧ I ∈ U ∧ 1 ˙ ∈ I ∧ a ∈ B → a ⋅ R 1 ˙ = a
9 1 2 6 lidlmcl ⊢ R ∈ Ring ∧ I ∈ U ∧ a ∈ B ∧ 1 ˙ ∈ I → a ⋅ R 1 ˙ ∈ I
10 9 ancom2s ⊢ R ∈ Ring ∧ I ∈ U ∧ 1 ˙ ∈ I ∧ a ∈ B → a ⋅ R 1 ˙ ∈ I
11 8 10 eqeltrrd ⊢ R ∈ Ring ∧ I ∈ U ∧ 1 ˙ ∈ I ∧ a ∈ B → a ∈ I
12 11 expr ⊢ R ∈ Ring ∧ I ∈ U ∧ 1 ˙ ∈ I → a ∈ B → a ∈ I
13 12 ssrdv ⊢ R ∈ Ring ∧ I ∈ U ∧ 1 ˙ ∈ I → B ⊆ I
14 5 13 eqssd ⊢ R ∈ Ring ∧ I ∈ U ∧ 1 ˙ ∈ I → I = B
15 14 ex ⊢ R ∈ Ring ∧ I ∈ U → 1 ˙ ∈ I → I = B
16 2 3 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ B
17 16 adantr ⊢ R ∈ Ring ∧ I ∈ U → 1 ˙ ∈ B
18 eleq2 ⊢ I = B → 1 ˙ ∈ I ↔ 1 ˙ ∈ B
19 17 18 syl5ibrcom ⊢ R ∈ Ring ∧ I ∈ U → I = B → 1 ˙ ∈ I
20 15 19 impbid ⊢ R ∈ Ring ∧ I ∈ U → 1 ˙ ∈ I ↔ I = B