lbsacsbs

Description: Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	lbsacsbs.1	$⊢ A = LSubSp (W)$
	lbsacsbs.2	$⊢ N = mrCls (A)$
	lbsacsbs.3	$⊢ X = {Base}_{W}$
	lbsacsbs.4	$⊢ I = mrInd (A)$
	lbsacsbs.5	$⊢ J = LBasis (W)$
Assertion	lbsacsbs	$⊢ W \in LVec \to (S \in J \leftrightarrow (S \in I \land N (S) = X))$

Proof

Step	Hyp	Ref	Expression
1		lbsacsbs.1	$⊢ A = LSubSp (W)$
2		lbsacsbs.2	$⊢ N = mrCls (A)$
3		lbsacsbs.3	$⊢ X = {Base}_{W}$
4		lbsacsbs.4	$⊢ I = mrInd (A)$
5		lbsacsbs.5	$⊢ J = LBasis (W)$
6		eqid	$⊢ LSpan (W) = LSpan (W)$
7	3 5 6	islbs2	$⊢ W \in LVec \to (S \in J \leftrightarrow (S \subseteq X \land LSpan (W) (S) = X \land \forall x \in S \neg x \in LSpan (W) (S ∖ \{x\})))$
8		lveclmod	$⊢ W \in LVec \to W \in LMod$
9	1 6 2	mrclsp	$⊢ W \in LMod \to LSpan (W) = N$
10	8 9	syl	$⊢ W \in LVec \to LSpan (W) = N$
11	10	fveq1d	$⊢ W \in LVec \to LSpan (W) (S) = N (S)$
12	11	eqeq1d	$⊢ W \in LVec \to (LSpan (W) (S) = X \leftrightarrow N (S) = X)$
13	10	fveq1d	$⊢ W \in LVec \to LSpan (W) (S ∖ \{x\}) = N (S ∖ \{x\})$
14	13	eleq2d	$⊢ W \in LVec \to (x \in LSpan (W) (S ∖ \{x\}) \leftrightarrow x \in N (S ∖ \{x\}))$
15	14	notbid	$⊢ W \in LVec \to (\neg x \in LSpan (W) (S ∖ \{x\}) \leftrightarrow \neg x \in N (S ∖ \{x\}))$
16	15	ralbidv	$⊢ W \in LVec \to (\forall x \in S \neg x \in LSpan (W) (S ∖ \{x\}) \leftrightarrow \forall x \in S \neg x \in N (S ∖ \{x\}))$
17	12 16	3anbi23d	$⊢ W \in LVec \to ((S \subseteq X \land LSpan (W) (S) = X \land \forall x \in S \neg x \in LSpan (W) (S ∖ \{x\})) \leftrightarrow (S \subseteq X \land N (S) = X \land \forall x \in S \neg x \in N (S ∖ \{x\})))$
18		3anan32	$⊢ (S \subseteq X \land N (S) = X \land \forall x \in S \neg x \in N (S ∖ \{x\})) \leftrightarrow ((S \subseteq X \land \forall x \in S \neg x \in N (S ∖ \{x\})) \land N (S) = X)$
19	3 1	lssmre	$⊢ W \in LMod \to A \in Moore (X)$
20	2 4	ismri	$⊢ A \in Moore (X) \to (S \in I \leftrightarrow (S \subseteq X \land \forall x \in S \neg x \in N (S ∖ \{x\})))$
21	8 19 20	3syl	$⊢ W \in LVec \to (S \in I \leftrightarrow (S \subseteq X \land \forall x \in S \neg x \in N (S ∖ \{x\})))$
22	21	anbi1d	$⊢ W \in LVec \to ((S \in I \land N (S) = X) \leftrightarrow ((S \subseteq X \land \forall x \in S \neg x \in N (S ∖ \{x\})) \land N (S) = X))$
23	18 22	bitr4id	$⊢ W \in LVec \to ((S \subseteq X \land N (S) = X \land \forall x \in S \neg x \in N (S ∖ \{x\})) \leftrightarrow (S \in I \land N (S) = X))$
24	7 17 23	3bitrd	$⊢ W \in LVec \to (S \in J \leftrightarrow (S \in I \land N (S) = X))$

Metamath Proof Explorer

Theorem lbsacsbs

Proof