Step | Hyp | Ref
| Expression |
1 | | df-linc 43214 |
. 2
⊢ linC =
(𝑚 ∈ V ↦ (𝑠 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))))) |
2 | | 2fveq3 6451 |
. . . 4
⊢ (𝑚 = 𝑀 → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) |
3 | 2 | oveq1d 6937 |
. . 3
⊢ (𝑚 = 𝑀 → ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣)) |
4 | | fveq2 6446 |
. . . 4
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
5 | 4 | pweqd 4384 |
. . 3
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) |
6 | | id 22 |
. . . 4
⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀) |
7 | | fveq2 6446 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (
·𝑠 ‘𝑚) = ( ·𝑠
‘𝑀)) |
8 | 7 | oveqd 6939 |
. . . . 5
⊢ (𝑚 = 𝑀 → ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥) = ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
9 | 8 | mpteq2dv 4980 |
. . . 4
⊢ (𝑚 = 𝑀 → (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)) = (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
10 | 6, 9 | oveq12d 6940 |
. . 3
⊢ (𝑚 = 𝑀 → (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
11 | 3, 5, 10 | mpt2eq123dv 6994 |
. 2
⊢ (𝑚 = 𝑀 → (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
12 | | elex 3414 |
. 2
⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V) |
13 | | fvex 6459 |
. . . 4
⊢
(Base‘𝑀)
∈ V |
14 | 13 | pwex 5092 |
. . 3
⊢ 𝒫
(Base‘𝑀) ∈
V |
15 | | ovexd 6956 |
. . . 4
⊢ (𝑀 ∈ 𝑋 → ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈
V) |
16 | 15 | ralrimivw 3149 |
. . 3
⊢ (𝑀 ∈ 𝑋 → ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈
V) |
17 | | eqid 2778 |
. . . 4
⊢ (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
18 | 17 | mpt2exxg2 43135 |
. . 3
⊢
((𝒫 (Base‘𝑀) ∈ V ∧ ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈ V) → (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) |
19 | 14, 16, 18 | sylancr 581 |
. 2
⊢ (𝑀 ∈ 𝑋 → (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) |
20 | 1, 11, 12, 19 | fvmptd3 6564 |
1
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |