Step | Hyp | Ref
| Expression |
1 | | aspval.a |
. . . . 5
⊢ 𝐴 = (AlgSpan‘𝑊) |
2 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
3 | | aspval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
4 | 2, 3 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
5 | 4 | pweqd 4113 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉) |
6 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (SubRing‘𝑤) = (SubRing‘𝑊)) |
7 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
8 | | aspval.l |
. . . . . . . . . . 11
⊢ 𝐿 = (LSubSp‘𝑊) |
9 | 7, 8 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝐿) |
10 | 6, 9 | ineq12d 3777 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) = ((SubRing‘𝑊) ∩ 𝐿)) |
11 | | rabeq 3166 |
. . . . . . . . 9
⊢
(((SubRing‘𝑤)
∩ (LSubSp‘𝑤)) =
((SubRing‘𝑊) ∩
𝐿) → {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
13 | 12 | inteqd 4415 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
14 | 5, 13 | mpteq12dv 4663 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ ∩ {𝑡
∈ ((SubRing‘𝑤)
∩ (LSubSp‘𝑤))
∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
15 | | df-asp 19134 |
. . . . . 6
⊢ AlgSpan =
(𝑤 ∈ AssAlg ↦
(𝑠 ∈ 𝒫
(Base‘𝑤) ↦
∩ {𝑡 ∈ ((SubRing‘𝑤) ∩ (LSubSp‘𝑤)) ∣ 𝑠 ⊆ 𝑡})) |
16 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
17 | 3, 16 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
18 | 17 | pwex 4774 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
19 | 18 | mptex 6390 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) ∈ V |
20 | 14, 15, 19 | fvmpt 6191 |
. . . . 5
⊢ (𝑊 ∈ AssAlg →
(AlgSpan‘𝑊) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
21 | 1, 20 | syl5eq 2656 |
. . . 4
⊢ (𝑊 ∈ AssAlg → 𝐴 = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})) |
22 | 21 | fveq1d 6105 |
. . 3
⊢ (𝑊 ∈ AssAlg → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
23 | 22 | adantr 480 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆)) |
24 | | simpr 476 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ 𝑉) |
25 | 17 | elpw2 4755 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉) |
26 | 24, 25 | sylibr 223 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → 𝑆 ∈ 𝒫 𝑉) |
27 | | assaring 19141 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring) |
28 | 3 | subrgid 18605 |
. . . . . . 7
⊢ (𝑊 ∈ Ring → 𝑉 ∈ (SubRing‘𝑊)) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ (SubRing‘𝑊)) |
30 | | assalmod 19140 |
. . . . . . 7
⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod) |
31 | 3, 8 | lss1 18760 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝐿) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ 𝐿) |
33 | 29, 32 | elind 3760 |
. . . . 5
⊢ (𝑊 ∈ AssAlg → 𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿)) |
34 | | sseq2 3590 |
. . . . . 6
⊢ (𝑡 = 𝑉 → (𝑆 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑉)) |
35 | 34 | rspcev 3282 |
. . . . 5
⊢ ((𝑉 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
36 | 33, 35 | sylan 487 |
. . . 4
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∃𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿)𝑆 ⊆ 𝑡) |
37 | | intexrab 4750 |
. . . 4
⊢
(∃𝑡 ∈
((SubRing‘𝑊) ∩
𝐿)𝑆 ⊆ 𝑡 ↔ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
38 | 36, 37 | sylib 207 |
. . 3
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) |
39 | | sseq1 3589 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑡 ↔ 𝑆 ⊆ 𝑡)) |
40 | 39 | rabbidv 3164 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
41 | 40 | inteqd 4415 |
. . . 4
⊢ (𝑠 = 𝑆 → ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡} = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
42 | | eqid 2610 |
. . . 4
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) = (𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡}) |
43 | 41, 42 | fvmptg 6189 |
. . 3
⊢ ((𝑆 ∈ 𝒫 𝑉 ∧ ∩ {𝑡
∈ ((SubRing‘𝑊)
∩ 𝐿) ∣ 𝑆 ⊆ 𝑡} ∈ V) → ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
44 | 26, 38, 43 | syl2anc 691 |
. 2
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → ((𝑠 ∈ 𝒫 𝑉 ↦ ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑠 ⊆ 𝑡})‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |
45 | 23, 44 | eqtrd 2644 |
1
⊢ ((𝑊 ∈ AssAlg ∧ 𝑆 ⊆ 𝑉) → (𝐴‘𝑆) = ∩ {𝑡 ∈ ((SubRing‘𝑊) ∩ 𝐿) ∣ 𝑆 ⊆ 𝑡}) |