Metamath Proof Explorer

Theorem islpidl

Description: Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p ⊢ P = LPIdeal ⁡ R
lpival.k ⊢ K = RSpan ⁡ R
lpival.b ⊢ B = Base R
Assertion islpidl ⊢ R ∈ Ring → I ∈ P ↔ ∃ g ∈ B I = K ⁡ g

Proof

Step Hyp Ref Expression
1 lpival.p ⊢ P = LPIdeal ⁡ R
2 lpival.k ⊢ K = RSpan ⁡ R
3 lpival.b ⊢ B = Base R
4 1 2 3 lpival ⊢ R ∈ Ring → P = ⋃ g ∈ B K ⁡ g
5 4 eleq2d ⊢ R ∈ Ring → I ∈ P ↔ I ∈ ⋃ g ∈ B K ⁡ g
6 eliun ⊢ I ∈ ⋃ g ∈ B K ⁡ g ↔ ∃ g ∈ B I ∈ K ⁡ g
7 fvex ⊢ K ⁡ g ∈ V
8 7 elsn2 ⊢ I ∈ K ⁡ g ↔ I = K ⁡ g
9 8 rexbii ⊢ ∃ g ∈ B I ∈ K ⁡ g ↔ ∃ g ∈ B I = K ⁡ g
10 6 9 bitri ⊢ I ∈ ⋃ g ∈ B K ⁡ g ↔ ∃ g ∈ B I = K ⁡ g
11 5 10 syl6bb ⊢ R ∈ Ring → I ∈ P ↔ ∃ g ∈ B I = K ⁡ g