lssats

Description: The lattice of subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of MaedaMaeda p. 70. Hypothesis ( shatomistici analog.) (Contributed by NM, 9-Apr-2014)

	Ref	Expression
Hypotheses	lssats.s	$⊢ S = LSubSp (W)$
	lssats.n	$⊢ N = LSpan (W)$
	lssats.a	$⊢ A = LSAtoms (W)$
Assertion	lssats	$⊢ (W \in LMod \land U \in S) \to U = N (⋃ \{x \in A \| x \subseteq U\})$

Proof

Step	Hyp	Ref	Expression
1		lssats.s	$⊢ S = LSubSp (W)$
2		lssats.n	$⊢ N = LSpan (W)$
3		lssats.a	$⊢ A = LSAtoms (W)$
4		eleq1	$⊢ y = 0_{W} \to (y \in N (⋃ \{x \in A \| x \subseteq U\}) \leftrightarrow 0_{W} \in N (⋃ \{x \in A \| x \subseteq U\}))$
5		simplll	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to W \in LMod$
6		simpllr	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to U \in S$
7		simplr	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to y \in U$
8		eqid	$⊢ {Base}_{W} = {Base}_{W}$
9	8 1	lssel	$⊢ (U \in S \land y \in U) \to y \in {Base}_{W}$
10	6 7 9	syl2anc	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to y \in {Base}_{W}$
11	8 1 2	lspsncl	$⊢ (W \in LMod \land y \in {Base}_{W}) \to N (\{y\}) \in S$
12	5 10 11	syl2anc	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (\{y\}) \in S$
13	1 2	lspid	$⊢ (W \in LMod \land N (\{y\}) \in S) \to N (N (\{y\})) = N (\{y\})$
14	5 12 13	syl2anc	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (N (\{y\})) = N (\{y\})$
15	1 3	lsatlss	$⊢ W \in LMod \to A \subseteq S$
16	15	adantr	$⊢ (W \in LMod \land U \in S) \to A \subseteq S$
17		rabss2	$⊢ A \subseteq S \to \{x \in A \| x \subseteq U\} \subseteq \{x \in S \| x \subseteq U\}$
18		uniss	$⊢ \{x \in A \| x \subseteq U\} \subseteq \{x \in S \| x \subseteq U\} \to ⋃ \{x \in A \| x \subseteq U\} \subseteq ⋃ \{x \in S \| x \subseteq U\}$
19	16 17 18	3syl	$⊢ (W \in LMod \land U \in S) \to ⋃ \{x \in A \| x \subseteq U\} \subseteq ⋃ \{x \in S \| x \subseteq U\}$
20		unimax	$⊢ U \in S \to ⋃ \{x \in S \| x \subseteq U\} = U$
21	8 1	lssss	$⊢ U \in S \to U \subseteq {Base}_{W}$
22	20 21	eqsstrd	$⊢ U \in S \to ⋃ \{x \in S \| x \subseteq U\} \subseteq {Base}_{W}$
23	22	adantl	$⊢ (W \in LMod \land U \in S) \to ⋃ \{x \in S \| x \subseteq U\} \subseteq {Base}_{W}$
24	19 23	sstrd	$⊢ (W \in LMod \land U \in S) \to ⋃ \{x \in A \| x \subseteq U\} \subseteq {Base}_{W}$
25	24	ad2antrr	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to ⋃ \{x \in A \| x \subseteq U\} \subseteq {Base}_{W}$
26		simpr	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to y \neq 0_{W}$
27		eqid	$⊢ 0_{W} = 0_{W}$
28	8 2 27 3	lsatlspsn2	$⊢ (W \in LMod \land y \in {Base}_{W} \land y \neq 0_{W}) \to N (\{y\}) \in A$
29	5 10 26 28	syl3anc	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (\{y\}) \in A$
30	1 2 5 6 7	ellspsn5	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (\{y\}) \subseteq U$
31		sseq1	$⊢ x = N (\{y\}) \to (x \subseteq U \leftrightarrow N (\{y\}) \subseteq U)$
32	31	elrab	$⊢ N (\{y\}) \in \{x \in A \| x \subseteq U\} \leftrightarrow (N (\{y\}) \in A \land N (\{y\}) \subseteq U)$
33	29 30 32	sylanbrc	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (\{y\}) \in \{x \in A \| x \subseteq U\}$
34		elssuni	$⊢ N (\{y\}) \in \{x \in A \| x \subseteq U\} \to N (\{y\}) \subseteq ⋃ \{x \in A \| x \subseteq U\}$
35	33 34	syl	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (\{y\}) \subseteq ⋃ \{x \in A \| x \subseteq U\}$
36	8 2	lspss	$⊢ (W \in LMod \land ⋃ \{x \in A \| x \subseteq U\} \subseteq {Base}_{W} \land N (\{y\}) \subseteq ⋃ \{x \in A \| x \subseteq U\}) \to N (N (\{y\})) \subseteq N (⋃ \{x \in A \| x \subseteq U\})$
37	5 25 35 36	syl3anc	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (N (\{y\})) \subseteq N (⋃ \{x \in A \| x \subseteq U\})$
38	14 37	eqsstrrd	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to N (\{y\}) \subseteq N (⋃ \{x \in A \| x \subseteq U\})$
39	8 2	lspsnid	$⊢ (W \in LMod \land y \in {Base}_{W}) \to y \in N (\{y\})$
40	5 10 39	syl2anc	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to y \in N (\{y\})$
41	38 40	sseldd	$⊢ (((W \in LMod \land U \in S) \land y \in U) \land y \neq 0_{W}) \to y \in N (⋃ \{x \in A \| x \subseteq U\})$
42		simpll	$⊢ ((W \in LMod \land U \in S) \land y \in U) \to W \in LMod$
43	8 1 2	lspcl	$⊢ (W \in LMod \land ⋃ \{x \in A \| x \subseteq U\} \subseteq {Base}_{W}) \to N (⋃ \{x \in A \| x \subseteq U\}) \in S$
44	24 43	syldan	$⊢ (W \in LMod \land U \in S) \to N (⋃ \{x \in A \| x \subseteq U\}) \in S$
45	44	adantr	$⊢ ((W \in LMod \land U \in S) \land y \in U) \to N (⋃ \{x \in A \| x \subseteq U\}) \in S$
46	27 1	lss0cl	$⊢ (W \in LMod \land N (⋃ \{x \in A \| x \subseteq U\}) \in S) \to 0_{W} \in N (⋃ \{x \in A \| x \subseteq U\})$
47	42 45 46	syl2anc	$⊢ ((W \in LMod \land U \in S) \land y \in U) \to 0_{W} \in N (⋃ \{x \in A \| x \subseteq U\})$
48	4 41 47	pm2.61ne	$⊢ ((W \in LMod \land U \in S) \land y \in U) \to y \in N (⋃ \{x \in A \| x \subseteq U\})$
49	48	ex	$⊢ (W \in LMod \land U \in S) \to (y \in U \to y \in N (⋃ \{x \in A \| x \subseteq U\}))$
50	49	ssrdv	$⊢ (W \in LMod \land U \in S) \to U \subseteq N (⋃ \{x \in A \| x \subseteq U\})$
51		simpl	$⊢ (W \in LMod \land U \in S) \to W \in LMod$
52	8 2	lspss	$⊢ (W \in LMod \land ⋃ \{x \in S \| x \subseteq U\} \subseteq {Base}_{W} \land ⋃ \{x \in A \| x \subseteq U\} \subseteq ⋃ \{x \in S \| x \subseteq U\}) \to N (⋃ \{x \in A \| x \subseteq U\}) \subseteq N (⋃ \{x \in S \| x \subseteq U\})$
53	51 23 19 52	syl3anc	$⊢ (W \in LMod \land U \in S) \to N (⋃ \{x \in A \| x \subseteq U\}) \subseteq N (⋃ \{x \in S \| x \subseteq U\})$
54	20	adantl	$⊢ (W \in LMod \land U \in S) \to ⋃ \{x \in S \| x \subseteq U\} = U$
55	54	fveq2d	$⊢ (W \in LMod \land U \in S) \to N (⋃ \{x \in S \| x \subseteq U\}) = N (U)$
56	1 2	lspid	$⊢ (W \in LMod \land U \in S) \to N (U) = U$
57	55 56	eqtrd	$⊢ (W \in LMod \land U \in S) \to N (⋃ \{x \in S \| x \subseteq U\}) = U$
58	53 57	sseqtrd	$⊢ (W \in LMod \land U \in S) \to N (⋃ \{x \in A \| x \subseteq U\}) \subseteq U$
59	50 58	eqssd	$⊢ (W \in LMod \land U \in S) \to U = N (⋃ \{x \in A \| x \subseteq U\})$

Metamath Proof Explorer

Theorem lssats

Proof