Step | Hyp | Ref
| Expression |
1 | | lnrring 36701 |
. . 3
⊢ (𝑅 ∈ LNoeR → 𝑅 ∈ Ring) |
2 | | hbt.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
3 | 2 | ply1ring 19439 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
4 | 1, 3 | syl 17 |
. 2
⊢ (𝑅 ∈ LNoeR → 𝑃 ∈ Ring) |
5 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | | eqid 2610 |
. . . . . . . 8
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
7 | 5, 6 | islnr3 36704 |
. . . . . . 7
⊢ (𝑅 ∈ LNoeR ↔ (𝑅 ∈ Ring ∧
(LIdeal‘𝑅) ∈
(NoeACS‘(Base‘𝑅)))) |
8 | 7 | simprbi 479 |
. . . . . 6
⊢ (𝑅 ∈ LNoeR →
(LIdeal‘𝑅) ∈
(NoeACS‘(Base‘𝑅))) |
9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → (LIdeal‘𝑅) ∈
(NoeACS‘(Base‘𝑅))) |
10 | | eqid 2610 |
. . . . . . 7
⊢
(LIdeal‘𝑃) =
(LIdeal‘𝑃) |
11 | | eqid 2610 |
. . . . . . 7
⊢
(ldgIdlSeq‘𝑅)
= (ldgIdlSeq‘𝑅) |
12 | 2, 10, 11, 6 | hbtlem7 36714 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ (LIdeal‘𝑃)) →
((ldgIdlSeq‘𝑅)‘𝑎):ℕ0⟶(LIdeal‘𝑅)) |
13 | 1, 12 | sylan 487 |
. . . . 5
⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) →
((ldgIdlSeq‘𝑅)‘𝑎):ℕ0⟶(LIdeal‘𝑅)) |
14 | 1 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑅 ∈ Ring) |
15 | | simplr 788 |
. . . . . . 7
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑎 ∈ (LIdeal‘𝑃)) |
16 | | simpr 476 |
. . . . . . 7
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑏 ∈
ℕ0) |
17 | | peano2nn0 11210 |
. . . . . . . 8
⊢ (𝑏 ∈ ℕ0
→ (𝑏 + 1) ∈
ℕ0) |
18 | 17 | adantl 481 |
. . . . . . 7
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → (𝑏 + 1) ∈
ℕ0) |
19 | | nn0re 11178 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℝ) |
20 | 19 | lep1d 10834 |
. . . . . . . 8
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ≤ (𝑏 + 1)) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) → 𝑏 ≤ (𝑏 + 1)) |
22 | 2, 10, 11, 14, 15, 16, 18, 21 | hbtlem4 36715 |
. . . . . 6
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑏 ∈ ℕ0) →
(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1))) |
23 | 22 | ralrimiva 2949 |
. . . . 5
⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∀𝑏 ∈ ℕ0
(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1))) |
24 | | nacsfix 36293 |
. . . . 5
⊢
(((LIdeal‘𝑅)
∈ (NoeACS‘(Base‘𝑅)) ∧ ((ldgIdlSeq‘𝑅)‘𝑎):ℕ0⟶(LIdeal‘𝑅) ∧ ∀𝑏 ∈ ℕ0
(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑏) ⊆ (((ldgIdlSeq‘𝑅)‘𝑎)‘(𝑏 + 1))) → ∃𝑐 ∈ ℕ0 ∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) |
25 | 9, 13, 23, 24 | syl3anc 1318 |
. . . 4
⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑐 ∈ ℕ0
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) |
26 | | fzfi 12633 |
. . . . . . 7
⊢
(0...𝑐) ∈
Fin |
27 | | eqid 2610 |
. . . . . . . . 9
⊢
(RSpan‘𝑃) =
(RSpan‘𝑃) |
28 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑅 ∈ LNoeR) |
29 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑎 ∈ (LIdeal‘𝑃)) |
30 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (0...𝑐) → 𝑒 ∈ ℕ0) |
31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → 𝑒 ∈ ℕ0) |
32 | 2, 10, 11, 27, 28, 29, 31 | hbtlem6 36718 |
. . . . . . . 8
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ 𝑒 ∈ (0...𝑐)) → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒)) |
33 | 32 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∀𝑒 ∈ (0...𝑐)∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒)) |
34 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑓‘𝑒) → ((RSpan‘𝑃)‘𝑏) = ((RSpan‘𝑃)‘(𝑓‘𝑒))) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑓‘𝑒) → ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏)) = ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))) |
36 | 35 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑏 = (𝑓‘𝑒) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)) |
37 | 36 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝑏 = (𝑓‘𝑒) → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) |
38 | 37 | ac6sfi 8089 |
. . . . . . 7
⊢
(((0...𝑐) ∈ Fin
∧ ∀𝑒 ∈
(0...𝑐)∃𝑏 ∈ (𝒫 𝑎 ∩
Fin)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘𝑏))‘𝑒)) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) |
39 | 26, 33, 38 | sylancr 694 |
. . . . . 6
⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) |
40 | 39 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∃𝑓(𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) |
41 | | frn 5966 |
. . . . . . . . . . . . 13
⊢ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝑎 ∩ Fin)) |
42 | 41 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ran 𝑓 ⊆ (𝒫 𝑎 ∩ Fin)) |
43 | | inss1 3795 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑎 ∩
Fin) ⊆ 𝒫 𝑎 |
44 | 42, 43 | syl6ss 3580 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ran 𝑓 ⊆ 𝒫 𝑎) |
45 | 44 | unissd 4398 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran
𝑓 ⊆ ∪ 𝒫 𝑎) |
46 | | unipw 4845 |
. . . . . . . . . 10
⊢ ∪ 𝒫 𝑎 = 𝑎 |
47 | 45, 46 | syl6sseq 3614 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran
𝑓 ⊆ 𝑎) |
48 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑎 ∈ (LIdeal‘𝑃)) |
49 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘𝑃) |
50 | 49, 10 | lidlss 19031 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (LIdeal‘𝑃) → 𝑎 ⊆ (Base‘𝑃)) |
51 | 48, 50 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑎 ⊆ (Base‘𝑃)) |
52 | 47, 51 | sstrd 3578 |
. . . . . . . 8
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran
𝑓 ⊆ (Base‘𝑃)) |
53 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑃)
∈ V |
54 | 53 | elpw2 4755 |
. . . . . . . 8
⊢ (∪ ran 𝑓 ∈ 𝒫 (Base‘𝑃) ↔ ∪ ran 𝑓 ⊆ (Base‘𝑃)) |
55 | 52, 54 | sylibr 223 |
. . . . . . 7
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran
𝑓 ∈ 𝒫
(Base‘𝑃)) |
56 | | simprl 790 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin)) |
57 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) → 𝑓 Fn (0...𝑐)) |
58 | | fniunfv 6409 |
. . . . . . . . 9
⊢ (𝑓 Fn (0...𝑐) → ∪
𝑔 ∈ (0...𝑐)(𝑓‘𝑔) = ∪ ran 𝑓) |
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . 8
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ 𝑔 ∈ (0...𝑐)(𝑓‘𝑔) = ∪ ran 𝑓) |
60 | | inss2 3796 |
. . . . . . . . . . 11
⊢
(𝒫 𝑎 ∩
Fin) ⊆ Fin |
61 | 56 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ (0...𝑐)) → (𝑓‘𝑔) ∈ (𝒫 𝑎 ∩ Fin)) |
62 | 60, 61 | sseldi 3566 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ (0...𝑐)) → (𝑓‘𝑔) ∈ Fin) |
63 | 62 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∀𝑔 ∈ (0...𝑐)(𝑓‘𝑔) ∈ Fin) |
64 | | iunfi 8137 |
. . . . . . . . 9
⊢
(((0...𝑐) ∈ Fin
∧ ∀𝑔 ∈
(0...𝑐)(𝑓‘𝑔) ∈ Fin) → ∪ 𝑔 ∈ (0...𝑐)(𝑓‘𝑔) ∈ Fin) |
65 | 26, 63, 64 | sylancr 694 |
. . . . . . . 8
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ 𝑔 ∈ (0...𝑐)(𝑓‘𝑔) ∈ Fin) |
66 | 59, 65 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran
𝑓 ∈
Fin) |
67 | 55, 66 | elind 3760 |
. . . . . 6
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran
𝑓 ∈ (𝒫
(Base‘𝑃) ∩
Fin)) |
68 | 1 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑅 ∈ Ring) |
69 | 4 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑃 ∈ Ring) |
70 | 27, 49, 10 | rspcl 19043 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Ring ∧ ∪ ran 𝑓 ⊆ (Base‘𝑃)) → ((RSpan‘𝑃)‘∪ ran
𝑓) ∈
(LIdeal‘𝑃)) |
71 | 69, 52, 70 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘∪ ran
𝑓) ∈
(LIdeal‘𝑃)) |
72 | 27, 10 | rspssp 19047 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Ring ∧ 𝑎 ∈ (LIdeal‘𝑃) ∧ ∪ ran 𝑓 ⊆ 𝑎) → ((RSpan‘𝑃)‘∪ ran
𝑓) ⊆ 𝑎) |
73 | 69, 48, 47, 72 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘∪ ran
𝑓) ⊆ 𝑎) |
74 | | nn0re 11178 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ ℕ0
→ 𝑔 ∈
ℝ) |
75 | 74 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → 𝑔 ∈
ℝ) |
76 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑐 ∈ ℕ0) |
77 | 76 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → 𝑐 ∈
ℕ0) |
78 | 77 | nn0red 11229 |
. . . . . . . . . 10
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → 𝑐 ∈
ℝ) |
79 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → 𝑔 ∈ ℕ0) |
80 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → 𝑔 ≤ 𝑐) |
81 | 76 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → 𝑐 ∈ ℕ0) |
82 | | fznn0 12301 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ℕ0
→ (𝑔 ∈ (0...𝑐) ↔ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐))) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → (𝑔 ∈ (0...𝑐) ↔ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐))) |
84 | 79, 80, 83 | mpbir2and 959 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → 𝑔 ∈ (0...𝑐)) |
85 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)) |
86 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = 𝑔 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔)) |
87 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝑔 → (𝑓‘𝑒) = (𝑓‘𝑔)) |
88 | 87 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝑔 → ((RSpan‘𝑃)‘(𝑓‘𝑒)) = ((RSpan‘𝑃)‘(𝑓‘𝑔))) |
89 | 88 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑔 → ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒))) = ((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))) |
90 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑔 → 𝑒 = 𝑔) |
91 | 89, 90 | fveq12d 6109 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = 𝑔 → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔)) |
92 | 86, 91 | sseq12d 3597 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = 𝑔 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔))) |
93 | 92 | rspcva 3280 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ (0...𝑐) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔)) |
94 | 84, 85, 93 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔)) |
95 | 68 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → 𝑅 ∈ Ring) |
96 | | fvssunirn 6127 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓‘𝑔) ⊆ ∪ ran
𝑓 |
97 | 96, 52 | syl5ss 3579 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → (𝑓‘𝑔) ⊆ (Base‘𝑃)) |
98 | 27, 49, 10 | rspcl 19043 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Ring ∧ (𝑓‘𝑔) ⊆ (Base‘𝑃)) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ∈ (LIdeal‘𝑃)) |
99 | 69, 97, 98 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ∈ (LIdeal‘𝑃)) |
100 | 99 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ∈ (LIdeal‘𝑃)) |
101 | 71 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → ((RSpan‘𝑃)‘∪ ran
𝑓) ∈
(LIdeal‘𝑃)) |
102 | 68, 3 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑃 ∈ Ring) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → 𝑃 ∈ Ring) |
104 | 27, 49 | rspssid 19044 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Ring ∧ ∪ ran 𝑓 ⊆ (Base‘𝑃)) → ∪ ran
𝑓 ⊆
((RSpan‘𝑃)‘∪ ran
𝑓)) |
105 | 69, 52, 104 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∪ ran
𝑓 ⊆
((RSpan‘𝑃)‘∪ ran
𝑓)) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → ∪ ran
𝑓 ⊆
((RSpan‘𝑃)‘∪ ran
𝑓)) |
107 | 96, 106 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → (𝑓‘𝑔) ⊆ ((RSpan‘𝑃)‘∪ ran
𝑓)) |
108 | 27, 10 | rspssp 19047 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ Ring ∧
((RSpan‘𝑃)‘∪ ran
𝑓) ∈
(LIdeal‘𝑃) ∧
(𝑓‘𝑔) ⊆ ((RSpan‘𝑃)‘∪ ran
𝑓)) →
((RSpan‘𝑃)‘(𝑓‘𝑔)) ⊆ ((RSpan‘𝑃)‘∪ ran
𝑓)) |
109 | 103, 101,
107, 108 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → ((RSpan‘𝑃)‘(𝑓‘𝑔)) ⊆ ((RSpan‘𝑃)‘∪ ran
𝑓)) |
110 | 2, 10, 11, 95, 100, 101, 109, 79 | hbtlem3 36716 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑔)))‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
111 | 94, 110 | sstrd 3578 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑔 ≤ 𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
112 | 111 | anassrs 678 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) ∧ 𝑔 ≤ 𝑐) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
113 | | nn0z 11277 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ ℕ0
→ 𝑐 ∈
ℤ) |
114 | 113 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ ℕ0
∧ (𝑔 ∈
ℕ0 ∧ 𝑐
≤ 𝑔)) → 𝑐 ∈
ℤ) |
115 | | nn0z 11277 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ ℕ0
→ 𝑔 ∈
ℤ) |
116 | 115 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ ℕ0
∧ (𝑔 ∈
ℕ0 ∧ 𝑐
≤ 𝑔)) → 𝑔 ∈
ℤ) |
117 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ ℕ0
∧ (𝑔 ∈
ℕ0 ∧ 𝑐
≤ 𝑔)) → 𝑐 ≤ 𝑔) |
118 | | eluz2 11569 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈
(ℤ≥‘𝑐) ↔ (𝑐 ∈ ℤ ∧ 𝑔 ∈ ℤ ∧ 𝑐 ≤ 𝑔)) |
119 | 114, 116,
117, 118 | syl3anbrc 1239 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ ℕ0
∧ (𝑔 ∈
ℕ0 ∧ 𝑐
≤ 𝑔)) → 𝑔 ∈
(ℤ≥‘𝑐)) |
120 | 76, 119 | sylan 487 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → 𝑔 ∈ (ℤ≥‘𝑐)) |
121 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) |
122 | 121 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) |
123 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = 𝑔 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔)) |
124 | 123 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑔 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) |
125 | 124 | rspcva 3280 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈
(ℤ≥‘𝑐) ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) |
126 | 120, 122,
125 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) |
127 | 76 | nn0red 11229 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑐 ∈ ℝ) |
128 | 127 | leidd 10473 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑐 ≤ 𝑐) |
129 | 111 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) → (𝑔 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))) |
130 | 129 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∀𝑔 ∈ ℕ0 (𝑔 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))) |
131 | | breq1 4586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑐 → (𝑔 ≤ 𝑐 ↔ 𝑐 ≤ 𝑐)) |
132 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐)) |
133 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑐 → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran
𝑓))‘𝑔) = (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐)) |
134 | 132, 133 | sseq12d 3597 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑐 → ((((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔) ↔ (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐))) |
135 | 131, 134 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑐 → ((𝑔 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) ↔ (𝑐 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐)))) |
136 | 135 | rspcva 3280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ ℕ0
∧ ∀𝑔 ∈
ℕ0 (𝑔 ≤
𝑐 →
(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔))) → (𝑐 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐))) |
137 | 76, 130, 136 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → (𝑐 ≤ 𝑐 → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐))) |
138 | 128, 137 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐)) |
139 | 138 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐)) |
140 | 68 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → 𝑅 ∈ Ring) |
141 | 71 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → ((RSpan‘𝑃)‘∪ ran
𝑓) ∈
(LIdeal‘𝑃)) |
142 | 76 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → 𝑐 ∈ ℕ0) |
143 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → 𝑔 ∈ ℕ0) |
144 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → 𝑐 ≤ 𝑔) |
145 | 2, 10, 11, 140, 141, 142, 143, 144 | hbtlem4 36715 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
146 | 139, 145 | sstrd 3578 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
147 | 126, 146 | eqsstrd 3602 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ (𝑔 ∈ ℕ0 ∧ 𝑐 ≤ 𝑔)) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
148 | 147 | anassrs 678 |
. . . . . . . . . 10
⊢
((((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) ∧ 𝑐 ≤ 𝑔) → (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
149 | 75, 78, 112, 148 | lecasei 10022 |
. . . . . . . . 9
⊢
(((((𝑅 ∈ LNoeR
∧ 𝑎 ∈
(LIdeal‘𝑃)) ∧
(𝑐 ∈
ℕ0 ∧ ∀𝑑 ∈ (ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) ∧ 𝑔 ∈ ℕ0) →
(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
150 | 149 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∀𝑔 ∈ ℕ0
(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑔) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘∪ ran 𝑓))‘𝑔)) |
151 | 2, 10, 11, 68, 71, 48, 73, 150 | hbtlem5 36717 |
. . . . . . 7
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ((RSpan‘𝑃)‘∪ ran
𝑓) = 𝑎) |
152 | 151 | eqcomd 2616 |
. . . . . 6
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → 𝑎 = ((RSpan‘𝑃)‘∪ ran
𝑓)) |
153 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑏 = ∪
ran 𝑓 →
((RSpan‘𝑃)‘𝑏) = ((RSpan‘𝑃)‘∪ ran
𝑓)) |
154 | 153 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑏 = ∪
ran 𝑓 → (𝑎 = ((RSpan‘𝑃)‘𝑏) ↔ 𝑎 = ((RSpan‘𝑃)‘∪ ran
𝑓))) |
155 | 154 | rspcev 3282 |
. . . . . 6
⊢ ((∪ ran 𝑓 ∈ (𝒫 (Base‘𝑃) ∩ Fin) ∧ 𝑎 = ((RSpan‘𝑃)‘∪ ran 𝑓)) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏)) |
156 | 67, 152, 155 | syl2anc 691 |
. . . . 5
⊢ ((((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) ∧ (𝑓:(0...𝑐)⟶(𝒫 𝑎 ∩ Fin) ∧ ∀𝑒 ∈ (0...𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑒) ⊆ (((ldgIdlSeq‘𝑅)‘((RSpan‘𝑃)‘(𝑓‘𝑒)))‘𝑒))) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏)) |
157 | 40, 156 | exlimddv 1850 |
. . . 4
⊢ (((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) ∧ (𝑐 ∈ ℕ0 ∧
∀𝑑 ∈
(ℤ≥‘𝑐)(((ldgIdlSeq‘𝑅)‘𝑎)‘𝑑) = (((ldgIdlSeq‘𝑅)‘𝑎)‘𝑐))) → ∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏)) |
158 | 25, 157 | rexlimddv 3017 |
. . 3
⊢ ((𝑅 ∈ LNoeR ∧ 𝑎 ∈ (LIdeal‘𝑃)) → ∃𝑏 ∈ (𝒫
(Base‘𝑃) ∩
Fin)𝑎 = ((RSpan‘𝑃)‘𝑏)) |
159 | 158 | ralrimiva 2949 |
. 2
⊢ (𝑅 ∈ LNoeR →
∀𝑎 ∈
(LIdeal‘𝑃)∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏)) |
160 | 49, 10, 27 | islnr2 36703 |
. 2
⊢ (𝑃 ∈ LNoeR ↔ (𝑃 ∈ Ring ∧ ∀𝑎 ∈ (LIdeal‘𝑃)∃𝑏 ∈ (𝒫 (Base‘𝑃) ∩ Fin)𝑎 = ((RSpan‘𝑃)‘𝑏))) |
161 | 4, 159, 160 | sylanbrc 695 |
1
⊢ (𝑅 ∈ LNoeR → 𝑃 ∈ LNoeR) |