Step | Hyp | Ref
| Expression |
1 | | df-linc 41989 |
. . 3
⊢ linC =
(𝑚 ∈ V ↦ (𝑠 ∈
((Base‘(Scalar‘𝑚)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝑀 ∈ 𝑋 → linC = (𝑚 ∈ V ↦ (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))))) |
3 | | fveq2 6103 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀)) |
4 | 3 | fveq2d 6107 |
. . . . 5
⊢ (𝑚 = 𝑀 → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) |
5 | 4 | oveq1d 6564 |
. . . 4
⊢ (𝑚 = 𝑀 → ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣)) |
6 | | fveq2 6103 |
. . . . 5
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
7 | 6 | pweqd 4113 |
. . . 4
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) |
8 | | id 22 |
. . . . 5
⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀) |
9 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (
·𝑠 ‘𝑚) = ( ·𝑠
‘𝑀)) |
10 | 9 | oveqd 6566 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥) = ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
11 | 10 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑚 = 𝑀 → (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)) = (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
12 | 8, 11 | oveq12d 6567 |
. . . 4
⊢ (𝑚 = 𝑀 → (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
13 | 5, 7, 12 | mpt2eq123dv 6615 |
. . 3
⊢ (𝑚 = 𝑀 → (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
14 | 13 | adantl 481 |
. 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑚 = 𝑀) → (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
15 | | elex 3185 |
. 2
⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V) |
16 | | fvex 6113 |
. . . 4
⊢
(Base‘𝑀)
∈ V |
17 | 16 | pwex 4774 |
. . 3
⊢ 𝒫
(Base‘𝑀) ∈
V |
18 | | ovex 6577 |
. . . . 5
⊢
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣) ∈ V |
19 | 18 | a1i 11 |
. . . 4
⊢ (𝑀 ∈ 𝑋 → ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈
V) |
20 | 19 | ralrimivw 2950 |
. . 3
⊢ (𝑀 ∈ 𝑋 → ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈
V) |
21 | | eqid 2610 |
. . . 4
⊢ (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
22 | 21 | mpt2exxg2 41909 |
. . 3
⊢
((𝒫 (Base‘𝑀) ∈ V ∧ ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) ∈ V) → (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) |
23 | 17, 20, 22 | sylancr 694 |
. 2
⊢ (𝑀 ∈ 𝑋 → (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) |
24 | 2, 14, 15, 23 | fvmptd 6197 |
1
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |