lssats2

Description: A way to express atomisticity (a subspace is the union of its atoms). (Contributed by NM, 3-Feb-2015)

	Ref	Expression
Hypotheses	lssats2.s	$⊢ S = LSubSp (W)$
	lssats2.n	$⊢ N = LSpan (W)$
	lssats2.w	$⊢ φ \to W \in LMod$
	lssats2.u	$⊢ φ \to U \in S$
Assertion	lssats2	$⊢ φ \to U = ⋃_{x \in U} N (\{x\})$

Proof

Step	Hyp	Ref	Expression
1		lssats2.s	$⊢ S = LSubSp (W)$
2		lssats2.n	$⊢ N = LSpan (W)$
3		lssats2.w	$⊢ φ \to W \in LMod$
4		lssats2.u	$⊢ φ \to U \in S$
5		simpr	$⊢ (φ \land y \in U) \to y \in U$
6	3	adantr	$⊢ (φ \land y \in U) \to W \in LMod$
7		eqid	$⊢ {Base}_{W} = {Base}_{W}$
8	7 1	lssel	$⊢ (U \in S \land y \in U) \to y \in {Base}_{W}$
9	4 8	sylan	$⊢ (φ \land y \in U) \to y \in {Base}_{W}$
10	7 2	lspsnid	$⊢ (W \in LMod \land y \in {Base}_{W}) \to y \in N (\{y\})$
11	6 9 10	syl2anc	$⊢ (φ \land y \in U) \to y \in N (\{y\})$
12		sneq	$⊢ x = y \to \{x\} = \{y\}$
13	12	fveq2d	$⊢ x = y \to N (\{x\}) = N (\{y\})$
14	13	eleq2d	$⊢ x = y \to (y \in N (\{x\}) \leftrightarrow y \in N (\{y\}))$
15	14	rspcev	$⊢ (y \in U \land y \in N (\{y\})) \to \exists x \in U y \in N (\{x\})$
16	5 11 15	syl2anc	$⊢ (φ \land y \in U) \to \exists x \in U y \in N (\{x\})$
17	16	ex	$⊢ φ \to (y \in U \to \exists x \in U y \in N (\{x\}))$
18	3	adantr	$⊢ (φ \land x \in U) \to W \in LMod$
19	4	adantr	$⊢ (φ \land x \in U) \to U \in S$
20		simpr	$⊢ (φ \land x \in U) \to x \in U$
21	1 2 18 19 20	lspsnel5a	$⊢ (φ \land x \in U) \to N (\{x\}) \subseteq U$
22	21	sseld	$⊢ (φ \land x \in U) \to (y \in N (\{x\}) \to y \in U)$
23	22	rexlimdva	$⊢ φ \to (\exists x \in U y \in N (\{x\}) \to y \in U)$
24	17 23	impbid	$⊢ φ \to (y \in U \leftrightarrow \exists x \in U y \in N (\{x\}))$
25		eliun	$⊢ y \in ⋃_{x \in U} N (\{x\}) \leftrightarrow \exists x \in U y \in N (\{x\})$
26	24 25	bitr4di	$⊢ φ \to (y \in U \leftrightarrow y \in ⋃_{x \in U} N (\{x\}))$
27	26	eqrdv	$⊢ φ \to U = ⋃_{x \in U} N (\{x\})$

Metamath Proof Explorer

Theorem lssats2

Proof