lssacsex

Description: In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs by lspsolv . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	lssacsex.1	$⊢ A = LSubSp (W)$
	lssacsex.2	$⊢ N = mrCls (A)$
	lssacsex.3	$⊢ X = {Base}_{W}$
Assertion	lssacsex	$⊢ W \in LVec \to (A \in ACS (X) \land \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\}))$

Proof

Step	Hyp	Ref	Expression
1		lssacsex.1	$⊢ A = LSubSp (W)$
2		lssacsex.2	$⊢ N = mrCls (A)$
3		lssacsex.3	$⊢ X = {Base}_{W}$
4		lveclmod	$⊢ W \in LVec \to W \in LMod$
5	3 1	lssacs	$⊢ W \in LMod \to A \in ACS (X)$
6	4 5	syl	$⊢ W \in LVec \to A \in ACS (X)$
7		simplll	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to W \in LVec$
8		simpllr	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to s \in 𝒫 X$
9	8	elpwid	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to s \subseteq X$
10		simplr	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to y \in X$
11		simpr	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to z \in (N (s \cup \{y\}) ∖ N (s))$
12		eqid	$⊢ LSpan (W) = LSpan (W)$
13	1 12 2	mrclsp	$⊢ W \in LMod \to LSpan (W) = N$
14	7 4 13	3syl	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to LSpan (W) = N$
15	14	fveq1d	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to LSpan (W) (s \cup \{y\}) = N (s \cup \{y\})$
16	14	fveq1d	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to LSpan (W) (s) = N (s)$
17	15 16	difeq12d	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to LSpan (W) (s \cup \{y\}) ∖ LSpan (W) (s) = N (s \cup \{y\}) ∖ N (s)$
18	11 17	eleqtrrd	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to z \in (LSpan (W) (s \cup \{y\}) ∖ LSpan (W) (s))$
19	3 1 12	lspsolv	$⊢ (W \in LVec \land (s \subseteq X \land y \in X \land z \in (LSpan (W) (s \cup \{y\}) ∖ LSpan (W) (s)))) \to y \in LSpan (W) (s \cup \{z\})$
20	7 9 10 18 19	syl13anc	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to y \in LSpan (W) (s \cup \{z\})$
21	14	fveq1d	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to LSpan (W) (s \cup \{z\}) = N (s \cup \{z\})$
22	20 21	eleqtrd	$⊢ (((W \in LVec \land s \in 𝒫 X) \land y \in X) \land z \in (N (s \cup \{y\}) ∖ N (s))) \to y \in N (s \cup \{z\})$
23	22	ralrimiva	$⊢ ((W \in LVec \land s \in 𝒫 X) \land y \in X) \to \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
24	23	ralrimiva	$⊢ (W \in LVec \land s \in 𝒫 X) \to \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
25	24	ralrimiva	$⊢ W \in LVec \to \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\})$
26	6 25	jca	$⊢ W \in LVec \to (A \in ACS (X) \land \forall s \in 𝒫 X \forall y \in X \forall z \in (N (s \cup \{y\}) ∖ N (s)) y \in N (s \cup \{z\}))$

Metamath Proof Explorer

Theorem lssacsex

Proof