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 sselid ⊢ ( ( ( ( ( 𝑅 ∈ 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 )