Step | Hyp | Ref
| Expression |
1 | | aspval.a |
. . . . 5
⊢ 𝐴 = (AlgSpan‘𝑊) |
2 | | fveq2 6735 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
3 | | aspval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
4 | 2, 3 | eqtr4di 2797 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
5 | 4 | pweqd 4546 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉) |
6 | | fveq2 6735 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (SubRing‘𝑤) = (SubRing‘𝑊)) |
7 | | fveq2 6735 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
8 | | aspval.l |
. . . . . . . . . . 11
⊢ 𝐿 = (LSubSp‘𝑊) |
9 | 7, 8 | eqtr4di 2797 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝐿) |
10 | 6, 9 | ineq12d 4142 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) = ((SubRing‘𝑊) ∩ 𝐿)) |
11 | 10 | rabeqdv 3407 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
12 | 11 | inteqd 4878 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
13 | 5, 12 | mpteq12dv 5154 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡
∈ ((SubRing‘𝑤)
∩ (LSubSp‘𝑤))
∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
14 | | df-asp 20840 |
. . . . . 6
⊢ AlgSpan =
(𝑤 ∈ AssAlg ↦
(𝑠 ∈ 𝒫
(Base‘𝑤) ↦
∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})) |
15 | 3 | fvexi 6749 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
16 | 15 | pwex 5287 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
17 | 16 | mptex 7057 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) ∈ V |
18 | 13, 14, 17 | fvmpt 6836 |
. . . . 5
⊢ (𝑊 ∈ AssAlg →
(AlgSpan‘𝑊) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
19 | 1, 18 | eqtrid 2790 |
. . . 4
⊢ (𝑊 ∈ AssAlg → 𝐴 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
20 | 19 | fveq1d 6737 |
. . 3
⊢ (𝑊 ∈ AssAlg → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
21 | 20 | adantr 484 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
22 | | eqid 2738 |
. . 3
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
23 | | sseq1 3940 |
. . . . 5
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑡)) |
24 | 23 | rabbidv 3402 |
. . . 4
⊢ (𝑠 = 𝑆 → {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
25 | 24 | inteqd 4878 |
. . 3
⊢ (𝑠 = 𝑆 → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
26 | | simpr 488 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
27 | 15 | elpw2 5252 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉) |
28 | 26, 27 | sylibr 237 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ∈ 𝒫 𝑉) |
29 | | assaring 20847 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
30 | 3 | subrgid 19826 |
. . . . . . 7
⊢ (𝑊 ∈ Ring → 𝑉 ∈ (SubRing‘𝑊)) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ (SubRing‘𝑊)) |
32 | | assalmod 20846 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
33 | 3, 8 | lss1 19999 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝐿) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ 𝐿) |
35 | 31, 34 | elind 4122 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿)) |
36 | | sseq2 3941 |
. . . . . 6
⊢ (𝑡 = 𝑉 → (𝑆 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑉)) |
37 | 36 | rspcev 3549 |
. . . . 5
⊢ ((𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
38 | 35, 37 | sylan 583 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
39 | | intexrab 5247 |
. . . 4
⊢
(∃𝑡 ∈
((SubRing‘𝑊) ∩
𝐿)𝑆 ⊆ 𝑡 ↔ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
40 | 38, 39 | sylib 221 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
41 | 22, 25, 28, 40 | fvmptd3 6859 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
42 | 21, 41 | eqtrd 2778 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |