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	bilani	|- ( ( M e. LMod /\ V e. ~P B ) -> V e. ~P ( Base ` M ) )
27		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 ) ) ) )
28	7 23 26 27	syl3anc	|- ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) )
29		simpr	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> v e. V )
30	4	fvexi	|- .1. e. _V
31	3	fvexi	|- .0. e. _V
32	30 31	ifex	|- if ( v = Z , .1. , .0. ) e. _V
33		eqeq1	|- ( x = v -> ( x = Z <-> v = Z ) )
34	33	ifbid	|- ( x = v -> if ( x = Z , .1. , .0. ) = if ( v = Z , .1. , .0. ) )
35	34 6	fvmptg	|- ( ( v e. V /\ if ( v = Z , .1. , .0. ) e. _V ) -> ( F ` v ) = if ( v = Z , .1. , .0. ) )
36	29 32 35	sylancl	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( F ` v ) = if ( v = Z , .1. , .0. ) )
37	36	oveq1d	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = ( if ( v = Z , .1. , .0. ) ( .s ` M ) v ) )
38		ovif	|- ( if ( v = Z , .1. , .0. ) ( .s ` M ) v ) = if ( v = Z , ( .1. ( .s ` M ) v ) , ( .0. ( .s ` M ) v ) )
39	38	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 ) ) )
40		oveq2	|- ( v = Z -> ( .1. ( .s ` M ) v ) = ( .1. ( .s ` M ) Z ) )
41	40	adantl	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( .1. ( .s ` M ) v ) = ( .1. ( .s ` M ) Z ) )
42		eqid	|- ( Base ` S ) = ( Base ` S )
43	2 42 4	lmod1cl	|- ( M e. LMod -> .1. e. ( Base ` S ) )
44	43	ancli	|- ( M e. LMod -> ( M e. LMod /\ .1. e. ( Base ` S ) ) )
45	44	adantr	|- ( ( M e. LMod /\ V e. ~P B ) -> ( M e. LMod /\ .1. e. ( Base ` S ) ) )
46	45	ad2antrr	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( M e. LMod /\ .1. e. ( Base ` S ) ) )
47		eqid	|- ( .s ` M ) = ( .s ` M )
48	2 47 42 5	lmodvs0	|- ( ( M e. LMod /\ .1. e. ( Base ` S ) ) -> ( .1. ( .s ` M ) Z ) = Z )
49	46 48	syl	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( .1. ( .s ` M ) Z ) = Z )
50	41 49	eqtrd	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ v = Z ) -> ( .1. ( .s ` M ) v ) = Z )
51	7	adantr	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> M e. LMod )
52		elelpwi	|- ( ( v e. V /\ V e. ~P B ) -> v e. B )
53	52	expcom	|- ( V e. ~P B -> ( v e. V -> v e. B ) )
54	53	adantl	|- ( ( M e. LMod /\ V e. ~P B ) -> ( v e. V -> v e. B ) )
55	54	imp	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> v e. B )
56	1 2 47 3 5	lmod0vs	|- ( ( M e. LMod /\ v e. B ) -> ( .0. ( .s ` M ) v ) = Z )
57	51 55 56	syl2anc	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( .0. ( .s ` M ) v ) = Z )
58	57	adantr	|- ( ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) /\ -. v = Z ) -> ( .0. ( .s ` M ) v ) = Z )
59	50 58	ifeqda	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> if ( v = Z , ( .1. ( .s ` M ) v ) , ( .0. ( .s ` M ) v ) ) = Z )
60	37 39 59	3eqtrd	|- ( ( ( M e. LMod /\ V e. ~P B ) /\ v e. V ) -> ( ( F ` v ) ( .s ` M ) v ) = Z )
61	60	mpteq2dva	|- ( ( M e. LMod /\ V e. ~P B ) -> ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) = ( v e. V |-> Z ) )
62	61	oveq2d	|- ( ( M e. LMod /\ V e. ~P B ) -> ( M gsum ( v e. V |-> ( ( F ` v ) ( .s ` M ) v ) ) ) = ( M gsum ( v e. V |-> Z ) ) )
63		lmodgrp	|- ( M e. LMod -> M e. Grp )
64	63	grpmndd	|- ( M e. LMod -> M e. Mnd )
65	5	gsumz	|- ( ( M e. Mnd /\ V e. ~P B ) -> ( M gsum ( v e. V |-> Z ) ) = Z )
66	64 65	sylan	|- ( ( M e. LMod /\ V e. ~P B ) -> ( M gsum ( v e. V |-> Z ) ) = Z )
67	28 62 66	3eqtrd	|- ( ( M e. LMod /\ V e. ~P B ) -> ( F ( linC ` M ) V ) = Z )