pnonsingN

Description: The intersection of a set of atoms and its polarity is empty. Definition of nonsingular in Holland95 p. 214. (Contributed by NM, 29-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2polat.a	$⊢ A = Atoms (K)$
	2polat.p	$⊢ P = ⊥_{𝑃} (K)$
Assertion	pnonsingN	$⊢ (K \in HL \land X \subseteq A) \to X \cap P (X) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		2polat.a	$⊢ A = Atoms (K)$
2		2polat.p	$⊢ P = ⊥_{𝑃} (K)$
3	1 2	2polssN	$⊢ (K \in HL \land X \subseteq A) \to X \subseteq P (P (X))$
4	3	ssrind	$⊢ (K \in HL \land X \subseteq A) \to X \cap P (X) \subseteq P (P (X)) \cap P (X)$
5		eqid	$⊢ lub (K) = lub (K)$
6		eqid	$⊢ pmap (K) = pmap (K)$
7	5 1 6 2	2polvalN	$⊢ (K \in HL \land X \subseteq A) \to P (P (X)) = pmap (K) (lub (K) (X))$
8		eqid	$⊢ oc (K) = oc (K)$
9	5 8 1 6 2	polval2N	$⊢ (K \in HL \land X \subseteq A) \to P (X) = pmap (K) (oc (K) (lub (K) (X)))$
10	7 9	ineq12d	$⊢ (K \in HL \land X \subseteq A) \to P (P (X)) \cap P (X) = pmap (K) (lub (K) (X)) \cap pmap (K) (oc (K) (lub (K) (X)))$
11		hlop	$⊢ K \in HL \to K \in OP$
12	11	adantr	$⊢ (K \in HL \land X \subseteq A) \to K \in OP$
13		hlclat	$⊢ K \in HL \to K \in CLat$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 1	atssbase	$⊢ A \subseteq {Base}_{K}$
16		sstr	$⊢ (X \subseteq A \land A \subseteq {Base}_{K}) \to X \subseteq {Base}_{K}$
17	15 16	mpan2	$⊢ X \subseteq A \to X \subseteq {Base}_{K}$
18	14 5	clatlubcl	$⊢ (K \in CLat \land X \subseteq {Base}_{K}) \to lub (K) (X) \in {Base}_{K}$
19	13 17 18	syl2an	$⊢ (K \in HL \land X \subseteq A) \to lub (K) (X) \in {Base}_{K}$
20		eqid	$⊢ meet (K) = meet (K)$
21		eqid	$⊢ 0. (K) = 0. (K)$
22	14 8 20 21	opnoncon	$⊢ (K \in OP \land lub (K) (X) \in {Base}_{K}) \to lub (K) (X) meet (K) oc (K) (lub (K) (X)) = 0. (K)$
23	12 19 22	syl2anc	$⊢ (K \in HL \land X \subseteq A) \to lub (K) (X) meet (K) oc (K) (lub (K) (X)) = 0. (K)$
24	23	fveq2d	$⊢ (K \in HL \land X \subseteq A) \to pmap (K) (lub (K) (X) meet (K) oc (K) (lub (K) (X))) = pmap (K) (0. (K))$
25		simpl	$⊢ (K \in HL \land X \subseteq A) \to K \in HL$
26	14 8	opoccl	$⊢ (K \in OP \land lub (K) (X) \in {Base}_{K}) \to oc (K) (lub (K) (X)) \in {Base}_{K}$
27	12 19 26	syl2anc	$⊢ (K \in HL \land X \subseteq A) \to oc (K) (lub (K) (X)) \in {Base}_{K}$
28	14 20 1 6	pmapmeet	$⊢ (K \in HL \land lub (K) (X) \in {Base}_{K} \land oc (K) (lub (K) (X)) \in {Base}_{K}) \to pmap (K) (lub (K) (X) meet (K) oc (K) (lub (K) (X))) = pmap (K) (lub (K) (X)) \cap pmap (K) (oc (K) (lub (K) (X)))$
29	25 19 27 28	syl3anc	$⊢ (K \in HL \land X \subseteq A) \to pmap (K) (lub (K) (X) meet (K) oc (K) (lub (K) (X))) = pmap (K) (lub (K) (X)) \cap pmap (K) (oc (K) (lub (K) (X)))$
30		hlatl	$⊢ K \in HL \to K \in AtLat$
31	30	adantr	$⊢ (K \in HL \land X \subseteq A) \to K \in AtLat$
32	21 6	pmap0	$⊢ K \in AtLat \to pmap (K) (0. (K)) = \emptyset$
33	31 32	syl	$⊢ (K \in HL \land X \subseteq A) \to pmap (K) (0. (K)) = \emptyset$
34	24 29 33	3eqtr3d	$⊢ (K \in HL \land X \subseteq A) \to pmap (K) (lub (K) (X)) \cap pmap (K) (oc (K) (lub (K) (X))) = \emptyset$
35	10 34	eqtrd	$⊢ (K \in HL \land X \subseteq A) \to P (P (X)) \cap P (X) = \emptyset$
36	4 35	sseqtrd	$⊢ (K \in HL \land X \subseteq A) \to X \cap P (X) \subseteq \emptyset$
37		ss0b	$⊢ X \cap P (X) \subseteq \emptyset \leftrightarrow X \cap P (X) = \emptyset$
38	36 37	sylib	$⊢ (K \in HL \land X \subseteq A) \to X \cap P (X) = \emptyset$

Metamath Proof Explorer

Theorem pnonsingN

Proof