Theorem lincval0

Description: The value of an empty linear combination. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Assertion	lincval0	⊢ ( 𝑀 ∈ 𝑋 → ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1	snid	⊢ ∅ ∈ { ∅ }
3		fvex	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
4		map0e	⊢ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = 1o )
5	3 4	mp1i	⊢ ( 𝑀 ∈ 𝑋 → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = 1o )
6		df1o2	⊢ 1o = { ∅ }
7	5 6	eqtrdi	⊢ ( 𝑀 ∈ 𝑋 → ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) = { ∅ } )
8	2 7	eleqtrrid	⊢ ( 𝑀 ∈ 𝑋 → ∅ ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) )
9		0elpw	⊢ ∅ ∈ 𝒫 ( Base ‘ 𝑀 )
10	9	a1i	⊢ ( 𝑀 ∈ 𝑋 → ∅ ∈ 𝒫 ( Base ‘ 𝑀 ) )
11		lincval	⊢ ( ( 𝑀 ∈ 𝑋 ∧ ∅ ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m ∅ ) ∧ ∅ ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 𝑀 Σg ( 𝑣 ∈ ∅ ↦ ( ( ∅ ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
12	8 10 11	mpd3an23	⊢ ( 𝑀 ∈ 𝑋 → ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 𝑀 Σg ( 𝑣 ∈ ∅ ↦ ( ( ∅ ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
13		mpt0	⊢ ( 𝑣 ∈ ∅ ↦ ( ( ∅ ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ∅
14	13	a1i	⊢ ( 𝑀 ∈ 𝑋 → ( 𝑣 ∈ ∅ ↦ ( ( ∅ ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ∅ )
15	14	oveq2d	⊢ ( 𝑀 ∈ 𝑋 → ( 𝑀 Σg ( 𝑣 ∈ ∅ ↦ ( ( ∅ ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( 𝑀 Σg ∅ ) )
16		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
17	16	gsum0	⊢ ( 𝑀 Σg ∅ ) = ( 0g ‘ 𝑀 )
18	15 17	eqtrdi	⊢ ( 𝑀 ∈ 𝑋 → ( 𝑀 Σg ( 𝑣 ∈ ∅ ↦ ( ( ∅ ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( 0g ‘ 𝑀 ) )
19	12 18	eqtrd	⊢ ( 𝑀 ∈ 𝑋 → ( ∅ ( linC ‘ 𝑀 ) ∅ ) = ( 0g ‘ 𝑀 ) )