Metamath Proof Explorer

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	$⊢ ((M \in LMod \land Scalar (M) \in NzRing) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to S linDepS M$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((M \in LMod \land Scalar (M) \in NzRing) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to M \in LMod$
2		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
3	2	isnzr2hash	$⊢ Scalar (M) \in NzRing \leftrightarrow (Scalar (M) \in Ring \land 1 < \|{Base}_{Scalar (M)}\|)$
4	3	simprbi	$⊢ Scalar (M) \in NzRing \to 1 < \|{Base}_{Scalar (M)}\|$
5	4	adantl	$⊢ (M \in LMod \land Scalar (M) \in NzRing) \to 1 < \|{Base}_{Scalar (M)}\|$
6	5	3ad2ant1	$⊢ ((M \in LMod \land Scalar (M) \in NzRing) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to 1 < \|{Base}_{Scalar (M)}\|$
7	1 6	jca	$⊢ ((M \in LMod \land Scalar (M) \in NzRing) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to (M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|)$
8		el0ldep	$⊢ ((M \in LMod \land 1 < \|{Base}_{Scalar (M)}\|) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to S linDepS M$
9	7 8	syld3an1	$⊢ ((M \in LMod \land Scalar (M) \in NzRing) \land S \in 𝒫 {Base}_{M} \land 0_{M} \in S) \to S linDepS M$