Theorem linc0scn0

Description: If a set contains the zero element of a module, there is a linear combination being 0 where not all scalars are 0. (Contributed by AV, 13-Apr-2019)

	Ref	Expression
Hypotheses	linc0scn0.b	|- B = ( Base ` M )
	linc0scn0.s	|- S = ( Scalar ` M )
	linc0scn0.0	|- .0. = ( 0g ` S )
	linc0scn0.1	|- .1. = ( 1r ` S )
	linc0scn0.z	|- Z = ( 0g ` M )
	linc0scn0.f	|- F = ( x e. V |-> if ( x = Z , .1. , .0. ) )
Assertion	linc0scn0	|- ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = Z )

Proof

Step	Hyp	Ref	Expression
1		linc0scn0.b	|- B = ( Base ` M )
2		linc0scn0.s	|- S = ( Scalar ` M )
3		linc0scn0.0	|- .0. = ( 0g ` S )
4		linc0scn0.1	|- .1. = ( 1r ` S )
5		linc0scn0.z	|- Z = ( 0g ` M )
6		linc0scn0.f	|- F = ( x e. V |-> if ( x = Z , .1. , .0. ) )
7		simpl	|- ( ( M e. LMod /\ V e. ~P B ) -> M e. LMod )
8	2	lmodring	|- ( M e. LMod -> S e. Ring )
9	2	eqcomi	|- ( Scalar ` M ) = S
10	9	fveq2i	|- ( Base ` ( Scalar ` M ) ) = ( Base ` S )
11	10 4	ringidcl	|- ( S e. Ring -> .1. e. ( Base ` ( Scalar ` M ) ) )
12	10 3	ring0cl	|- ( S e. Ring -> .0. e. ( Base ` ( Scalar ` M ) ) )
13	11 12	jca	|- ( S e. Ring -> ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) )
14	8 13	syl	|- ( M e. LMod -> ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) )
15	14	ad2antrr	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. V ) -> ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) )
16		ifcl	|- ( ( .1. e. ( Base ` ( Scalar ` M ) ) /\ .0. e. ( Base ` ( Scalar ` M ) ) ) -> if ( x = Z , .1. , .0. ) e. ( Base ` ( Scalar ` M ) ) )
17	15 16	syl	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ x e. V ) -> if ( x = Z , .1. , .0. ) e. ( Base ` ( Scalar ` M ) ) )
18	17 6	fmptd	|- ( ( M e. LMod /\ V e. ~P B ) -> F : V --> ( Base ` ( Scalar ` M ) ) )
19		fvex	|- ( Base ` ( Scalar ` M ) ) e. _V
20	19	a1i	|- ( M e. LMod -> ( Base ` ( Scalar ` M ) ) e. _V )
21		elmapg	|- ( ( ( Base ` ( Scalar ` M ) ) e. _V /\ V e. ~P B ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
22	20 21	sylan	|- ( ( M e. LMod /\ V e. ~P B ) -> ( F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) <-> F : V --> ( Base ` ( Scalar ` M ) ) ) )
23	18 22	mpbird	|- ( ( M e. LMod /\ V e. ~P B ) -> F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) )
24	1	pweqi	|- ~P B = ~P ( Base ` M )
25	24	eleq2i	|- ( V e. ~P B <-> V e. ~P ( Base ` M ) )
26	25	biimpi	|- ( V e. ~P B -> V e. ~P ( Base ` M ) )
27	26	adantl	|- ( ( M e. LMod /\ V e. ~P B ) -> V e. ~P ( Base ` M ) )
28		lincval	|- ( ( M e. LMod /\ F e. ( ( Base ` ( Scalar ` M ) ) ^m V ) /\ V e. ~P ( Base ` M ) ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
29	7 23 27 28	syl3anc	|- ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
30		simpr	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> v e. V )
31	4	fvexi	|- .1. e. _V
32	3	fvexi	|- .0. e. _V
33	31 32	ifex	|- if ( v = Z , .1. , .0. ) e. _V
34		eqeq1	|- ( x = v -> ( x = Z <-> v = Z ) )
35	34	ifbid	|- ( x = v -> if ( x = Z , .1. , .0. ) = if ( v = Z , .1. , .0. ) )
36	35 6	fvmptg	|- ( ( v e. V /\ if ( v = Z , .1. , .0. ) e. _V ) -> ( F ` v ) = if ( v = Z , .1. , .0. ) )
37	30 33 36	sylancl	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( F ` v ) = if ( v = Z , .1. , .0. ) )
38	37	oveq1d	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = ( if ( v = Z , .1. , .0. ) ( .s ` M ) v ) )
39		ovif	|- ( if ( v = Z , .1. , .0. ) ( .s ` M ) v ) = if ( v = Z , ( .1. ( .s ` M ) v ) , ( .0. ( .s ` M ) v ) )
40	39	a1i	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( if ( v = Z , .1. , .0. ) ( .s ` M ) v ) = if ( v = Z , ( .1. ( .s ` M ) v ) , ( .0. ( .s ` M ) v ) ) )
41		oveq2	|- ( v = Z -> ( .1. ( .s ` M ) v ) = ( .1. ( .s ` M ) Z ) )
42	41	adantl	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( .1. ( .s ` M ) v ) = ( .1. ( .s ` M ) Z ) )
43		eqid	|- ( Base ` S ) = ( Base ` S )
44	2 43 4	lmod1cl	|- ( M e. LMod -> .1. e. ( Base ` S ) )
45	44	ancli	|- ( M e. LMod -> ( M e. LMod /\ .1. e. ( Base ` S ) ) )
46	45	adantr	|- ( ( M e. LMod /\ V e. ~P B ) -> ( M e. LMod /\ .1. e. ( Base ` S ) ) )
47	46	ad2antrr	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( M e. LMod /\ .1. e. ( Base ` S ) ) )
48		eqid	|- ( .s ` M ) = ( .s ` M )
49	2 48 43 5	lmodvs0	|- ( ( M e. LMod /\ .1. e. ( Base ` S ) ) -> ( .1. ( .s ` M ) Z ) = Z )
50	47 49	syl	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( .1. ( .s ` M ) Z ) = Z )
51	42 50	eqtrd	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( .1. ( .s ` M ) v ) = Z )
52	7	adantr	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> M e. LMod )
53		elelpwi	|- ( ( v e. V /\ V e. ~P B ) -> v e. B )
54	53	expcom	|- ( V e. ~P B -> ( v e. V -> v e. B ) )
55	54	adantl	|- ( ( M e. LMod /\ V e. ~P B ) -> ( v e. V -> v e. B ) )
56	55	imp	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> v e. B )
57	1 2 48 3 5	lmod0vs	|- ( ( M e. LMod /\ v e. B ) -> ( .0. ( .s ` M ) v ) = Z )
58	52 56 57	syl2anc	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( .0. ( .s ` M ) v ) = Z )
59	58	adantr	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ -. v = Z ) -> ( .0. ( .s ` M ) v ) = Z )
60	51 59	ifeqda	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> if ( v = Z , ( .1. ( .s ` M ) v ) , ( .0. ( .s ` M ) v ) ) = Z )
61	38 40 60	3eqtrd	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = Z )
62	61	mpteq2dva	|- ( ( M e. LMod /\ V e. ~P B ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) = ( v e. V |-> Z ) )
63	62	oveq2d	|- ( ( M e. LMod /\ V e. ~P B ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) = ( M gsum ( v e. V |-> Z ) ) )
64		lmodgrp	|- ( M e. LMod -> M e. Grp )
65	64	grpmndd	|- ( M e. LMod -> M e. Mnd )
66	5	gsumz	|- ( ( M e. Mnd /\ V e. ~P B ) -> ( M gsum ( v e. V |-> Z ) ) = Z )
67	65 66	sylan	|- ( ( M e. LMod /\ V e. ~P B ) -> ( M gsum ( v e. V |-> Z ) ) = Z )
68	29 63 67	3eqtrd	|- ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = Z )