Metamath Proof Explorer

Theorem lincval

Description: The value of a linear combination. (Contributed by AV, 30-Mar-2019)

		Ref	Expression
	Assertion	lincval	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lincop	⊢ ( 𝑀 ∈ 𝑋 → ( linC ‘ 𝑀 ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
2	1	3ad2ant1	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( linC ‘ 𝑀 ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) )
3	2	oveqd	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑆 ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) 𝑉 ) )
4		simp2	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) )
5		simp3	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
6		ovexd	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ∈ V )
7		simpr	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑣 = 𝑉 ) → 𝑣 = 𝑉 )
8		fveq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
9	8	oveq1d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) )
10	9	adantr	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑣 = 𝑉 ) → ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) )
11	7 10	mpteq12dv	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑣 = 𝑉 ) → ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) )
12	11	oveq2d	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑣 = 𝑉 ) → ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) = ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
13		oveq2	⊢ ( 𝑣 = 𝑉 → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) = ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) )
14		eqid	⊢ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) = ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
15	12 13 14	ovmpox2	⊢ ( ( 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ∈ V ) → ( 𝑆 ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) 𝑉 ) = ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
16	4 5 6 15	syl3anc	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑆 ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑣 ) , 𝑣 ∈ 𝒫 ( Base ‘ 𝑀 ) ↦ ( 𝑀 Σ_g ( 𝑥 ∈ 𝑣 ↦ ( ( 𝑠 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) ) 𝑉 ) = ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )
17	3 16	eqtrd	⊢ ( ( 𝑀 ∈ 𝑋 ∧ 𝑆 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑆 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σ_g ( 𝑥 ∈ 𝑉 ↦ ( ( 𝑆 ‘ 𝑥 ) ( ·_𝑠 ‘ 𝑀 ) 𝑥 ) ) ) )