pmapocjN

Description: The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapocj.b	$⊢ B = {Base}_{K}$
	pmapocj.j	$⊢ \underset{˙}{\lor} = join (K)$
	pmapocj.m	$⊢ \underset{˙}{\land} = meet (K)$
	pmapocj.o	$⊢ \underset{˙}{⊥} = oc (K)$
	pmapocj.f	$⊢ F = pmap (K)$
	pmapocj.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	pmapocj.r	$⊢ N = ⊥_{𝑃} (K)$
Assertion	pmapocjN	$⊢ (K \in HL \land X \in B \land Y \in B) \to F (\underset{˙}{⊥} (X \underset{˙}{\lor} Y)) = N (F (X) \underset{˙}{+} F (Y))$

Proof

Step	Hyp	Ref	Expression
1		pmapocj.b	$⊢ B = {Base}_{K}$
2		pmapocj.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pmapocj.m	$⊢ \underset{˙}{\land} = meet (K)$
4		pmapocj.o	$⊢ \underset{˙}{⊥} = oc (K)$
5		pmapocj.f	$⊢ F = pmap (K)$
6		pmapocj.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
7		pmapocj.r	$⊢ N = ⊥_{𝑃} (K)$
8	1 2 5 6 7	pmapj2N	$⊢ (K \in HL \land X \in B \land Y \in B) \to F (X \underset{˙}{\lor} Y) = N (N (F (X) \underset{˙}{+} F (Y)))$
9	8	fveq2d	$⊢ (K \in HL \land X \in B \land Y \in B) \to N (F (X \underset{˙}{\lor} Y)) = N (N (N (F (X) \underset{˙}{+} F (Y))))$
10		simp1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in HL$
11		hllat	$⊢ K \in HL \to K \in Lat$
12	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
13	11 12	syl3an1	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
14	1 4 5 7	polpmapN	$⊢ (K \in HL \land X \underset{˙}{\lor} Y \in B) \to N (F (X \underset{˙}{\lor} Y)) = F (\underset{˙}{⊥} (X \underset{˙}{\lor} Y))$
15	10 13 14	syl2anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to N (F (X \underset{˙}{\lor} Y)) = F (\underset{˙}{⊥} (X \underset{˙}{\lor} Y))$
16		eqid	$⊢ Atoms (K) = Atoms (K)$
17	1 16 5	pmapssat	$⊢ (K \in HL \land X \in B) \to F (X) \subseteq Atoms (K)$
18	17	3adant3	$⊢ (K \in HL \land X \in B \land Y \in B) \to F (X) \subseteq Atoms (K)$
19	1 16 5	pmapssat	$⊢ (K \in HL \land Y \in B) \to F (Y) \subseteq Atoms (K)$
20	19	3adant2	$⊢ (K \in HL \land X \in B \land Y \in B) \to F (Y) \subseteq Atoms (K)$
21	16 6	paddssat	$⊢ (K \in HL \land F (X) \subseteq Atoms (K) \land F (Y) \subseteq Atoms (K)) \to F (X) \underset{˙}{+} F (Y) \subseteq Atoms (K)$
22	10 18 20 21	syl3anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to F (X) \underset{˙}{+} F (Y) \subseteq Atoms (K)$
23	16 7	3polN	$⊢ (K \in HL \land F (X) \underset{˙}{+} F (Y) \subseteq Atoms (K)) \to N (N (N (F (X) \underset{˙}{+} F (Y)))) = N (F (X) \underset{˙}{+} F (Y))$
24	10 22 23	syl2anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to N (N (N (F (X) \underset{˙}{+} F (Y)))) = N (F (X) \underset{˙}{+} F (Y))$
25	9 15 24	3eqtr3d	$⊢ (K \in HL \land X \in B \land Y \in B) \to F (\underset{˙}{⊥} (X \underset{˙}{\lor} Y)) = N (F (X) \underset{˙}{+} F (Y))$

Metamath Proof Explorer

Theorem pmapocjN

Proof