Step | Hyp | Ref
| Expression |
1 | | rgspnval.sp |
. 2
⊢ (𝜑 → 𝑈 = (𝑁‘𝐴)) |
2 | | rgspnval.n |
. . 3
⊢ (𝜑 → 𝑁 = (RingSpan‘𝑅)) |
3 | 2 | fveq1d 6193 |
. 2
⊢ (𝜑 → (𝑁‘𝐴) = ((RingSpan‘𝑅)‘𝐴)) |
4 | | rgspnval.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
5 | | elex 3212 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ V) |
6 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑎 = 𝑅 → (Base‘𝑎) = (Base‘𝑅)) |
7 | 6 | pweqd 4163 |
. . . . . . 7
⊢ (𝑎 = 𝑅 → 𝒫 (Base‘𝑎) = 𝒫 (Base‘𝑅)) |
8 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑎 = 𝑅 → (SubRing‘𝑎) = (SubRing‘𝑅)) |
9 | | rabeq 3192 |
. . . . . . . . 9
⊢
((SubRing‘𝑎) =
(SubRing‘𝑅) →
{𝑡 ∈
(SubRing‘𝑎) ∣
𝑏 ⊆ 𝑡} = {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡}) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝑎 = 𝑅 → {𝑡 ∈ (SubRing‘𝑎) ∣ 𝑏 ⊆ 𝑡} = {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡}) |
11 | 10 | inteqd 4480 |
. . . . . . 7
⊢ (𝑎 = 𝑅 → ∩ {𝑡 ∈ (SubRing‘𝑎) ∣ 𝑏 ⊆ 𝑡} = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡}) |
12 | 7, 11 | mpteq12dv 4733 |
. . . . . 6
⊢ (𝑎 = 𝑅 → (𝑏 ∈ 𝒫 (Base‘𝑎) ↦ ∩ {𝑡
∈ (SubRing‘𝑎)
∣ 𝑏 ⊆ 𝑡}) = (𝑏 ∈ 𝒫 (Base‘𝑅) ↦ ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝑏 ⊆ 𝑡})) |
13 | | df-rgspn 18779 |
. . . . . 6
⊢ RingSpan
= (𝑎 ∈ V ↦
(𝑏 ∈ 𝒫
(Base‘𝑎) ↦
∩ {𝑡 ∈ (SubRing‘𝑎) ∣ 𝑏 ⊆ 𝑡})) |
14 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝑅)
∈ V |
15 | 14 | pwex 4848 |
. . . . . . 7
⊢ 𝒫
(Base‘𝑅) ∈
V |
16 | 15 | mptex 6486 |
. . . . . 6
⊢ (𝑏 ∈ 𝒫
(Base‘𝑅) ↦
∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡}) ∈ V |
17 | 12, 13, 16 | fvmpt 6282 |
. . . . 5
⊢ (𝑅 ∈ V →
(RingSpan‘𝑅) = (𝑏 ∈ 𝒫
(Base‘𝑅) ↦
∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡})) |
18 | 4, 5, 17 | 3syl 18 |
. . . 4
⊢ (𝜑 → (RingSpan‘𝑅) = (𝑏 ∈ 𝒫 (Base‘𝑅) ↦ ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝑏 ⊆ 𝑡})) |
19 | 18 | fveq1d 6193 |
. . 3
⊢ (𝜑 → ((RingSpan‘𝑅)‘𝐴) = ((𝑏 ∈ 𝒫 (Base‘𝑅) ↦ ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝑏 ⊆ 𝑡})‘𝐴)) |
20 | | rgspnval.ss |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
21 | | rgspnval.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
22 | 20, 21 | sseqtrd 3641 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ (Base‘𝑅)) |
23 | 14 | elpw2 4828 |
. . . . 5
⊢ (𝐴 ∈ 𝒫
(Base‘𝑅) ↔ 𝐴 ⊆ (Base‘𝑅)) |
24 | 22, 23 | sylibr 224 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝒫 (Base‘𝑅)) |
25 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
26 | 25 | subrgid 18782 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) ∈
(SubRing‘𝑅)) |
27 | 4, 26 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑅) ∈ (SubRing‘𝑅)) |
28 | 21, 27 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅)) |
29 | | sseq2 3627 |
. . . . . . 7
⊢ (𝑡 = 𝐵 → (𝐴 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝐵)) |
30 | 29 | rspcev 3309 |
. . . . . 6
⊢ ((𝐵 ∈ (SubRing‘𝑅) ∧ 𝐴 ⊆ 𝐵) → ∃𝑡 ∈ (SubRing‘𝑅)𝐴 ⊆ 𝑡) |
31 | 28, 20, 30 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ∃𝑡 ∈ (SubRing‘𝑅)𝐴 ⊆ 𝑡) |
32 | | intexrab 4823 |
. . . . 5
⊢
(∃𝑡 ∈
(SubRing‘𝑅)𝐴 ⊆ 𝑡 ↔ ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡} ∈ V) |
33 | 31, 32 | sylib 208 |
. . . 4
⊢ (𝜑 → ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝐴 ⊆ 𝑡} ∈ V) |
34 | | sseq1 3626 |
. . . . . . 7
⊢ (𝑏 = 𝐴 → (𝑏 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝑡)) |
35 | 34 | rabbidv 3189 |
. . . . . 6
⊢ (𝑏 = 𝐴 → {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡} = {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
36 | 35 | inteqd 4480 |
. . . . 5
⊢ (𝑏 = 𝐴 → ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡} = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
37 | | eqid 2622 |
. . . . 5
⊢ (𝑏 ∈ 𝒫
(Base‘𝑅) ↦
∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡}) = (𝑏 ∈ 𝒫 (Base‘𝑅) ↦ ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝑏 ⊆ 𝑡}) |
38 | 36, 37 | fvmptg 6280 |
. . . 4
⊢ ((𝐴 ∈ 𝒫
(Base‘𝑅) ∧ ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝐴 ⊆ 𝑡} ∈ V) → ((𝑏 ∈ 𝒫
(Base‘𝑅) ↦
∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝑏 ⊆ 𝑡})‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
39 | 24, 33, 38 | syl2anc 693 |
. . 3
⊢ (𝜑 → ((𝑏 ∈ 𝒫 (Base‘𝑅) ↦ ∩ {𝑡
∈ (SubRing‘𝑅)
∣ 𝑏 ⊆ 𝑡})‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
40 | 19, 39 | eqtrd 2656 |
. 2
⊢ (𝜑 → ((RingSpan‘𝑅)‘𝐴) = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |
41 | 1, 3, 40 | 3eqtrd 2660 |
1
⊢ (𝜑 → 𝑈 = ∩ {𝑡 ∈ (SubRing‘𝑅) ∣ 𝐴 ⊆ 𝑡}) |