Metamath Proof Explorer

Theorem lnr2i

Description: Given an ideal in a left-Noetherian ring, there is a finite subset which generates it. (Contributed by Stefan O'Rear, 31-Mar-2015)

Ref Expression
Hypotheses lnr2i.u 
|- U = ( LIdeal ` R )
lnr2i.n 
|- N = ( RSpan ` R )
Assertion lnr2i 
|- ( ( R e. LNoeR /\ I e. U ) -> E. g e. ( ~P I i^i Fin ) I = ( N ` g ) )

Proof

Step Hyp Ref Expression
1 lnr2i.u 
 |-  U = ( LIdeal ` R )
2 lnr2i.n 
 |-  N = ( RSpan ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 1 2 islnr2 
 |-  ( R e. LNoeR <-> ( R e. Ring /\ A. i e. U E. g e. ( ~P ( Base ` R ) i^i Fin ) i = ( N ` g ) ) )
5 4 simprbi 
 |-  ( R e. LNoeR -> A. i e. U E. g e. ( ~P ( Base ` R ) i^i Fin ) i = ( N ` g ) )
6 eqeq1 
 |-  ( i = I -> ( i = ( N ` g ) <-> I = ( N ` g ) ) )
7 6 rexbidv 
 |-  ( i = I -> ( E. g e. ( ~P ( Base ` R ) i^i Fin ) i = ( N ` g ) <-> E. g e. ( ~P ( Base ` R ) i^i Fin ) I = ( N ` g ) ) )
8 7 rspcva 
 |-  ( ( I e. U /\ A. i e. U E. g e. ( ~P ( Base ` R ) i^i Fin ) i = ( N ` g ) ) -> E. g e. ( ~P ( Base ` R ) i^i Fin ) I = ( N ` g ) )
9 5 8 sylan2 
 |-  ( ( I e. U /\ R e. LNoeR ) -> E. g e. ( ~P ( Base ` R ) i^i Fin ) I = ( N ` g ) )
10 9 ancoms 
 |-  ( ( R e. LNoeR /\ I e. U ) -> E. g e. ( ~P ( Base ` R ) i^i Fin ) I = ( N ` g ) )
11 lnrring 
 |-  ( R e. LNoeR -> R e. Ring )
12 2 3 rspssid 
 |-  ( ( R e. Ring /\ g C_ ( Base ` R ) ) -> g C_ ( N ` g ) )
13 11 12 sylan 
 |-  ( ( R e. LNoeR /\ g C_ ( Base ` R ) ) -> g C_ ( N ` g ) )
14 13 ex 
 |-  ( R e. LNoeR -> ( g C_ ( Base ` R ) -> g C_ ( N ` g ) ) )
15 vex 
 |-  g e. _V
16 15 elpw 
 |-  ( g e. ~P ( Base ` R ) <-> g C_ ( Base ` R ) )
17 15 elpw 
 |-  ( g e. ~P ( N ` g ) <-> g C_ ( N ` g ) )
18 14 16 17 3imtr4g 
 |-  ( R e. LNoeR -> ( g e. ~P ( Base ` R ) -> g e. ~P ( N ` g ) ) )
19 18 anim1d 
 |-  ( R e. LNoeR -> ( ( g e. ~P ( Base ` R ) /\ g e. Fin ) -> ( g e. ~P ( N ` g ) /\ g e. Fin ) ) )
20 elin 
 |-  ( g e. ( ~P ( Base ` R ) i^i Fin ) <-> ( g e. ~P ( Base ` R ) /\ g e. Fin ) )
21 elin 
 |-  ( g e. ( ~P ( N ` g ) i^i Fin ) <-> ( g e. ~P ( N ` g ) /\ g e. Fin ) )
22 19 20 21 3imtr4g 
 |-  ( R e. LNoeR -> ( g e. ( ~P ( Base ` R ) i^i Fin ) -> g e. ( ~P ( N ` g ) i^i Fin ) ) )
23 pweq 
 |-  ( I = ( N ` g ) -> ~P I = ~P ( N ` g ) )
24 23 ineq1d 
 |-  ( I = ( N ` g ) -> ( ~P I i^i Fin ) = ( ~P ( N ` g ) i^i Fin ) )
25 24 eleq2d 
 |-  ( I = ( N ` g ) -> ( g e. ( ~P I i^i Fin ) <-> g e. ( ~P ( N ` g ) i^i Fin ) ) )
26 25 imbi2d 
 |-  ( I = ( N ` g ) -> ( ( g e. ( ~P ( Base ` R ) i^i Fin ) -> g e. ( ~P I i^i Fin ) ) <-> ( g e. ( ~P ( Base ` R ) i^i Fin ) -> g e. ( ~P ( N ` g ) i^i Fin ) ) ) )
27 22 26 syl5ibrcom 
 |-  ( R e. LNoeR -> ( I = ( N ` g ) -> ( g e. ( ~P ( Base ` R ) i^i Fin ) -> g e. ( ~P I i^i Fin ) ) ) )
28 27 imdistand 
 |-  ( R e. LNoeR -> ( ( I = ( N ` g ) /\ g e. ( ~P ( Base ` R ) i^i Fin ) ) -> ( I = ( N ` g ) /\ g e. ( ~P I i^i Fin ) ) ) )
29 ancom 
 |-  ( ( g e. ( ~P ( Base ` R ) i^i Fin ) /\ I = ( N ` g ) ) <-> ( I = ( N ` g ) /\ g e. ( ~P ( Base ` R ) i^i Fin ) ) )
30 ancom 
 |-  ( ( g e. ( ~P I i^i Fin ) /\ I = ( N ` g ) ) <-> ( I = ( N ` g ) /\ g e. ( ~P I i^i Fin ) ) )
31 28 29 30 3imtr4g 
 |-  ( R e. LNoeR -> ( ( g e. ( ~P ( Base ` R ) i^i Fin ) /\ I = ( N ` g ) ) -> ( g e. ( ~P I i^i Fin ) /\ I = ( N ` g ) ) ) )
32 31 reximdv2 
 |-  ( R e. LNoeR -> ( E. g e. ( ~P ( Base ` R ) i^i Fin ) I = ( N ` g ) -> E. g e. ( ~P I i^i Fin ) I = ( N ` g ) ) )
33 32 adantr 
 |-  ( ( R e. LNoeR /\ I e. U ) -> ( E. g e. ( ~P ( Base ` R ) i^i Fin ) I = ( N ` g ) -> E. g e. ( ~P I i^i Fin ) I = ( N ` g ) ) )
34 10 33 mpd 
 |-  ( ( R e. LNoeR /\ I e. U ) -> E. g e. ( ~P I i^i Fin ) I = ( N ` g ) )