Metamath Proof Explorer

Theorem lincop

Description: A linear combination as operation. (Contributed by AV, 30-Mar-2019)

Ref Expression
Assertion lincop ( 𝑀 ∈ 𝑋 → ( linC ‘ 𝑀 ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-linc ⊢ linC = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) ) ) )
2 2fveq3 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
3 2 oveq1d ⊢ ( 𝑚 = 𝑀 → ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) )
4 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
5 4 pweqd ⊢ ( 𝑚 = 𝑀 → 𝒫 ( Base ‘ 𝑚 ) = 𝒫 ( Base ‘ 𝑀 ) )
6 id ⊢ ( 𝑚 = 𝑀 → 𝑚 = 𝑀 )
7 fveq2 ⊢ ( 𝑚 = 𝑀 → ( ·𝑠 ‘ 𝑚 ) = ( ·𝑠 ‘ 𝑀 ) )
8 7 oveqd ⊢ ( 𝑚 = 𝑀 → ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) = ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
9 8 mpteq2dv ⊢ ( 𝑚 = 𝑀 → ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) )
10 6 9 oveq12d ⊢ ( 𝑚 = 𝑀 → ( 𝑚 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) ) = ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
11 3 5 10 mpoeq123dv ⊢ ( 𝑚 = 𝑀 → ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑚 ) 𝑥 ) ) ) ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
12 elex ⊢ ( 𝑀 ∈ 𝑋 → 𝑀 ∈ V )
13 fvex ⊢ ( Base ‘ 𝑀 ) ∈ V
14 13 pwex ⊢ 𝒫 ( Base ‘ 𝑀 ) ∈ V
15 ovexd ⊢ ( 𝑀 ∈ 𝑋 → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) ∈ V )
16 15 ralrimivw ⊢ ( 𝑀 ∈ 𝑋 → ∀ 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) ∈ V )
17 eqid ⊢ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
18 17 mpoexxg2 ⊢ ( ( 𝒫 ( Base ‘ 𝑀 ) ∈ V ∧ ∀ 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) ∈ V ) → ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) ∈ V )
19 14 16 18 sylancr ⊢ ( 𝑀 ∈ 𝑋 → ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) ∈ V )
20 1 11 12 19 fvmptd3 ⊢ ( 𝑀 ∈ 𝑋 → ( linC ‘ 𝑀 ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σg ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )