Theorem pclunN

Description: The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclun.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pclun.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
	pclun.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
Assertion	pclunN	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(X\cup Y\right)=U\left(X\underset{\dot{}}{+}Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		pclun.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		pclun.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
3		pclun.c	$$⊢U=\mathrm{PCl}\left(K\right)$$
4		simp1	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to K\in V$$
5	1 2	paddunssN	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\cup Y\subseteq X\underset{\dot{}}{+}Y$$
6	1 2	paddssat	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\underset{\dot{}}{+}Y\subseteq A$$
7	1 3	pclssN	$$⊢\left(K\in V\wedge X\cup Y\subseteq X\underset{\dot{}}{+}Y\wedge X\underset{\dot{}}{+}Y\subseteq A\right)\to U\left(X\cup Y\right)\subseteq U\left(X\underset{\dot{}}{+}Y\right)$$
8	4 5 6 7	syl3anc	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(X\cup Y\right)\subseteq U\left(X\underset{\dot{}}{+}Y\right)$$
9		unss	$$⊢\left(X\subseteq A\wedge Y\subseteq A\right)\leftrightarrow X\cup Y\subseteq A$$
10	9	biimpi	$$⊢\left(X\subseteq A\wedge Y\subseteq A\right)\to X\cup Y\subseteq A$$
11	10	3adant1	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\cup Y\subseteq A$$
12	1 3	pclssidN	$$⊢\left(K\in V\wedge X\cup Y\subseteq A\right)\to X\cup Y\subseteq U\left(X\cup Y\right)$$
13	4 11 12	syl2anc	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\cup Y\subseteq U\left(X\cup Y\right)$$
14		unss	$$⊢\left(X\subseteq U\left(X\cup Y\right)\wedge Y\subseteq U\left(X\cup Y\right)\right)\leftrightarrow X\cup Y\subseteq U\left(X\cup Y\right)$$
15	13 14	sylibr	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to \left(X\subseteq U\left(X\cup Y\right)\wedge Y\subseteq U\left(X\cup Y\right)\right)$$
16		simp2	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\subseteq A$$
17		simp3	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to Y\subseteq A$$
18		eqid	$$⊢\mathrm{PSubSp}\left(K\right)=\mathrm{PSubSp}\left(K\right)$$
19	1 18 3	pclclN	$$⊢\left(K\in V\wedge X\cup Y\subseteq A\right)\to U\left(X\cup Y\right)\in \mathrm{PSubSp}\left(K\right)$$
20	4 11 19	syl2anc	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(X\cup Y\right)\in \mathrm{PSubSp}\left(K\right)$$
21	1 18 2	paddss	$$⊢\left(K\in V\wedge \left(X\subseteq A\wedge Y\subseteq A\wedge U\left(X\cup Y\right)\in \mathrm{PSubSp}\left(K\right)\right)\right)\to \left(\left(X\subseteq U\left(X\cup Y\right)\wedge Y\subseteq U\left(X\cup Y\right)\right)\leftrightarrow X\underset{\dot{}}{+}Y\subseteq U\left(X\cup Y\right)\right)$$
22	4 16 17 20 21	syl13anc	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to \left(\left(X\subseteq U\left(X\cup Y\right)\wedge Y\subseteq U\left(X\cup Y\right)\right)\leftrightarrow X\underset{\dot{}}{+}Y\subseteq U\left(X\cup Y\right)\right)$$
23	15 22	mpbid	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\underset{\dot{}}{+}Y\subseteq U\left(X\cup Y\right)$$
24	1 18	psubssat	$$⊢\left(K\in V\wedge U\left(X\cup Y\right)\in \mathrm{PSubSp}\left(K\right)\right)\to U\left(X\cup Y\right)\subseteq A$$
25	4 20 24	syl2anc	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(X\cup Y\right)\subseteq A$$
26	1 3	pclssN	$$⊢\left(K\in V\wedge X\underset{\dot{}}{+}Y\subseteq U\left(X\cup Y\right)\wedge U\left(X\cup Y\right)\subseteq A\right)\to U\left(X\underset{\dot{}}{+}Y\right)\subseteq U\left(U\left(X\cup Y\right)\right)$$
27	4 23 25 26	syl3anc	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(X\underset{\dot{}}{+}Y\right)\subseteq U\left(U\left(X\cup Y\right)\right)$$
28	18 3	pclidN	$$⊢\left(K\in V\wedge U\left(X\cup Y\right)\in \mathrm{PSubSp}\left(K\right)\right)\to U\left(U\left(X\cup Y\right)\right)=U\left(X\cup Y\right)$$
29	4 20 28	syl2anc	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(U\left(X\cup Y\right)\right)=U\left(X\cup Y\right)$$
30	27 29	sseqtrd	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(X\underset{\dot{}}{+}Y\right)\subseteq U\left(X\cup Y\right)$$
31	8 30	eqssd	$$⊢\left(K\in V\wedge X\subseteq A\wedge Y\subseteq A\right)\to U\left(X\cup Y\right)=U\left(X\underset{\dot{}}{+}Y\right)$$