lindssnlvec

Description: A singleton not containing the zero element of a vector space is always linearly independent. (Contributed by AV, 16-Apr-2019) (Revised by AV, 28-Apr-2019)

		Ref	Expression
	Assertion	lindssnlvec	$⊢ (M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \to \{S\} linIndS M$

Proof

Step	Hyp	Ref	Expression
1		eldifsni	$⊢ s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) \to s \neq 0_{Scalar (M)}$
2	1	adantl	$⊢ ((M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \land s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\})) \to s \neq 0_{Scalar (M)}$
3		simpl3	$⊢ ((M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \land s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\})) \to S \neq 0_{M}$
4		eqid	$⊢ {Base}_{M} = {Base}_{M}$
5		eqid	$⊢ \cdot_{M} = \cdot_{M}$
6		eqid	$⊢ Scalar (M) = Scalar (M)$
7		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
8		eqid	$⊢ 0_{Scalar (M)} = 0_{Scalar (M)}$
9		eqid	$⊢ 0_{M} = 0_{M}$
10		simpl1	$⊢ ((M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \land s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\})) \to M \in LVec$
11		eldifi	$⊢ s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) \to s \in {Base}_{Scalar (M)}$
12	11	adantl	$⊢ ((M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \land s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\})) \to s \in {Base}_{Scalar (M)}$
13		simpl2	$⊢ ((M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \land s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\})) \to S \in {Base}_{M}$
14	4 5 6 7 8 9 10 12 13	lvecvsn0	$⊢ ((M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \land s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\})) \to (s \cdot_{M} S \neq 0_{M} \leftrightarrow (s \neq 0_{Scalar (M)} \land S \neq 0_{M}))$
15	2 3 14	mpbir2and	$⊢ ((M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \land s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\})) \to s \cdot_{M} S \neq 0_{M}$
16	15	ralrimiva	$⊢ (M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \to \forall s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) s \cdot_{M} S \neq 0_{M}$
17		lveclmod	$⊢ M \in LVec \to M \in LMod$
18	17	anim1i	$⊢ (M \in LVec \land S \in {Base}_{M}) \to (M \in LMod \land S \in {Base}_{M})$
19	18	3adant3	$⊢ (M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \to (M \in LMod \land S \in {Base}_{M})$
20	4 6 7 8 9 5	snlindsntor	$⊢ (M \in LMod \land S \in {Base}_{M}) \to (\forall s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) s \cdot_{M} S \neq 0_{M} \leftrightarrow \{S\} linIndS M)$
21	19 20	syl	$⊢ (M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \to (\forall s \in ({Base}_{Scalar (M)} ∖ \{0_{Scalar (M)}\}) s \cdot_{M} S \neq 0_{M} \leftrightarrow \{S\} linIndS M)$
22	16 21	mpbid	$⊢ (M \in LVec \land S \in {Base}_{M} \land S \neq 0_{M}) \to \{S\} linIndS M$

Metamath Proof Explorer

Theorem lindssnlvec

Proof