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 𝑃 = ( Poly1𝑅 )
Assertion hbt ( 𝑅 ∈ LNoeR → 𝑃 ∈ LNoeR )

Proof

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