Metamath Proof Explorer

Theorem islnr3

Description: Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypotheses islnr3.b 
|- B = ( Base ` R )
islnr3.u 
|- U = ( LIdeal ` R )
Assertion islnr3 
|- ( R e. LNoeR <-> ( R e. Ring /\ U e. ( NoeACS ` B ) ) )

Proof

Step Hyp Ref Expression
1 islnr3.b 
 |-  B = ( Base ` R )
2 islnr3.u 
 |-  U = ( LIdeal ` R )
3 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
4 1 2 3 islnr2 
 |-  ( R e. LNoeR <-> ( R e. Ring /\ A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( RSpan ` R ) ` y ) ) )
5 eqid 
 |-  ( mrCls ` U ) = ( mrCls ` U )
6 2 3 5 mrcrsp 
 |-  ( R e. Ring -> ( RSpan ` R ) = ( mrCls ` U ) )
7 6 fveq1d 
 |-  ( R e. Ring -> ( ( RSpan ` R ) ` y ) = ( ( mrCls ` U ) ` y ) )
8 7 eqeq2d 
 |-  ( R e. Ring -> ( x = ( ( RSpan ` R ) ` y ) <-> x = ( ( mrCls ` U ) ` y ) ) )
9 8 rexbidv 
 |-  ( R e. Ring -> ( E. y e. ( ~P B i^i Fin ) x = ( ( RSpan ` R ) ` y ) <-> E. y e. ( ~P B i^i Fin ) x = ( ( mrCls ` U ) ` y ) ) )
10 9 ralbidv 
 |-  ( R e. Ring -> ( A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( RSpan ` R ) ` y ) <-> A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( mrCls ` U ) ` y ) ) )
11 1 2 lidlacs 
 |-  ( R e. Ring -> U e. ( ACS ` B ) )
12 11 biantrurd 
 |-  ( R e. Ring -> ( A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( mrCls ` U ) ` y ) <-> ( U e. ( ACS ` B ) /\ A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( mrCls ` U ) ` y ) ) ) )
13 10 12 bitrd 
 |-  ( R e. Ring -> ( A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( RSpan ` R ) ` y ) <-> ( U e. ( ACS ` B ) /\ A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( mrCls ` U ) ` y ) ) ) )
14 5 isnacs 
 |-  ( U e. ( NoeACS ` B ) <-> ( U e. ( ACS ` B ) /\ A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( mrCls ` U ) ` y ) ) )
15 13 14 bitr4di 
 |-  ( R e. Ring -> ( A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( RSpan ` R ) ` y ) <-> U e. ( NoeACS ` B ) ) )
16 15 pm5.32i 
 |-  ( ( R e. Ring /\ A. x e. U E. y e. ( ~P B i^i Fin ) x = ( ( RSpan ` R ) ` y ) ) <-> ( R e. Ring /\ U e. ( NoeACS ` B ) ) )
17 4 16 bitri 
 |-  ( R e. LNoeR <-> ( R e. Ring /\ U e. ( NoeACS ` B ) ) )