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	|- B = ( Base ` M )
	lincval1.s	|- S = ( Scalar ` M )
	lincval1.r	|- R = ( Base ` S )
	lincval1.f	|- F = { <. V , ( 0g ` S ) >. }
Assertion	lcosn0	|- ( ( M e. LMod /\ V e. B ) -> ( F e. ( R ^m { V } ) /\ F finSupp ( 0g ` S ) /\ ( F ( linC ` M ) { V } ) = ( 0g ` M ) ) )

Proof

Step	Hyp	Ref	Expression
1		lincval1.b	|- B = ( Base ` M )
2		lincval1.s	|- S = ( Scalar ` M )
3		lincval1.r	|- R = ( Base ` S )
4		lincval1.f	|- F = { <. V , ( 0g ` S ) >. }
5		simpr	|- ( ( M e. LMod /\ V e. B ) -> V e. B )
6		eqid	|- ( 0g ` S ) = ( 0g ` S )
7	2 3 6	lmod0cl	|- ( M e. LMod -> ( 0g ` S ) e. R )
8	7	adantr	|- ( ( M e. LMod /\ V e. B ) -> ( 0g ` S ) e. R )
9	3	fvexi	|- R e. _V
10	9	a1i	|- ( ( M e. LMod /\ V e. B ) -> R e. _V )
11	4	mapsnop	|- ( ( V e. B /\ ( 0g ` S ) e. R /\ R e. _V ) -> F e. ( R ^m { V } ) )
12	5 8 10 11	syl3anc	|- ( ( M e. LMod /\ V e. B ) -> F e. ( R ^m { V } ) )
13		elmapi	|- ( F e. ( R ^m { V } ) -> F : { V } --> R )
14	12 13	syl	|- ( ( M e. LMod /\ V e. B ) -> F : { V } --> R )
15		snfi	|- { V } e. Fin
16	15	a1i	|- ( ( M e. LMod /\ V e. B ) -> { V } e. Fin )
17		fvex	|- ( 0g ` S ) e. _V
18	17	a1i	|- ( ( M e. LMod /\ V e. B ) -> ( 0g ` S ) e. _V )
19	14 16 18	fdmfifsupp	|- ( ( M e. LMod /\ V e. B ) -> F finSupp ( 0g ` S ) )
20	1 2 3 4	lincval1	|- ( ( M e. LMod /\ V e. B ) -> ( F ( linC ` M ) { V } ) = ( 0g ` M ) )
21	12 19 20	3jca	|- ( ( M e. LMod /\ V e. B ) -> ( F e. ( R ^m { V } ) /\ F finSupp ( 0g ` S ) /\ ( F ( linC ` M ) { V } ) = ( 0g ` M ) ) )