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	⊢ 𝐵 = ( Base ‘ 𝑀 )
	linc0scn0.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	linc0scn0.0	⊢ 0 = ( 0g ‘ 𝑆 )
	linc0scn0.1	⊢ 1 = ( 1r ‘ 𝑆 )
	linc0scn0.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
	linc0scn0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑍 , 1 , 0 ) )
Assertion	linc0scn0	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		linc0scn0.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		linc0scn0.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3		linc0scn0.0	⊢ 0 = ( 0g ‘ 𝑆 )
4		linc0scn0.1	⊢ 1 = ( 1r ‘ 𝑆 )
5		linc0scn0.z	⊢ 𝑍 = ( 0g ‘ 𝑀 )
6		linc0scn0.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑍 , 1 , 0 ) )
7		simpl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑀 ∈ LMod )
8	2	lmodring	⊢ ( 𝑀 ∈ LMod → 𝑆 ∈ Ring )
9	2	eqcomi	⊢ ( Scalar ‘ 𝑀 ) = 𝑆
10	9	fveq2i	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
11	10 4	ringidcl	⊢ ( 𝑆 ∈ Ring → 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
12	10 3	ring0cl	⊢ ( 𝑆 ∈ Ring → 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
13	11 12	jca	⊢ ( 𝑆 ∈ Ring → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
14	8 13	syl	⊢ ( 𝑀 ∈ LMod → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
15	14	ad2antrr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
16		ifcl	⊢ ( ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) → if ( 𝑥 = 𝑍 , 1 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
17	15 16	syl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) → if ( 𝑥 = 𝑍 , 1 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
18	17 6	fmptd	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
19		fvex	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
20	19	a1i	⊢ ( 𝑀 ∈ LMod → ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
21		elmapg	⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
22	20 21	sylan	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
23	18 22	mpbird	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
24	1	pweqi	⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
25	24	eleq2i	⊢ ( 𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
26	25	biimpi	⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
27	26	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
28		lincval	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
29	7 23 27 28	syl3anc	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
30		simpr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
31	4	fvexi	⊢ 1 ∈ V
32	3	fvexi	⊢ 0 ∈ V
33	31 32	ifex	⊢ if ( 𝑣 = 𝑍 , 1 , 0 ) ∈ V
34		eqeq1	⊢ ( 𝑥 = 𝑣 → ( 𝑥 = 𝑍 ↔ 𝑣 = 𝑍 ) )
35	34	ifbid	⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑍 , 1 , 0 ) = if ( 𝑣 = 𝑍 , 1 , 0 ) )
36	35 6	fvmptg	⊢ ( ( 𝑣 ∈ 𝑉 ∧ if ( 𝑣 = 𝑍 , 1 , 0 ) ∈ V ) → ( 𝐹 ‘ 𝑣 ) = if ( 𝑣 = 𝑍 , 1 , 0 ) )
37	30 33 36	sylancl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) = if ( 𝑣 = 𝑍 , 1 , 0 ) )
38	37	oveq1d	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( if ( 𝑣 = 𝑍 , 1 , 0 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
39		ovif	⊢ ( if ( 𝑣 = 𝑍 , 1 , 0 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = if ( 𝑣 = 𝑍 , ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) , ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
40	39	a1i	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( if ( 𝑣 = 𝑍 , 1 , 0 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = if ( 𝑣 = 𝑍 , ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) , ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
41		oveq2	⊢ ( 𝑣 = 𝑍 → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) )
42	41	adantl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) )
43		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
44	2 43 4	lmod1cl	⊢ ( 𝑀 ∈ LMod → 1 ∈ ( Base ‘ 𝑆 ) )
45	44	ancli	⊢ ( 𝑀 ∈ LMod → ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) )
46	45	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) )
47	46	ad2antrr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) )
48		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
49	2 48 43 5	lmodvs0	⊢ ( ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) = 𝑍 )
50	47 49	syl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) = 𝑍 )
51	42 50	eqtrd	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
52	7	adantr	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
53		elelpwi	⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑣 ∈ 𝐵 )
54	53	expcom	⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
55	54	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
56	55	imp	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
57	1 2 48 3 5	lmod0vs	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
58	52 56 57	syl2anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
59	58	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ ¬ 𝑣 = 𝑍 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
60	51 59	ifeqda	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → if ( 𝑣 = 𝑍 , ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) , ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = 𝑍 )
61	38 40 60	3eqtrd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
62	61	mpteq2dva	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) )
63	62	oveq2d	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) )
64		lmodgrp	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
65	64	grpmndd	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
66	5	gsumz	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
67	65 66	sylan	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
68	29 63 67	3eqtrd	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 )