Metamath Proof Explorer

Theorem dflinc2

Description: Alternative definition of linear combinations using the function operation. (Contributed by AV, 1-Apr-2019)

Ref Expression
Assertion dflinc2 linC = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑠 ∘f ( ·𝑠 ‘ 𝑚 ) ( I ↾ 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-linc ⊢ linC = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑖 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑚 ) 𝑖 ) ) ) ) )
2 elmapfn ⊢ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) → 𝑠 Fn 𝑣 )
3 2 adantr ⊢ ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → 𝑠 Fn 𝑣 )
4 fnresi ⊢ ( I ↾ 𝑣 ) Fn 𝑣
5 4 a1i ⊢ ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → ( I ↾ 𝑣 ) Fn 𝑣 )
6 vex ⊢ 𝑣 ∈ V
7 6 a1i ⊢ ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → 𝑣 ∈ V )
8 inidm ⊢ ( 𝑣 ∩ 𝑣 ) = 𝑣
9 eqidd ⊢ ( ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) ∧ 𝑖 ∈ 𝑣 ) → ( 𝑠 ‘ 𝑖 ) = ( 𝑠 ‘ 𝑖 ) )
10 fvresi ⊢ ( 𝑖 ∈ 𝑣 → ( ( I ↾ 𝑣 ) ‘ 𝑖 ) = 𝑖 )
11 10 adantl ⊢ ( ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) ∧ 𝑖 ∈ 𝑣 ) → ( ( I ↾ 𝑣 ) ‘ 𝑖 ) = 𝑖 )
12 3 5 7 7 8 9 11 offval ⊢ ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → ( 𝑠 ∘f ( ·𝑠 ‘ 𝑚 ) ( I ↾ 𝑣 ) ) = ( 𝑖 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑚 ) 𝑖 ) ) )
13 12 eqcomd ⊢ ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → ( 𝑖 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑚 ) 𝑖 ) ) = ( 𝑠 ∘f ( ·𝑠 ‘ 𝑚 ) ( I ↾ 𝑣 ) ) )
14 13 oveq2d ⊢ ( ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) ∧ 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ) → ( 𝑚 Σg ( 𝑖 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑚 ) 𝑖 ) ) ) = ( 𝑚 Σg ( 𝑠 ∘f ( ·𝑠 ‘ 𝑚 ) ( I ↾ 𝑣 ) ) ) )
15 14 mpoeq3ia ⊢ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑖 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑚 ) 𝑖 ) ) ) ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑠 ∘f ( ·𝑠 ‘ 𝑚 ) ( I ↾ 𝑣 ) ) ) )
16 15 mpteq2i ⊢ ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑖 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑚 ) 𝑖 ) ) ) ) ) = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑠 ∘f ( ·𝑠 ‘ 𝑚 ) ( I ↾ 𝑣 ) ) ) ) )
17 1 16 eqtri ⊢ linC = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑚 ) ) ↑m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ ( 𝑚 Σg ( 𝑠 ∘f ( ·𝑠 ‘ 𝑚 ) ( I ↾ 𝑣 ) ) ) ) )