paddunN

Description: The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d .) (Contributed by NM, 6-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	paddun.a	$⊢ A = Atoms (K)$
	paddun.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	paddun.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
Assertion	paddunN	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S \underset{˙}{+} T) = \underset{˙}{⊥} (S \cup T)$

Proof

Step	Hyp	Ref	Expression
1		paddun.a	$⊢ A = Atoms (K)$
2		paddun.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		paddun.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
4		simp1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to K \in HL$
5	1 2	paddssat	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \underset{˙}{+} T \subseteq A$
6	1 2	paddunssN	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \cup T \subseteq S \underset{˙}{+} T$
7	1 3	polcon3N	$⊢ (K \in HL \land S \underset{˙}{+} T \subseteq A \land S \cup T \subseteq S \underset{˙}{+} T) \to \underset{˙}{⊥} (S \underset{˙}{+} T) \subseteq \underset{˙}{⊥} (S \cup T)$
8	4 5 6 7	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S \underset{˙}{+} T) \subseteq \underset{˙}{⊥} (S \cup T)$
9		hlclat	$⊢ K \in HL \to K \in CLat$
10	9	3ad2ant1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to K \in CLat$
11		unss	$⊢ (S \subseteq A \land T \subseteq A) \leftrightarrow S \cup T \subseteq A$
12	11	biimpi	$⊢ (S \subseteq A \land T \subseteq A) \to S \cup T \subseteq A$
13	12	3adant1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \cup T \subseteq A$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 1	atssbase	$⊢ A \subseteq {Base}_{K}$
16	13 15	sstrdi	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \cup T \subseteq {Base}_{K}$
17		eqid	$⊢ lub (K) = lub (K)$
18	14 17	clatlubcl	$⊢ (K \in CLat \land S \cup T \subseteq {Base}_{K}) \to lub (K) (S \cup T) \in {Base}_{K}$
19	10 16 18	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (S \cup T) \in {Base}_{K}$
20		eqid	$⊢ pmap (K) = pmap (K)$
21	14 20	pmapssbaN	$⊢ (K \in HL \land lub (K) (S \cup T) \in {Base}_{K}) \to pmap (K) (lub (K) (S \cup T)) \subseteq {Base}_{K}$
22	4 19 21	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (lub (K) (S \cup T)) \subseteq {Base}_{K}$
23	1 3	polssatN	$⊢ (K \in HL \land S \subseteq A) \to \underset{˙}{⊥} (S) \subseteq A$
24	23	3adant3	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S) \subseteq A$
25	1 3	polssatN	$⊢ (K \in HL \land \underset{˙}{⊥} (S) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq A$
26	4 24 25	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq A$
27	1 3	polssatN	$⊢ (K \in HL \land T \subseteq A) \to \underset{˙}{⊥} (T) \subseteq A$
28	27	3adant2	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (T) \subseteq A$
29	1 3	polssatN	$⊢ (K \in HL \land \underset{˙}{⊥} (T) \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (T)) \subseteq A$
30	4 28 29	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (T)) \subseteq A$
31	4 26 30	3jca	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to (K \in HL \land \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (T)) \subseteq A)$
32	1 3	2polssN	$⊢ (K \in HL \land S \subseteq A) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
33	32	3adant3	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
34	1 3	2polssN	$⊢ (K \in HL \land T \subseteq A) \to T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
35	34	3adant2	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
36	33 35	jca	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to (S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \land T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (T)))$
37	1 2	paddss12	$⊢ (K \in HL \land \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (T)) \subseteq A) \to ((S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \land T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (T))) \to S \underset{˙}{+} T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \underset{˙}{+} \underset{˙}{⊥} (\underset{˙}{⊥} (T)))$
38	31 36 37	sylc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \underset{˙}{+} T \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \underset{˙}{+} \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
39	17 1 20 3	2polvalN	$⊢ (K \in HL \land S \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) = pmap (K) (lub (K) (S))$
40	39	3adant3	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) = pmap (K) (lub (K) (S))$
41	17 1 20 3	2polvalN	$⊢ (K \in HL \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (T)) = pmap (K) (lub (K) (T))$
42	41	3adant2	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (T)) = pmap (K) (lub (K) (T))$
43	40 42	oveq12d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \underset{˙}{+} \underset{˙}{⊥} (\underset{˙}{⊥} (T)) = pmap (K) (lub (K) (S)) \underset{˙}{+} pmap (K) (lub (K) (T))$
44	38 43	sseqtrd	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \underset{˙}{+} T \subseteq pmap (K) (lub (K) (S)) \underset{˙}{+} pmap (K) (lub (K) (T))$
45		hllat	$⊢ K \in HL \to K \in Lat$
46	45	3ad2ant1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to K \in Lat$
47		simp2	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \subseteq A$
48	47 15	sstrdi	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \subseteq {Base}_{K}$
49	14 17	clatlubcl	$⊢ (K \in CLat \land S \subseteq {Base}_{K}) \to lub (K) (S) \in {Base}_{K}$
50	10 48 49	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (S) \in {Base}_{K}$
51		simp3	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to T \subseteq A$
52	51 15	sstrdi	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to T \subseteq {Base}_{K}$
53	14 17	clatlubcl	$⊢ (K \in CLat \land T \subseteq {Base}_{K}) \to lub (K) (T) \in {Base}_{K}$
54	10 52 53	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (T) \in {Base}_{K}$
55		eqid	$⊢ join (K) = join (K)$
56	14 55 20 2	pmapjoin	$⊢ (K \in Lat \land lub (K) (S) \in {Base}_{K} \land lub (K) (T) \in {Base}_{K}) \to pmap (K) (lub (K) (S)) \underset{˙}{+} pmap (K) (lub (K) (T)) \subseteq pmap (K) (lub (K) (S) join (K) lub (K) (T))$
57	46 50 54 56	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (lub (K) (S)) \underset{˙}{+} pmap (K) (lub (K) (T)) \subseteq pmap (K) (lub (K) (S) join (K) lub (K) (T))$
58	44 57	sstrd	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \underset{˙}{+} T \subseteq pmap (K) (lub (K) (S) join (K) lub (K) (T))$
59	14 55 17	lubun	$⊢ (K \in CLat \land S \subseteq {Base}_{K} \land T \subseteq {Base}_{K}) \to lub (K) (S \cup T) = lub (K) (S) join (K) lub (K) (T)$
60	10 48 52 59	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (S \cup T) = lub (K) (S) join (K) lub (K) (T)$
61	60	fveq2d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (lub (K) (S \cup T)) = pmap (K) (lub (K) (S) join (K) lub (K) (T))$
62	58 61	sseqtrrd	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \underset{˙}{+} T \subseteq pmap (K) (lub (K) (S \cup T))$
63		eqid	$⊢ \leq_{K} = \leq_{K}$
64	14 63 17	lubss	$⊢ (K \in CLat \land pmap (K) (lub (K) (S \cup T)) \subseteq {Base}_{K} \land S \underset{˙}{+} T \subseteq pmap (K) (lub (K) (S \cup T))) \to lub (K) (S \underset{˙}{+} T) \leq_{K} lub (K) (pmap (K) (lub (K) (S \cup T)))$
65	10 22 62 64	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (S \underset{˙}{+} T) \leq_{K} lub (K) (pmap (K) (lub (K) (S \cup T)))$
66	5 15	sstrdi	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \underset{˙}{+} T \subseteq {Base}_{K}$
67	14 17	clatlubcl	$⊢ (K \in CLat \land S \underset{˙}{+} T \subseteq {Base}_{K}) \to lub (K) (S \underset{˙}{+} T) \in {Base}_{K}$
68	10 66 67	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (S \underset{˙}{+} T) \in {Base}_{K}$
69	14 17	clatlubcl	$⊢ (K \in CLat \land pmap (K) (lub (K) (S \cup T)) \subseteq {Base}_{K}) \to lub (K) (pmap (K) (lub (K) (S \cup T))) \in {Base}_{K}$
70	10 22 69	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (pmap (K) (lub (K) (S \cup T))) \in {Base}_{K}$
71	14 63 20	pmaple	$⊢ (K \in HL \land lub (K) (S \underset{˙}{+} T) \in {Base}_{K} \land lub (K) (pmap (K) (lub (K) (S \cup T))) \in {Base}_{K}) \to (lub (K) (S \underset{˙}{+} T) \leq_{K} lub (K) (pmap (K) (lub (K) (S \cup T))) \leftrightarrow pmap (K) (lub (K) (S \underset{˙}{+} T)) \subseteq pmap (K) (lub (K) (pmap (K) (lub (K) (S \cup T)))))$
72	4 68 70 71	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to (lub (K) (S \underset{˙}{+} T) \leq_{K} lub (K) (pmap (K) (lub (K) (S \cup T))) \leftrightarrow pmap (K) (lub (K) (S \underset{˙}{+} T)) \subseteq pmap (K) (lub (K) (pmap (K) (lub (K) (S \cup T)))))$
73	65 72	mpbid	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (lub (K) (S \underset{˙}{+} T)) \subseteq pmap (K) (lub (K) (pmap (K) (lub (K) (S \cup T))))$
74	17 1 20 3	2polvalN	$⊢ (K \in HL \land S \underset{˙}{+} T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S \underset{˙}{+} T)) = pmap (K) (lub (K) (S \underset{˙}{+} T))$
75	4 5 74	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S \underset{˙}{+} T)) = pmap (K) (lub (K) (S \underset{˙}{+} T))$
76	17 1 20 3	2polvalN	$⊢ (K \in HL \land S \cup T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S \cup T)) = pmap (K) (lub (K) (S \cup T))$
77	4 13 76	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S \cup T)) = pmap (K) (lub (K) (S \cup T))$
78	17 1 20	2pmaplubN	$⊢ (K \in HL \land S \cup T \subseteq A) \to pmap (K) (lub (K) (pmap (K) (lub (K) (S \cup T)))) = pmap (K) (lub (K) (S \cup T))$
79	4 13 78	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (lub (K) (pmap (K) (lub (K) (S \cup T)))) = pmap (K) (lub (K) (S \cup T))$
80	77 79	eqtr4d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S \cup T)) = pmap (K) (lub (K) (pmap (K) (lub (K) (S \cup T))))$
81	73 75 80	3sstr4d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (\underset{˙}{⊥} (S \underset{˙}{+} T)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S \cup T))$
82	1 3	2polcon4bN	$⊢ (K \in HL \land S \underset{˙}{+} T \subseteq A \land S \cup T \subseteq A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (S \underset{˙}{+} T)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S \cup T)) \leftrightarrow \underset{˙}{⊥} (S \cup T) \subseteq \underset{˙}{⊥} (S \underset{˙}{+} T))$
83	4 5 13 82	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to (\underset{˙}{⊥} (\underset{˙}{⊥} (S \underset{˙}{+} T)) \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S \cup T)) \leftrightarrow \underset{˙}{⊥} (S \cup T) \subseteq \underset{˙}{⊥} (S \underset{˙}{+} T))$
84	81 83	mpbid	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S \cup T) \subseteq \underset{˙}{⊥} (S \underset{˙}{+} T)$
85	8 84	eqssd	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S \underset{˙}{+} T) = \underset{˙}{⊥} (S \cup T)$

Metamath Proof Explorer

Theorem paddunN

Proof