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 ) |