Theorem lincval1

Description: The linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019)

	Ref	Expression
Hypotheses	lincval1.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	lincval1.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	lincval1.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lincval1.f	⊢ 𝐹 = { ⟨ 𝑉 , ( 0g ‘ 𝑆 ) ⟩ }
Assertion	lincval1	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 0g ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		lincval1.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		lincval1.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3		lincval1.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
4		lincval1.f	⊢ 𝐹 = { ⟨ 𝑉 , ( 0g ‘ 𝑆 ) ⟩ }
5		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
6	2 3 5	lmod0cl	⊢ ( 𝑀 ∈ LMod → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
7	6	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
8		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
9	1 2 3 8 4	lincvalsn	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ∧ ( 0g ‘ 𝑆 ) ∈ 𝑅 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( ( 0g ‘ 𝑆 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
10	7 9	mpd3an3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( ( 0g ‘ 𝑆 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) )
11		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
12	1 2 8 5 11	lmod0vs	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( ( 0g ‘ 𝑆 ) ( ·𝑠 ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) )
13	10 12	eqtrd	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 0g ‘ 𝑀 ) )