Theorem el0ldepsnzr

Description: A set containing the zero element of a module over a nonzero ring is always linearly dependent. (Contributed by AV, 14-Apr-2019) (Revised by AV, 27-Apr-2019)

	Ref	Expression
Assertion	el0ldepsnzr	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ NzRing ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑆 linDepS 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		simp1l	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ NzRing ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑀 ∈ LMod )
2		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
3	2	isnzr2hash	⊢ ( ( Scalar ‘ 𝑀 ) ∈ NzRing ↔ ( ( Scalar ‘ 𝑀 ) ∈ Ring ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
4	3	simprbi	⊢ ( ( Scalar ‘ 𝑀 ) ∈ NzRing → 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
5	4	adantl	⊢ ( ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ NzRing ) → 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
6	5	3ad2ant1	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ NzRing ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ) → 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
7	1 6	jca	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ NzRing ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ) → ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) )
8		el0ldep	⊢ ( ( ( 𝑀 ∈ LMod ∧ 1 < ( ♯ ‘ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑆 linDepS 𝑀 )
9	7 8	syld3an1	⊢ ( ( ( 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) ∈ NzRing ) ∧ 𝑆 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ) → 𝑆 linDepS 𝑀 )