Step | Hyp | Ref
| Expression |
1 | | df-linc 42195 |
. . 3
⊢ linC =
(𝑚 ∈ V ↦ (𝑠 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝑀 ∈ 𝑋 → linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))))) |
3 | | fveq2 6191 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀)) |
4 | 3 | fveq2d 6195 |
. . . . 5
⊢ (𝑚 = 𝑀 → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) |
5 | 4 | oveq1d 6665 |
. . . 4
⊢ (𝑚 = 𝑀 → ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣)) |
6 | | fveq2 6191 |
. . . . 5
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
7 | 6 | pweqd 4163 |
. . . 4
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) |
8 | | id 22 |
. . . . 5
⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀) |
9 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (
·𝑠 ‘𝑚) = ( ·𝑠
‘𝑀)) |
10 | 9 | oveqd 6667 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥) = ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
11 | 10 | mpteq2dv 4745 |
. . . . 5
⊢ (𝑚 = 𝑀 → (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)) = (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
12 | 8, 11 | oveq12d 6668 |
. . . 4
⊢ (𝑚 = 𝑀 → (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
13 | 5, 7, 12 | mpt2eq123dv 6717 |
. . 3
⊢ (𝑚 = 𝑀 → (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
14 | 13 | adantl 482 |
. 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑚 = 𝑀) → (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
15 | | elex 3212 |
. 2
⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V) |
16 | | fvex 6201 |
. . . 4
⊢
(Base‘𝑀)
∈ V |
17 | 16 | pwex 4848 |
. . 3
⊢ 𝒫
(Base‘𝑀) ∈
V |
18 | | ovexd 6680 |
. . . 4
⊢ (𝑀 ∈ 𝑋 → ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈
V) |
19 | 18 | ralrimivw 2967 |
. . 3
⊢ (𝑀 ∈ 𝑋 → ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈
V) |
20 | | eqid 2622 |
. . . 4
⊢ (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
21 | 20 | mpt2exxg2 42116 |
. . 3
⊢
((𝒫 (Base‘𝑀) ∈ V ∧ ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈ V) → (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) |
22 | 17, 19, 21 | sylancr 695 |
. 2
⊢ (𝑀 ∈ 𝑋 → (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) |
23 | 2, 14, 15, 22 | fvmptd 6288 |
1
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |