| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. . . 4
⊢ (𝑊 ∈ 𝑉 → 𝑊 ∈ V) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → 𝑊 ∈ V) |
| 3 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
| 4 | 3 | pweqd 4617 |
. . . . 5
⊢ (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 (Base‘𝑊)) |
| 5 | | id 22 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
| 6 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑤 ↾s 𝑠) = (𝑊 ↾s 𝑠)) |
| 7 | 6 | opeq2d 4880 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → 〈(Scalar‘ndx), (𝑤 ↾s 𝑠)〉 =
〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) |
| 8 | 5, 7 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑤 sSet 〈(Scalar‘ndx), (𝑤 ↾s 𝑠)〉) = (𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉)) |
| 9 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (.r‘𝑤) = (.r‘𝑊)) |
| 10 | 9 | opeq2d 4880 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 〈(
·𝑠 ‘ndx), (.r‘𝑤)〉 = 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) |
| 11 | 8, 10 | oveq12d 7449 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝑤 sSet 〈(Scalar‘ndx), (𝑤 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑤)〉) = ((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) |
| 12 | 9 | opeq2d 4880 |
. . . . . 6
⊢ (𝑤 = 𝑊 →
〈(·𝑖‘ndx),
(.r‘𝑤)〉 =
〈(·𝑖‘ndx),
(.r‘𝑊)〉) |
| 13 | 11, 12 | oveq12d 7449 |
. . . . 5
⊢ (𝑤 = 𝑊 → (((𝑤 sSet 〈(Scalar‘ndx), (𝑤 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑤)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑤)〉) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
| 14 | 4, 13 | mpteq12dv 5233 |
. . . 4
⊢ (𝑤 = 𝑊 → (𝑠 ∈ 𝒫 (Base‘𝑤) ↦ (((𝑤 sSet 〈(Scalar‘ndx), (𝑤 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑤)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑤)〉)) = (𝑠 ∈ 𝒫 (Base‘𝑊) ↦ (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
| 15 | | df-sra 21172 |
. . . 4
⊢
subringAlg = (𝑤
∈ V ↦ (𝑠 ∈
𝒫 (Base‘𝑤)
↦ (((𝑤 sSet
〈(Scalar‘ndx), (𝑤 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑤)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑤)〉))) |
| 16 | | fvex 6919 |
. . . . . 6
⊢
(Base‘𝑊)
∈ V |
| 17 | 16 | pwex 5380 |
. . . . 5
⊢ 𝒫
(Base‘𝑊) ∈
V |
| 18 | 17 | mptex 7243 |
. . . 4
⊢ (𝑠 ∈ 𝒫
(Base‘𝑊) ↦
(((𝑊 sSet
〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) ∈ V |
| 19 | 14, 15, 18 | fvmpt 7016 |
. . 3
⊢ (𝑊 ∈ V → (subringAlg
‘𝑊) = (𝑠 ∈ 𝒫
(Base‘𝑊) ↦
(((𝑊 sSet
〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
| 20 | 2, 19 | syl 17 |
. 2
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → (subringAlg ‘𝑊) = (𝑠 ∈ 𝒫 (Base‘𝑊) ↦ (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉))) |
| 21 | | simpr 484 |
. . . . . . 7
⊢ (((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
| 22 | 21 | oveq2d 7447 |
. . . . . 6
⊢ (((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) ∧ 𝑠 = 𝑆) → (𝑊 ↾s 𝑠) = (𝑊 ↾s 𝑆)) |
| 23 | 22 | opeq2d 4880 |
. . . . 5
⊢ (((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) ∧ 𝑠 = 𝑆) → 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉 =
〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) |
| 24 | 23 | oveq2d 7447 |
. . . 4
⊢ (((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) ∧ 𝑠 = 𝑆) → (𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) = (𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉)) |
| 25 | 24 | oveq1d 7446 |
. . 3
⊢ (((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) ∧ 𝑠 = 𝑆) → ((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) = ((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉)) |
| 26 | 25 | oveq1d 7446 |
. 2
⊢ (((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) ∧ 𝑠 = 𝑆) → (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑠)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |
| 27 | | simpr 484 |
. . 3
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → 𝑆 ⊆ (Base‘𝑊)) |
| 28 | 16 | elpw2 5334 |
. . 3
⊢ (𝑆 ∈ 𝒫
(Base‘𝑊) ↔ 𝑆 ⊆ (Base‘𝑊)) |
| 29 | 27, 28 | sylibr 234 |
. 2
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → 𝑆 ∈ 𝒫 (Base‘𝑊)) |
| 30 | | ovexd 7466 |
. 2
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉) ∈ V) |
| 31 | 20, 26, 29, 30 | fvmptd 7023 |
1
⊢ ((𝑊 ∈ 𝑉 ∧ 𝑆 ⊆ (Base‘𝑊)) → ((subringAlg ‘𝑊)‘𝑆) = (((𝑊 sSet 〈(Scalar‘ndx), (𝑊 ↾s 𝑆)〉) sSet 〈(
·𝑠 ‘ndx), (.r‘𝑊)〉) sSet
〈(·𝑖‘ndx),
(.r‘𝑊)〉)) |