Theorem lcosn0

Description: Properties of a linear combination over a singleton mapping to 0. (Contributed by AV, 12-Apr-2019) (Revised by AV, 28-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		lincval1.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		lincval1.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3		lincval1.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
4		lincval1.f	⊢ 𝐹 = { ⟨ 𝑉 , ( 0g ‘ 𝑆 ) ⟩ }
5		simpr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → 𝑉 ∈ 𝐵 )
6		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
7	2 3 6	lmod0cl	⊢ ( 𝑀 ∈ LMod → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
8	7	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
9	3	fvexi	⊢ 𝑅 ∈ V
10	9	a1i	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → 𝑅 ∈ V )
11	4	mapsnop	⊢ ( ( 𝑉 ∈ 𝐵 ∧ ( 0g ‘ 𝑆 ) ∈ 𝑅 ∧ 𝑅 ∈ V ) → 𝐹 ∈ ( 𝑅 ↑m { 𝑉 } ) )
12	5 8 10 11	syl3anc	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → 𝐹 ∈ ( 𝑅 ↑m { 𝑉 } ) )
13		elmapi	⊢ ( 𝐹 ∈ ( 𝑅 ↑m { 𝑉 } ) → 𝐹 : { 𝑉 } ⟶ 𝑅 )
14	12 13	syl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → 𝐹 : { 𝑉 } ⟶ 𝑅 )
15		snfi	⊢ { 𝑉 } ∈ Fin
16	15	a1i	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → { 𝑉 } ∈ Fin )
17		fvex	⊢ ( 0g ‘ 𝑆 ) ∈ V
18	17	a1i	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 0g ‘ 𝑆 ) ∈ V )
19	14 16 18	fdmfifsupp	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → 𝐹 finSupp ( 0g ‘ 𝑆 ) )
20	1 2 3 4	lincval1	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 0g ‘ 𝑀 ) )
21	12 19 20	3jca	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ∈ ( 𝑅 ↑m { 𝑉 } ) ∧ 𝐹 finSupp ( 0g ‘ 𝑆 ) ∧ ( 𝐹 ( linC ‘ 𝑀 ) { 𝑉 } ) = ( 0g ‘ 𝑀 ) ) )