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