Step | Hyp | Ref
| Expression |
1 | | aspval.a |
. . . . 5
⊢ 𝐴 = (AlgSpan‘𝑊) |
2 | | fveq2 6340 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
3 | | aspval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
4 | 2, 3 | syl6eqr 2800 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
5 | 4 | pweqd 4295 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉) |
6 | | fveq2 6340 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (SubRing‘𝑤) = (SubRing‘𝑊)) |
7 | | fveq2 6340 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
8 | | aspval.l |
. . . . . . . . . . 11
⊢ 𝐿 = (LSubSp‘𝑊) |
9 | 7, 8 | syl6eqr 2800 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝐿) |
10 | 6, 9 | ineq12d 3946 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) = ((SubRing‘𝑊) ∩ 𝐿)) |
11 | | rabeq 3320 |
. . . . . . . . 9
⊢
(((SubRing‘𝑤)
∩ (LSubSp‘𝑤)) =
((SubRing‘𝑊) ∩
𝐿) → {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
13 | 12 | inteqd 4620 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
14 | 5, 13 | mpteq12dv 4873 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡
∈ ((SubRing‘𝑤)
∩ (LSubSp‘𝑤))
∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
15 | | df-asp 19486 |
. . . . . 6
⊢ AlgSpan =
(𝑤 ∈ AssAlg ↦
(𝑠 ∈ 𝒫
(Base‘𝑤) ↦
∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})) |
16 | | fvex 6350 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
17 | 3, 16 | eqeltri 2823 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
18 | 17 | pwex 4985 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
19 | 18 | mptex 6638 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) ∈ V |
20 | 14, 15, 19 | fvmpt 6432 |
. . . . 5
⊢ (𝑊 ∈ AssAlg →
(AlgSpan‘𝑊) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
21 | 1, 20 | syl5eq 2794 |
. . . 4
⊢ (𝑊 ∈ AssAlg → 𝐴 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
22 | 21 | fveq1d 6342 |
. . 3
⊢ (𝑊 ∈ AssAlg → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
23 | 22 | adantr 472 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
24 | | simpr 479 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
25 | 17 | elpw2 4965 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉) |
26 | 24, 25 | sylibr 224 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ∈ 𝒫 𝑉) |
27 | | assaring 19493 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
28 | 3 | subrgid 18955 |
. . . . . . 7
⊢ (𝑊 ∈ Ring → 𝑉 ∈ (SubRing‘𝑊)) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ (SubRing‘𝑊)) |
30 | | assalmod 19492 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
31 | 3, 8 | lss1 19112 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝐿) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ 𝐿) |
33 | 29, 32 | elind 3929 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿)) |
34 | | sseq2 3756 |
. . . . . 6
⊢ (𝑡 = 𝑉 → (𝑆 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑉)) |
35 | 34 | rspcev 3437 |
. . . . 5
⊢ ((𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
36 | 33, 35 | sylan 489 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
37 | | intexrab 4960 |
. . . 4
⊢
(∃𝑡 ∈
((SubRing‘𝑊) ∩
𝐿)𝑆 ⊆ 𝑡 ↔ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
38 | 36, 37 | sylib 208 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
39 | | sseq1 3755 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑡)) |
40 | 39 | rabbidv 3317 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
41 | 40 | inteqd 4620 |
. . . 4
⊢ (𝑠 = 𝑆 → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
42 | | eqid 2748 |
. . . 4
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
43 | 41, 42 | fvmptg 6430 |
. . 3
⊢ ((𝑆 ∈ 𝒫 𝑉 ∧ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) → ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
44 | 26, 38, 43 | syl2anc 696 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
45 | 23, 44 | eqtrd 2782 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |