poldmj1N

Description: De Morgan's law for polarity of projective sum. ( oldmj1 analog.) (Contributed by NM, 7-Mar-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		paddun.a	$⊢ A = Atoms (K)$
2		paddun.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		paddun.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
4	1 2 3	paddunN	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S \underset{˙}{+} T) = \underset{˙}{⊥} (S \cup T)$
5		simp1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to K \in HL$
6		unss	$⊢ (S \subseteq A \land T \subseteq A) \leftrightarrow S \cup T \subseteq A$
7	6	biimpi	$⊢ (S \subseteq A \land T \subseteq A) \to S \cup T \subseteq A$
8	7	3adant1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \cup T \subseteq A$
9		eqid	$⊢ lub (K) = lub (K)$
10		eqid	$⊢ oc (K) = oc (K)$
11		eqid	$⊢ pmap (K) = pmap (K)$
12	9 10 1 11 3	polval2N	$⊢ (K \in HL \land S \cup T \subseteq A) \to \underset{˙}{⊥} (S \cup T) = pmap (K) (oc (K) (lub (K) (S \cup T)))$
13	5 8 12	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S \cup T) = pmap (K) (oc (K) (lub (K) (S \cup T)))$
14		hlop	$⊢ K \in HL \to K \in OP$
15	14	3ad2ant1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to K \in OP$
16		hlclat	$⊢ K \in HL \to K \in CLat$
17	16	3ad2ant1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to K \in CLat$
18		simp2	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \subseteq A$
19		eqid	$⊢ {Base}_{K} = {Base}_{K}$
20	19 1	atssbase	$⊢ A \subseteq {Base}_{K}$
21	18 20	sstrdi	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to S \subseteq {Base}_{K}$
22	19 9	clatlubcl	$⊢ (K \in CLat \land S \subseteq {Base}_{K}) \to lub (K) (S) \in {Base}_{K}$
23	17 21 22	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (S) \in {Base}_{K}$
24	19 10	opoccl	$⊢ (K \in OP \land lub (K) (S) \in {Base}_{K}) \to oc (K) (lub (K) (S)) \in {Base}_{K}$
25	15 23 24	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to oc (K) (lub (K) (S)) \in {Base}_{K}$
26		simp3	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to T \subseteq A$
27	26 20	sstrdi	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to T \subseteq {Base}_{K}$
28	19 9	clatlubcl	$⊢ (K \in CLat \land T \subseteq {Base}_{K}) \to lub (K) (T) \in {Base}_{K}$
29	17 27 28	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to lub (K) (T) \in {Base}_{K}$
30	19 10	opoccl	$⊢ (K \in OP \land lub (K) (T) \in {Base}_{K}) \to oc (K) (lub (K) (T)) \in {Base}_{K}$
31	15 29 30	syl2anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to oc (K) (lub (K) (T)) \in {Base}_{K}$
32		eqid	$⊢ meet (K) = meet (K)$
33	19 32 1 11	pmapmeet	$⊢ (K \in HL \land oc (K) (lub (K) (S)) \in {Base}_{K} \land oc (K) (lub (K) (T)) \in {Base}_{K}) \to pmap (K) (oc (K) (lub (K) (S)) meet (K) oc (K) (lub (K) (T))) = pmap (K) (oc (K) (lub (K) (S))) \cap pmap (K) (oc (K) (lub (K) (T)))$
34	5 25 31 33	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (oc (K) (lub (K) (S)) meet (K) oc (K) (lub (K) (T))) = pmap (K) (oc (K) (lub (K) (S))) \cap pmap (K) (oc (K) (lub (K) (T)))$
35		eqid	$⊢ join (K) = join (K)$
36	19 35 9	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)$
37	17 21 27 36	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)$
38	37	fveq2d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to oc (K) (lub (K) (S \cup T)) = oc (K) (lub (K) (S) join (K) lub (K) (T))$
39		hlol	$⊢ K \in HL \to K \in OL$
40	39	3ad2ant1	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to K \in OL$
41	19 35 32 10	oldmj1	$⊢ (K \in OL \land lub (K) (S) \in {Base}_{K} \land lub (K) (T) \in {Base}_{K}) \to oc (K) (lub (K) (S) join (K) lub (K) (T)) = oc (K) (lub (K) (S)) meet (K) oc (K) (lub (K) (T))$
42	40 23 29 41	syl3anc	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to oc (K) (lub (K) (S) join (K) lub (K) (T)) = oc (K) (lub (K) (S)) meet (K) oc (K) (lub (K) (T))$
43	38 42	eqtrd	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to oc (K) (lub (K) (S \cup T)) = oc (K) (lub (K) (S)) meet (K) oc (K) (lub (K) (T))$
44	43	fveq2d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (oc (K) (lub (K) (S \cup T))) = pmap (K) (oc (K) (lub (K) (S)) meet (K) oc (K) (lub (K) (T)))$
45	9 10 1 11 3	polval2N	$⊢ (K \in HL \land S \subseteq A) \to \underset{˙}{⊥} (S) = pmap (K) (oc (K) (lub (K) (S)))$
46	45	3adant3	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S) = pmap (K) (oc (K) (lub (K) (S)))$
47	9 10 1 11 3	polval2N	$⊢ (K \in HL \land T \subseteq A) \to \underset{˙}{⊥} (T) = pmap (K) (oc (K) (lub (K) (T)))$
48	47	3adant2	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (T) = pmap (K) (oc (K) (lub (K) (T)))$
49	46 48	ineq12d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S) \cap \underset{˙}{⊥} (T) = pmap (K) (oc (K) (lub (K) (S))) \cap pmap (K) (oc (K) (lub (K) (T)))$
50	34 44 49	3eqtr4d	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to pmap (K) (oc (K) (lub (K) (S \cup T))) = \underset{˙}{⊥} (S) \cap \underset{˙}{⊥} (T)$
51	4 13 50	3eqtrd	$⊢ (K \in HL \land S \subseteq A \land T \subseteq A) \to \underset{˙}{⊥} (S \underset{˙}{+} T) = \underset{˙}{⊥} (S) \cap \underset{˙}{⊥} (T)$

Metamath Proof Explorer

Theorem poldmj1N

Proof