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

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 e. Ring -> P C_ 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 e. Ring -> ( a e. P <-> E. g e. ( Base ` R ) a = ( ( RSpan ` R ) ` { g } ) ) )
6 snssi 
 |-  ( g e. ( Base ` R ) -> { g } C_ ( Base ` R ) )
7 3 4 2 rspcl 
 |-  ( ( R e. Ring /\ { g } C_ ( Base ` R ) ) -> ( ( RSpan ` R ) ` { g } ) e. U )
8 6 7 sylan2 
 |-  ( ( R e. Ring /\ g e. ( Base ` R ) ) -> ( ( RSpan ` R ) ` { g } ) e. U )
9 eleq1 
 |-  ( a = ( ( RSpan ` R ) ` { g } ) -> ( a e. U <-> ( ( RSpan ` R ) ` { g } ) e. U ) )
10 8 9 syl5ibrcom 
 |-  ( ( R e. Ring /\ g e. ( Base ` R ) ) -> ( a = ( ( RSpan ` R ) ` { g } ) -> a e. U ) )
11 10 rexlimdva 
 |-  ( R e. Ring -> ( E. g e. ( Base ` R ) a = ( ( RSpan ` R ) ` { g } ) -> a e. U ) )
12 5 11 sylbid 
 |-  ( R e. Ring -> ( a e. P -> a e. U ) )
13 12 ssrdv 
 |-  ( R e. Ring -> P C_ U )