Metamath Proof Explorer

Theorem lpiss

Description: Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

Ref Expression
Hypotheses lpival.p ⊢ P = LPIdeal ⁡ R
lpiss.u ⊢ U = LIdeal ⁡ R
Assertion lpiss ⊢ R ∈ Ring → P ⊆ U

Proof

Step Hyp Ref Expression
1 lpival.p ⊢ P = LPIdeal ⁡ R
2 lpiss.u ⊢ U = LIdeal ⁡ R
3 eqid ⊢ RSpan ⁡ R = RSpan ⁡ R
4 eqid ⊢ Base R = Base R
5 1 3 4 islpidl ⊢ R ∈ Ring → a ∈ P ↔ ∃ g ∈ Base R a = RSpan ⁡ R ⁡ g
6 snssi ⊢ g ∈ Base R → g ⊆ Base R
7 3 4 2 rspcl ⊢ R ∈ Ring ∧ g ⊆ Base R → RSpan ⁡ R ⁡ g ∈ U
8 6 7 sylan2 ⊢ R ∈ Ring ∧ g ∈ Base R → RSpan ⁡ R ⁡ g ∈ U
9 eleq1 ⊢ a = RSpan ⁡ R ⁡ g → a ∈ U ↔ RSpan ⁡ R ⁡ g ∈ U
10 8 9 syl5ibrcom ⊢ R ∈ Ring ∧ g ∈ Base R → a = RSpan ⁡ R ⁡ g → a ∈ U
11 10 rexlimdva ⊢ R ∈ Ring → ∃ g ∈ Base R a = RSpan ⁡ R ⁡ g → a ∈ U
12 5 11 sylbid ⊢ R ∈ Ring → a ∈ P → a ∈ U
13 12 ssrdv ⊢ R ∈ Ring → P ⊆ U