lindszr

Description: Any subset of a module over a zero ring is always linearly independent. (Contributed by AV, 27-Apr-2019)

		Ref	Expression
	Assertion	lindszr	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing \land S \in 𝒫 {Base}_{M}) \to S linIndS M$

Step	Hyp	Ref	Expression
1		simp2	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing \land S \in 𝒫 {Base}_{M}) \to \neg Scalar (M) \in NzRing$
2		eqid	$⊢ Scalar (M) = Scalar (M)$
3	2	lmodring	$⊢ M \in LMod \to Scalar (M) \in Ring$
4	3	3ad2ant1	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing \land S \in 𝒫 {Base}_{M}) \to Scalar (M) \in Ring$
5		0ringnnzr	$⊢ Scalar (M) \in Ring \to (\|{Base}_{Scalar (M)}\| = 1 \leftrightarrow \neg Scalar (M) \in NzRing)$
6	4 5	syl	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing \land S \in 𝒫 {Base}_{M}) \to (\|{Base}_{Scalar (M)}\| = 1 \leftrightarrow \neg Scalar (M) \in NzRing)$
7	1 6	mpbird	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing \land S \in 𝒫 {Base}_{M}) \to \|{Base}_{Scalar (M)}\| = 1$
8	7	olcd	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing \land S \in 𝒫 {Base}_{M}) \to (\|{Base}_{Scalar (M)}\| = 0 \lor \|{Base}_{Scalar (M)}\| = 1)$
9		eqid	$⊢ {Base}_{M} = {Base}_{M}$
10		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
11	9 2 10	lindsrng01	$⊢ (M \in LMod \land (\|{Base}_{Scalar (M)}\| = 0 \lor \|{Base}_{Scalar (M)}\| = 1) \land S \in 𝒫 {Base}_{M}) \to S linIndS M$
12	8 11	syld3an2	$⊢ (M \in LMod \land \neg Scalar (M) \in NzRing \land S \in 𝒫 {Base}_{M}) \to S linIndS M$

Metamath Proof Explorer