| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-linc 48328 | . 2
⊢  linC =
(𝑚 ∈ V ↦ (𝑠 ∈
((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))))) | 
| 2 |  | 2fveq3 6910 | . . . 4
⊢ (𝑚 = 𝑀 → (Base‘(Scalar‘𝑚)) =
(Base‘(Scalar‘𝑀))) | 
| 3 | 2 | oveq1d 7447 | . . 3
⊢ (𝑚 = 𝑀 → ((Base‘(Scalar‘𝑚)) ↑m 𝑣) =
((Base‘(Scalar‘𝑀)) ↑m 𝑣)) | 
| 4 |  | fveq2 6905 | . . . 4
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) | 
| 5 | 4 | pweqd 4616 | . . 3
⊢ (𝑚 = 𝑀 → 𝒫 (Base‘𝑚) = 𝒫 (Base‘𝑀)) | 
| 6 |  | id 22 | . . . 4
⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀) | 
| 7 |  | fveq2 6905 | . . . . . 6
⊢ (𝑚 = 𝑀 → (
·𝑠 ‘𝑚) = ( ·𝑠
‘𝑀)) | 
| 8 | 7 | oveqd 7449 | . . . . 5
⊢ (𝑚 = 𝑀 → ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥) = ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)) | 
| 9 | 8 | mpteq2dv 5243 | . . . 4
⊢ (𝑚 = 𝑀 → (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)) = (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))) | 
| 10 | 6, 9 | oveq12d 7450 | . . 3
⊢ (𝑚 = 𝑀 → (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) | 
| 11 | 3, 5, 10 | mpoeq123dv 7509 | . 2
⊢ (𝑚 = 𝑀 → (𝑠 ∈ ((Base‘(Scalar‘𝑚)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑚) ↦ (𝑚 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑚)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) | 
| 12 |  | elex 3500 | . 2
⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V) | 
| 13 |  | fvex 6918 | . . . 4
⊢
(Base‘𝑀)
∈ V | 
| 14 | 13 | pwex 5379 | . . 3
⊢ 𝒫
(Base‘𝑀) ∈
V | 
| 15 |  | ovexd 7467 | . . . 4
⊢ (𝑀 ∈ 𝑋 → ((Base‘(Scalar‘𝑀)) ↑m 𝑣) ∈ V) | 
| 16 | 15 | ralrimivw 3149 | . . 3
⊢ (𝑀 ∈ 𝑋 → ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑m 𝑣) ∈ V) | 
| 17 |  | eqid 2736 | . . . 4
⊢ (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) | 
| 18 | 17 | mpoexxg2 48259 | . . 3
⊢
((𝒫 (Base‘𝑀) ∈ V ∧ ∀𝑣 ∈ 𝒫 (Base‘𝑀)((Base‘(Scalar‘𝑀)) ↑m 𝑣) ∈ V) → (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) | 
| 19 | 14, 16, 18 | sylancr 587 | . 2
⊢ (𝑀 ∈ 𝑋 → (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) ∈ V) | 
| 20 | 1, 11, 12, 19 | fvmptd3 7038 | 1
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑m 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |