Metamath Proof Explorer

Theorem hbt

Description: The Hilbert Basis Theorem - the ring of univariate polynomials over a Noetherian ring is a Noetherian ring. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypothesis hbt.p 
|- P = ( Poly1 ` R )
Assertion hbt 
|- ( R e. LNoeR -> P e. LNoeR )

Proof

Step Hyp Ref Expression
1 hbt.p 
 |-  P = ( Poly1 ` R )
2 lnrring 
 |-  ( R e. LNoeR -> R e. Ring )
3 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
4 2 3 syl 
 |-  ( R e. LNoeR -> P e. Ring )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
7 5 6 islnr3 
 |-  ( R e. LNoeR <-> ( R e. Ring /\ ( LIdeal ` R ) e. ( NoeACS ` ( Base ` R ) ) ) )
8 7 simprbi 
 |-  ( R e. LNoeR -> ( LIdeal ` R ) e. ( NoeACS ` ( Base ` R ) ) )
9 8 adantr 
 |-  ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) -> ( LIdeal ` R ) e. ( NoeACS ` ( Base ` R ) ) )
10 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
11 eqid 
 |-  ( ldgIdlSeq ` R ) = ( ldgIdlSeq ` R )
12 1 10 11 6 hbtlem7 
 |-  ( ( R e. Ring /\ a e. ( LIdeal ` P ) ) -> ( ( ldgIdlSeq ` R ) ` a ) : NN0 --> ( LIdeal ` R ) )
13 2 12 sylan 
 |-  ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) -> ( ( ldgIdlSeq ` R ) ` a ) : NN0 --> ( LIdeal ` R ) )
14 2 ad2antrr 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ b e. NN0 ) -> R e. Ring )
15 simplr 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ b e. NN0 ) -> a e. ( LIdeal ` P ) )
16 simpr 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ b e. NN0 ) -> b e. NN0 )
17 peano2nn0 
 |-  ( b e. NN0 -> ( b + 1 ) e. NN0 )
18 17 adantl 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ b e. NN0 ) -> ( b + 1 ) e. NN0 )
19 nn0re 
 |-  ( b e. NN0 -> b e. RR )
20 19 lep1d 
 |-  ( b e. NN0 -> b <_ ( b + 1 ) )
21 20 adantl 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ b e. NN0 ) -> b <_ ( b + 1 ) )
22 1 10 11 14 15 16 18 21 hbtlem4 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ b e. NN0 ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` b ) C_ ( ( ( ldgIdlSeq ` R ) ` a ) ` ( b + 1 ) ) )
23 22 ralrimiva 
 |-  ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) -> A. b e. NN0 ( ( ( ldgIdlSeq ` R ) ` a ) ` b ) C_ ( ( ( ldgIdlSeq ` R ) ` a ) ` ( b + 1 ) ) )
24 nacsfix 
 |-  ( ( ( LIdeal ` R ) e. ( NoeACS ` ( Base ` R ) ) /\ ( ( ldgIdlSeq ` R ) ` a ) : NN0 --> ( LIdeal ` R ) /\ A. b e. NN0 ( ( ( ldgIdlSeq ` R ) ` a ) ` b ) C_ ( ( ( ldgIdlSeq ` R ) ` a ) ` ( b + 1 ) ) ) -> E. c e. NN0 A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) )
25 9 13 23 24 syl3anc 
 |-  ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) -> E. c e. NN0 A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) )
26 fzfi 
 |-  ( 0 ... c ) e. Fin
27 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
28 simpll 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ e e. ( 0 ... c ) ) -> R e. LNoeR )
29 simplr 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ e e. ( 0 ... c ) ) -> a e. ( LIdeal ` P ) )
30 elfznn0 
 |-  ( e e. ( 0 ... c ) -> e e. NN0 )
31 30 adantl 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ e e. ( 0 ... c ) ) -> e e. NN0 )
32 1 10 11 27 28 29 31 hbtlem6 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ e e. ( 0 ... c ) ) -> E. b e. ( ~P a i^i Fin ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` b ) ) ` e ) )
33 32 ralrimiva 
 |-  ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) -> A. e e. ( 0 ... c ) E. b e. ( ~P a i^i Fin ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` b ) ) ` e ) )
34 2fveq3 
 |-  ( b = ( f ` e ) -> ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` b ) ) = ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) )
35 34 fveq1d 
 |-  ( b = ( f ` e ) -> ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` b ) ) ` e ) = ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) )
36 35 sseq2d 
 |-  ( b = ( f ` e ) -> ( ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` b ) ) ` e ) <-> ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) )
37 36 ac6sfi 
 |-  ( ( ( 0 ... c ) e. Fin /\ A. e e. ( 0 ... c ) E. b e. ( ~P a i^i Fin ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` b ) ) ` e ) ) -> E. f ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) )
38 26 33 37 sylancr 
 |-  ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) -> E. f ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) )
39 38 adantr 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) -> E. f ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) )
40 frn 
 |-  ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) -> ran f C_ ( ~P a i^i Fin ) )
41 40 ad2antrl 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ran f C_ ( ~P a i^i Fin ) )
42 inss1 
 |-  ( ~P a i^i Fin ) C_ ~P a
43 41 42 sstrdi 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ran f C_ ~P a )
44 43 unissd 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U. ran f C_ U. ~P a )
45 unipw 
 |-  U. ~P a = a
46 44 45 sseqtrdi 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U. ran f C_ a )
47 simpllr 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> a e. ( LIdeal ` P ) )
48 eqid 
 |-  ( Base ` P ) = ( Base ` P )
49 48 10 lidlss 
 |-  ( a e. ( LIdeal ` P ) -> a C_ ( Base ` P ) )
50 47 49 syl 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> a C_ ( Base ` P ) )
51 46 50 sstrd 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U. ran f C_ ( Base ` P ) )
52 fvex 
 |-  ( Base ` P ) e. _V
53 52 elpw2 
 |-  ( U. ran f e. ~P ( Base ` P ) <-> U. ran f C_ ( Base ` P ) )
54 51 53 sylibr 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U. ran f e. ~P ( Base ` P ) )
55 simprl 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> f : ( 0 ... c ) --> ( ~P a i^i Fin ) )
56 ffn 
 |-  ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) -> f Fn ( 0 ... c ) )
57 fniunfv 
 |-  ( f Fn ( 0 ... c ) -> U_ g e. ( 0 ... c ) ( f ` g ) = U. ran f )
58 55 56 57 3syl 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U_ g e. ( 0 ... c ) ( f ` g ) = U. ran f )
59 inss2 
 |-  ( ~P a i^i Fin ) C_ Fin
60 55 ffvelrnda 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. ( 0 ... c ) ) -> ( f ` g ) e. ( ~P a i^i Fin ) )
61 59 60 sseldi 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. ( 0 ... c ) ) -> ( f ` g ) e. Fin )
62 61 ralrimiva 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> A. g e. ( 0 ... c ) ( f ` g ) e. Fin )
63 iunfi 
 |-  ( ( ( 0 ... c ) e. Fin /\ A. g e. ( 0 ... c ) ( f ` g ) e. Fin ) -> U_ g e. ( 0 ... c ) ( f ` g ) e. Fin )
64 26 62 63 sylancr 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U_ g e. ( 0 ... c ) ( f ` g ) e. Fin )
65 58 64 eqeltrrd 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U. ran f e. Fin )
66 54 65 elind 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U. ran f e. ( ~P ( Base ` P ) i^i Fin ) )
67 2 ad3antrrr 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> R e. Ring )
68 4 ad3antrrr 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> P e. Ring )
69 27 48 10 rspcl 
 |-  ( ( P e. Ring /\ U. ran f C_ ( Base ` P ) ) -> ( ( RSpan ` P ) ` U. ran f ) e. ( LIdeal ` P ) )
70 68 51 69 syl2anc 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ( ( RSpan ` P ) ` U. ran f ) e. ( LIdeal ` P ) )
71 27 10 rspssp 
 |-  ( ( P e. Ring /\ a e. ( LIdeal ` P ) /\ U. ran f C_ a ) -> ( ( RSpan ` P ) ` U. ran f ) C_ a )
72 68 47 46 71 syl3anc 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ( ( RSpan ` P ) ` U. ran f ) C_ a )
73 nn0re 
 |-  ( g e. NN0 -> g e. RR )
74 73 adantl 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. NN0 ) -> g e. RR )
75 simplrl 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> c e. NN0 )
76 75 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. NN0 ) -> c e. NN0 )
77 76 nn0red 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. NN0 ) -> c e. RR )
78 simprl 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> g e. NN0 )
79 simprr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> g <_ c )
80 75 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> c e. NN0 )
81 fznn0 
 |-  ( c e. NN0 -> ( g e. ( 0 ... c ) <-> ( g e. NN0 /\ g <_ c ) ) )
82 80 81 syl 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( g e. ( 0 ... c ) <-> ( g e. NN0 /\ g <_ c ) ) )
83 78 79 82 mpbir2and 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> g e. ( 0 ... c ) )
84 simplrr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) )
85 fveq2 
 |-  ( e = g -> ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) )
86 2fveq3 
 |-  ( e = g -> ( ( RSpan ` P ) ` ( f ` e ) ) = ( ( RSpan ` P ) ` ( f ` g ) ) )
87 86 fveq2d 
 |-  ( e = g -> ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) = ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` g ) ) ) )
88 id 
 |-  ( e = g -> e = g )
89 87 88 fveq12d 
 |-  ( e = g -> ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) = ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` g ) ) ) ` g ) )
90 85 89 sseq12d 
 |-  ( e = g -> ( ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) <-> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` g ) ) ) ` g ) ) )
91 90 rspcva 
 |-  ( ( g e. ( 0 ... c ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` g ) ) ) ` g ) )
92 83 84 91 syl2anc 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` g ) ) ) ` g ) )
93 67 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> R e. Ring )
94 fvssunirn 
 |-  ( f ` g ) C_ U. ran f
95 94 51 sstrid 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ( f ` g ) C_ ( Base ` P ) )
96 27 48 10 rspcl 
 |-  ( ( P e. Ring /\ ( f ` g ) C_ ( Base ` P ) ) -> ( ( RSpan ` P ) ` ( f ` g ) ) e. ( LIdeal ` P ) )
97 68 95 96 syl2anc 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ( ( RSpan ` P ) ` ( f ` g ) ) e. ( LIdeal ` P ) )
98 97 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( ( RSpan ` P ) ` ( f ` g ) ) e. ( LIdeal ` P ) )
99 70 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( ( RSpan ` P ) ` U. ran f ) e. ( LIdeal ` P ) )
100 67 3 syl 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> P e. Ring )
101 100 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> P e. Ring )
102 27 48 rspssid 
 |-  ( ( P e. Ring /\ U. ran f C_ ( Base ` P ) ) -> U. ran f C_ ( ( RSpan ` P ) ` U. ran f ) )
103 68 51 102 syl2anc 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> U. ran f C_ ( ( RSpan ` P ) ` U. ran f ) )
104 103 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> U. ran f C_ ( ( RSpan ` P ) ` U. ran f ) )
105 94 104 sstrid 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( f ` g ) C_ ( ( RSpan ` P ) ` U. ran f ) )
106 27 10 rspssp 
 |-  ( ( P e. Ring /\ ( ( RSpan ` P ) ` U. ran f ) e. ( LIdeal ` P ) /\ ( f ` g ) C_ ( ( RSpan ` P ) ` U. ran f ) ) -> ( ( RSpan ` P ) ` ( f ` g ) ) C_ ( ( RSpan ` P ) ` U. ran f ) )
107 101 99 105 106 syl3anc 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( ( RSpan ` P ) ` ( f ` g ) ) C_ ( ( RSpan ` P ) ` U. ran f ) )
108 1 10 11 93 98 99 107 78 hbtlem3 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` g ) ) ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
109 92 108 sstrd 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ g <_ c ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
110 109 anassrs 
 |-  ( ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. NN0 ) /\ g <_ c ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
111 nn0z 
 |-  ( c e. NN0 -> c e. ZZ )
112 111 adantr 
 |-  ( ( c e. NN0 /\ ( g e. NN0 /\ c <_ g ) ) -> c e. ZZ )
113 nn0z 
 |-  ( g e. NN0 -> g e. ZZ )
114 113 ad2antrl 
 |-  ( ( c e. NN0 /\ ( g e. NN0 /\ c <_ g ) ) -> g e. ZZ )
115 simprr 
 |-  ( ( c e. NN0 /\ ( g e. NN0 /\ c <_ g ) ) -> c <_ g )
116 eluz2 
 |-  ( g e. ( ZZ>= ` c ) <-> ( c e. ZZ /\ g e. ZZ /\ c <_ g ) )
117 112 114 115 116 syl3anbrc 
 |-  ( ( c e. NN0 /\ ( g e. NN0 /\ c <_ g ) ) -> g e. ( ZZ>= ` c ) )
118 75 117 sylan 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> g e. ( ZZ>= ` c ) )
119 simprr 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) -> A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) )
120 119 ad2antrr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) )
121 fveqeq2 
 |-  ( d = g -> ( ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) <-> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) )
122 121 rspcva 
 |-  ( ( g e. ( ZZ>= ` c ) /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) )
123 118 120 122 syl2anc 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) )
124 75 nn0red 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> c e. RR )
125 124 leidd 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> c <_ c )
126 109 expr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. NN0 ) -> ( g <_ c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) ) )
127 126 ralrimiva 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> A. g e. NN0 ( g <_ c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) ) )
128 breq1 
 |-  ( g = c -> ( g <_ c <-> c <_ c ) )
129 fveq2 
 |-  ( g = c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) )
130 fveq2 
 |-  ( g = c -> ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) = ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) )
131 129 130 sseq12d 
 |-  ( g = c -> ( ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) <-> ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) ) )
132 128 131 imbi12d 
 |-  ( g = c -> ( ( g <_ c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) ) <-> ( c <_ c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) ) ) )
133 132 rspcva 
 |-  ( ( c e. NN0 /\ A. g e. NN0 ( g <_ c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) ) ) -> ( c <_ c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) ) )
134 75 127 133 syl2anc 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ( c <_ c -> ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) ) )
135 125 134 mpd 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) )
136 135 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) )
137 67 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> R e. Ring )
138 70 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> ( ( RSpan ` P ) ` U. ran f ) e. ( LIdeal ` P ) )
139 75 adantr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> c e. NN0 )
140 simprl 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> g e. NN0 )
141 simprr 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> c <_ g )
142 1 10 11 137 138 139 140 141 hbtlem4 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
143 136 142 sstrd 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
144 123 143 eqsstrd 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ ( g e. NN0 /\ c <_ g ) ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
145 144 anassrs 
 |-  ( ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. NN0 ) /\ c <_ g ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
146 74 77 110 145 lecasei 
 |-  ( ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) /\ g e. NN0 ) -> ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
147 146 ralrimiva 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> A. g e. NN0 ( ( ( ldgIdlSeq ` R ) ` a ) ` g ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` U. ran f ) ) ` g ) )
148 1 10 11 67 70 47 72 147 hbtlem5 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> ( ( RSpan ` P ) ` U. ran f ) = a )
149 148 eqcomd 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> a = ( ( RSpan ` P ) ` U. ran f ) )
150 fveq2 
 |-  ( b = U. ran f -> ( ( RSpan ` P ) ` b ) = ( ( RSpan ` P ) ` U. ran f ) )
151 150 rspceeqv 
 |-  ( ( U. ran f e. ( ~P ( Base ` P ) i^i Fin ) /\ a = ( ( RSpan ` P ) ` U. ran f ) ) -> E. b e. ( ~P ( Base ` P ) i^i Fin ) a = ( ( RSpan ` P ) ` b ) )
152 66 149 151 syl2anc 
 |-  ( ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) /\ ( f : ( 0 ... c ) --> ( ~P a i^i Fin ) /\ A. e e. ( 0 ... c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` e ) C_ ( ( ( ldgIdlSeq ` R ) ` ( ( RSpan ` P ) ` ( f ` e ) ) ) ` e ) ) ) -> E. b e. ( ~P ( Base ` P ) i^i Fin ) a = ( ( RSpan ` P ) ` b ) )
153 39 152 exlimddv 
 |-  ( ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) /\ ( c e. NN0 /\ A. d e. ( ZZ>= ` c ) ( ( ( ldgIdlSeq ` R ) ` a ) ` d ) = ( ( ( ldgIdlSeq ` R ) ` a ) ` c ) ) ) -> E. b e. ( ~P ( Base ` P ) i^i Fin ) a = ( ( RSpan ` P ) ` b ) )
154 25 153 rexlimddv 
 |-  ( ( R e. LNoeR /\ a e. ( LIdeal ` P ) ) -> E. b e. ( ~P ( Base ` P ) i^i Fin ) a = ( ( RSpan ` P ) ` b ) )
155 154 ralrimiva 
 |-  ( R e. LNoeR -> A. a e. ( LIdeal ` P ) E. b e. ( ~P ( Base ` P ) i^i Fin ) a = ( ( RSpan ` P ) ` b ) )
156 48 10 27 islnr2 
 |-  ( P e. LNoeR <-> ( P e. Ring /\ A. a e. ( LIdeal ` P ) E. b e. ( ~P ( Base ` P ) i^i Fin ) a = ( ( RSpan ` P ) ` b ) ) )
157 4 155 156 sylanbrc 
 |-  ( R e. LNoeR -> P e. LNoeR )