Step | Hyp | Ref
| Expression |
1 | | aspval.a |
. . . . 5
⊢ 𝐴 = (AlgSpan‘𝑊) |
2 | | fveq2 6665 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
3 | | aspval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
4 | 2, 3 | syl6eqr 2874 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
5 | 4 | pweqd 4544 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉) |
6 | | fveq2 6665 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (SubRing‘𝑤) = (SubRing‘𝑊)) |
7 | | fveq2 6665 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
8 | | aspval.l |
. . . . . . . . . . 11
⊢ 𝐿 = (LSubSp‘𝑊) |
9 | 7, 8 | syl6eqr 2874 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝐿) |
10 | 6, 9 | ineq12d 4190 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) = ((SubRing‘𝑊) ∩ 𝐿)) |
11 | 10 | rabeqdv 3485 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
12 | 11 | inteqd 4874 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
13 | 5, 12 | mpteq12dv 5144 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡
∈ ((SubRing‘𝑤)
∩ (LSubSp‘𝑤))
∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
14 | | df-asp 20080 |
. . . . . 6
⊢ AlgSpan =
(𝑤 ∈ AssAlg ↦
(𝑠 ∈ 𝒫
(Base‘𝑤) ↦
∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})) |
15 | 3 | fvexi 6679 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
16 | 15 | pwex 5274 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
17 | 16 | mptex 6980 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) ∈ V |
18 | 13, 14, 17 | fvmpt 6763 |
. . . . 5
⊢ (𝑊 ∈ AssAlg →
(AlgSpan‘𝑊) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
19 | 1, 18 | syl5eq 2868 |
. . . 4
⊢ (𝑊 ∈ AssAlg → 𝐴 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
20 | 19 | fveq1d 6667 |
. . 3
⊢ (𝑊 ∈ AssAlg → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
21 | 20 | adantr 483 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
22 | | eqid 2821 |
. . 3
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
23 | | sseq1 3992 |
. . . . 5
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑡)) |
24 | 23 | rabbidv 3481 |
. . . 4
⊢ (𝑠 = 𝑆 → {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
25 | 24 | inteqd 4874 |
. . 3
⊢ (𝑠 = 𝑆 → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
26 | | simpr 487 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
27 | 15 | elpw2 5241 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉) |
28 | 26, 27 | sylibr 236 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ∈ 𝒫 𝑉) |
29 | | assaring 20087 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
30 | 3 | subrgid 19531 |
. . . . . . 7
⊢ (𝑊 ∈ Ring → 𝑉 ∈ (SubRing‘𝑊)) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ (SubRing‘𝑊)) |
32 | | assalmod 20086 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
33 | 3, 8 | lss1 19704 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝐿) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ 𝐿) |
35 | 31, 34 | elind 4171 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿)) |
36 | | sseq2 3993 |
. . . . . 6
⊢ (𝑡 = 𝑉 → (𝑆 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑉)) |
37 | 36 | rspcev 3623 |
. . . . 5
⊢ ((𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
38 | 35, 37 | sylan 582 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
39 | | intexrab 5236 |
. . . 4
⊢
(∃𝑡 ∈
((SubRing‘𝑊) ∩
𝐿)𝑆 ⊆ 𝑡 ↔ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
40 | 38, 39 | sylib 220 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
41 | 22, 25, 28, 40 | fvmptd3 6786 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
42 | 21, 41 | eqtrd 2856 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |