Metamath Proof Explorer

Theorem lpirlnr

Description: Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion lpirlnr 
|- ( R e. LPIR -> R e. LNoeR )

Proof

Step Hyp Ref Expression
1 lpirring 
 |-  ( R e. LPIR -> R e. Ring )
2 eqid 
 |-  ( LPIdeal ` R ) = ( LPIdeal ` R )
3 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 2 3 4 islpidl 
 |-  ( R e. Ring -> ( a e. ( LPIdeal ` R ) <-> E. c e. ( Base ` R ) a = ( ( RSpan ` R ) ` { c } ) ) )
6 1 5 syl 
 |-  ( R e. LPIR -> ( a e. ( LPIdeal ` R ) <-> E. c e. ( Base ` R ) a = ( ( RSpan ` R ) ` { c } ) ) )
7 6 biimpa 
 |-  ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) -> E. c e. ( Base ` R ) a = ( ( RSpan ` R ) ` { c } ) )
8 snelpwi 
 |-  ( c e. ( Base ` R ) -> { c } e. ~P ( Base ` R ) )
9 8 adantl 
 |-  ( ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) /\ c e. ( Base ` R ) ) -> { c } e. ~P ( Base ` R ) )
10 snfi 
 |-  { c } e. Fin
11 10 a1i 
 |-  ( ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) /\ c e. ( Base ` R ) ) -> { c } e. Fin )
12 9 11 elind 
 |-  ( ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) /\ c e. ( Base ` R ) ) -> { c } e. ( ~P ( Base ` R ) i^i Fin ) )
13 eqid 
 |-  ( ( RSpan ` R ) ` { c } ) = ( ( RSpan ` R ) ` { c } )
14 fveq2 
 |-  ( b = { c } -> ( ( RSpan ` R ) ` b ) = ( ( RSpan ` R ) ` { c } ) )
15 14 rspceeqv 
 |-  ( ( { c } e. ( ~P ( Base ` R ) i^i Fin ) /\ ( ( RSpan ` R ) ` { c } ) = ( ( RSpan ` R ) ` { c } ) ) -> E. b e. ( ~P ( Base ` R ) i^i Fin ) ( ( RSpan ` R ) ` { c } ) = ( ( RSpan ` R ) ` b ) )
16 12 13 15 sylancl 
 |-  ( ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) /\ c e. ( Base ` R ) ) -> E. b e. ( ~P ( Base ` R ) i^i Fin ) ( ( RSpan ` R ) ` { c } ) = ( ( RSpan ` R ) ` b ) )
17 eqeq1 
 |-  ( a = ( ( RSpan ` R ) ` { c } ) -> ( a = ( ( RSpan ` R ) ` b ) <-> ( ( RSpan ` R ) ` { c } ) = ( ( RSpan ` R ) ` b ) ) )
18 17 rexbidv 
 |-  ( a = ( ( RSpan ` R ) ` { c } ) -> ( E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) <-> E. b e. ( ~P ( Base ` R ) i^i Fin ) ( ( RSpan ` R ) ` { c } ) = ( ( RSpan ` R ) ` b ) ) )
19 16 18 syl5ibrcom 
 |-  ( ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) /\ c e. ( Base ` R ) ) -> ( a = ( ( RSpan ` R ) ` { c } ) -> E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) ) )
20 19 rexlimdva 
 |-  ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) -> ( E. c e. ( Base ` R ) a = ( ( RSpan ` R ) ` { c } ) -> E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) ) )
21 7 20 mpd 
 |-  ( ( R e. LPIR /\ a e. ( LPIdeal ` R ) ) -> E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) )
22 21 ralrimiva 
 |-  ( R e. LPIR -> A. a e. ( LPIdeal ` R ) E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) )
23 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
24 2 23 islpir 
 |-  ( R e. LPIR <-> ( R e. Ring /\ ( LIdeal ` R ) = ( LPIdeal ` R ) ) )
25 24 simprbi 
 |-  ( R e. LPIR -> ( LIdeal ` R ) = ( LPIdeal ` R ) )
26 25 raleqdv 
 |-  ( R e. LPIR -> ( A. a e. ( LIdeal ` R ) E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) <-> A. a e. ( LPIdeal ` R ) E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) ) )
27 22 26 mpbird 
 |-  ( R e. LPIR -> A. a e. ( LIdeal ` R ) E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) )
28 4 23 3 islnr2 
 |-  ( R e. LNoeR <-> ( R e. Ring /\ A. a e. ( LIdeal ` R ) E. b e. ( ~P ( Base ` R ) i^i Fin ) a = ( ( RSpan ` R ) ` b ) ) )
29 1 27 28 sylanbrc 
 |-  ( R e. LPIR -> R e. LNoeR )