Step | Hyp | Ref
| Expression |
1 | | lincop 41991 |
. . . 4
⊢ (𝑀 ∈ 𝑋 → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
2 | 1 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → ( linC ‘𝑀) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))) |
3 | 2 | oveqd 6566 |
. 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑆(𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))𝑉)) |
4 | | simp2 1055 |
. . 3
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉)) |
5 | | simp3 1056 |
. . 3
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
6 | | ovex 6577 |
. . . 4
⊢ (𝑀 Σg
(𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥))) ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥))) ∈ V) |
8 | | simpr 476 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉) |
9 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → (𝑠‘𝑥) = (𝑆‘𝑥)) |
10 | 9 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥) = ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑣 = 𝑉) → ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥) = ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥)) |
12 | 8, 11 | mpteq12dv 4663 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑣 = 𝑉) → (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
13 | 12 | oveq2d 6565 |
. . . 4
⊢ ((𝑠 = 𝑆 ∧ 𝑣 = 𝑉) → (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
14 | | oveq2 6557 |
. . . 4
⊢ (𝑣 = 𝑉 → ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣) =
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉)) |
15 | | eqid 2610 |
. . . 4
⊢ (𝑠 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) = (𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
16 | 13, 14, 15 | ovmpt2x2 41912 |
. . 3
⊢ ((𝑆 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀) ∧ (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥))) ∈ V) → (𝑆(𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
17 | 4, 5, 7, 16 | syl3anc 1318 |
. 2
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆(𝑠 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑣), 𝑣 ∈ 𝒫 (Base‘𝑀) ↦ (𝑀 Σg (𝑥 ∈ 𝑣 ↦ ((𝑠‘𝑥)( ·𝑠
‘𝑀)𝑥))))𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
18 | 3, 17 | eqtrd 2644 |
1
⊢ ((𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
𝑉) ∧ 𝑉 ∈ 𝒫 (Base‘𝑀)) → (𝑆( linC ‘𝑀)𝑉) = (𝑀 Σg (𝑥 ∈ 𝑉 ↦ ((𝑆‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |