el0ldep

Description: A set containing the zero element of a module is always linearly dependent, if the underlying ring has at least two elements. (Contributed by AV, 13-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

		Ref	Expression
	Assertion	el0ldep	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑆 linDepS 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
2		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
3		eqid	⊢ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0_g ‘ ( Scalar ‘ 𝑀 ) )
4		eqid	⊢ ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) = ( 1_r ‘ ( Scalar ‘ 𝑀 ) )
5		eqeq1	⊢ ( 𝑠 = 𝑦 → ( 𝑠 = ( 0_g ‘ 𝑀 ) ↔ 𝑦 = ( 0_g ‘ 𝑀 ) ) )
6	5	ifbid	⊢ ( 𝑠 = 𝑦 → if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) = if ( 𝑦 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
7	6	cbvmptv	⊢ ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) = ( 𝑦 ∈ 𝑆 ↦ if ( 𝑦 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
8	1 2 3 4 7	mptcfsupp	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) )
9	8	3adant1r	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) )
10		simp1l	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑀 ∈ LMod )
11		simp2	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) )
12		eqid	⊢ ( 0_g ‘ 𝑀 ) = ( 0_g ‘ 𝑀 )
13		eqid	⊢ ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
14	1 2 3 4 12 13	linc0scn0	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) )
15	10 11 14	syl2anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) )
16		simp3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 0_g ‘ 𝑀 ) ∈ 𝑆 )
17		fveq2	⊢ ( 𝑥 = ( 0_g ‘ 𝑀 ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ ( 0_g ‘ 𝑀 ) ) )
18	17	neeq1d	⊢ ( 𝑥 = ( 0_g ‘ 𝑀 ) → ( ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ ( 0_g ‘ 𝑀 ) ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
19	18	adantl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) ∧ 𝑥 = ( 0_g ‘ 𝑀 ) ) → ( ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ ( 0_g ‘ 𝑀 ) ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
20		iftrue	⊢ ( 𝑠 = ( 0_g ‘ 𝑀 ) → if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) = ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) )
21		fvexd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
22	13 20 16 21	fvmptd3	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ ( 0_g ‘ 𝑀 ) ) = ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) )
23	2	lmodring	⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) ∈ Ring )
24	23	anim1i	⊢ ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
25	24	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
26		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
27	26 4 3	ring1ne0	⊢ ( ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) )
28	25 27	syl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) )
29	22 28	eqnetrd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ ( 0_g ‘ 𝑀 ) ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) )
30	16 19 29	rspcedvd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝑆 ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) )
31	2 26 4	lmod1cl	⊢ ( 𝑀 ∈ LMod → ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
32	2 26 3	lmod0cl	⊢ ( 𝑀 ∈ LMod → ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
33	31 32	ifcld	⊢ ( 𝑀 ∈ LMod → if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
34	33	adantr	⊢ ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) → if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
35	34	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
36	35	adantr	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) ∧ 𝑠 ∈ 𝑆 ) → if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
37	36	fmpttd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) : 𝑆 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
38		fvexd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
39	38 11	elmapd	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑆 ) ↔ ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) : 𝑆 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
40	37 39	mpbird	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑆 ) )
41		breq1	⊢ ( 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑓 finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
42		oveq1	⊢ ( 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) )
43	42	eqeq1d	⊢ ( 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ↔ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ) )
44		fveq1	⊢ ( 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) )
45	44	neeq1d	⊢ ( 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
46	45	rexbidv	⊢ ( 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ∃ 𝑥 ∈ 𝑆 ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
47	41 43 46	3anbi123d	⊢ ( 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( 𝑓 finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ↔ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
48	47	adantl	⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) ∧ 𝑓 = ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ) → ( ( 𝑓 finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ↔ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
49	40 48	rspcedv	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( ( 𝑠 ∈ 𝑆 ↦ if ( 𝑠 = ( 0_g ‘ 𝑀 ) , ( 1_r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) → ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑆 ) ( 𝑓 finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
50	9 15 30 49	mp3and	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑆 ) ( 𝑓 finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) )
51	1 12 2 26 3	islindeps	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑆 ) ( 𝑓 finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
52	10 11 51	syl2anc	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → ( 𝑆 linDepS 𝑀 ↔ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑_m 𝑆 ) ( 𝑓 finSupp ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 𝑓 ( linC ‘ 𝑀 ) 𝑆 ) = ( 0_g ‘ 𝑀 ) ∧ ∃ 𝑥 ∈ 𝑆 ( 𝑓 ‘ 𝑥 ) ≠ ( 0_g ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
53	50 52	mpbird	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0_g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑆 linDepS 𝑀 )

Metamath Proof Explorer

Theorem el0ldep

Proof