pmapj2N

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

	Ref	Expression
Hypotheses	pmapj2.b	$⊢ B = {Base}_{K}$
	pmapj2.j	$⊢ \underset{˙}{\lor} = join (K)$
	pmapj2.m	$⊢ M = pmap (K)$
	pmapj2.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	pmapj2.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
Assertion	pmapj2N	$⊢ (K \in HL \land X \in B \land Y \in B) \to M (X \underset{˙}{\lor} Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (M (X) \underset{˙}{+} M (Y)))$

Proof

Step	Hyp	Ref	Expression
1		pmapj2.b	$⊢ B = {Base}_{K}$
2		pmapj2.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pmapj2.m	$⊢ M = pmap (K)$
4		pmapj2.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		pmapj2.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
6		simp1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in HL$
7		hllat	$⊢ K \in HL \to K \in Lat$
8	7	3ad2ant1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in Lat$
9		hlop	$⊢ K \in HL \to K \in OP$
10	9	3ad2ant1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in OP$
11		simp2	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \in B$
12		eqid	$⊢ oc (K) = oc (K)$
13	1 12	opoccl	$⊢ (K \in OP \land X \in B) \to oc (K) (X) \in B$
14	10 11 13	syl2anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to oc (K) (X) \in B$
15		simp3	$⊢ (K \in HL \land X \in B \land Y \in B) \to Y \in B$
16	1 12	opoccl	$⊢ (K \in OP \land Y \in B) \to oc (K) (Y) \in B$
17	10 15 16	syl2anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to oc (K) (Y) \in B$
18		eqid	$⊢ meet (K) = meet (K)$
19	1 18	latmcl	$⊢ (K \in Lat \land oc (K) (X) \in B \land oc (K) (Y) \in B) \to oc (K) (X) meet (K) oc (K) (Y) \in B$
20	8 14 17 19	syl3anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to oc (K) (X) meet (K) oc (K) (Y) \in B$
21	1 12 3 5	polpmapN	$⊢ (K \in HL \land oc (K) (X) meet (K) oc (K) (Y) \in B) \to \underset{˙}{⊥} (M (oc (K) (X) meet (K) oc (K) (Y))) = M (oc (K) (oc (K) (X) meet (K) oc (K) (Y)))$
22	6 20 21	syl2anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (M (oc (K) (X) meet (K) oc (K) (Y))) = M (oc (K) (oc (K) (X) meet (K) oc (K) (Y)))$
23	1 12 3 5	polpmapN	$⊢ (K \in HL \land X \in B) \to \underset{˙}{⊥} (M (X)) = M (oc (K) (X))$
24	23	3adant3	$⊢ (K \in HL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (M (X)) = M (oc (K) (X))$
25	1 12 3 5	polpmapN	$⊢ (K \in HL \land Y \in B) \to \underset{˙}{⊥} (M (Y)) = M (oc (K) (Y))$
26	25	3adant2	$⊢ (K \in HL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (M (Y)) = M (oc (K) (Y))$
27	24 26	ineq12d	$⊢ (K \in HL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (M (X)) \cap \underset{˙}{⊥} (M (Y)) = M (oc (K) (X)) \cap M (oc (K) (Y))$
28		eqid	$⊢ Atoms (K) = Atoms (K)$
29	1 28 3	pmapssat	$⊢ (K \in HL \land X \in B) \to M (X) \subseteq Atoms (K)$
30	29	3adant3	$⊢ (K \in HL \land X \in B \land Y \in B) \to M (X) \subseteq Atoms (K)$
31	1 28 3	pmapssat	$⊢ (K \in HL \land Y \in B) \to M (Y) \subseteq Atoms (K)$
32	31	3adant2	$⊢ (K \in HL \land X \in B \land Y \in B) \to M (Y) \subseteq Atoms (K)$
33	28 4 5	poldmj1N	$⊢ (K \in HL \land M (X) \subseteq Atoms (K) \land M (Y) \subseteq Atoms (K)) \to \underset{˙}{⊥} (M (X) \underset{˙}{+} M (Y)) = \underset{˙}{⊥} (M (X)) \cap \underset{˙}{⊥} (M (Y))$
34	6 30 32 33	syl3anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (M (X) \underset{˙}{+} M (Y)) = \underset{˙}{⊥} (M (X)) \cap \underset{˙}{⊥} (M (Y))$
35	1 18 28 3	pmapmeet	$⊢ (K \in HL \land oc (K) (X) \in B \land oc (K) (Y) \in B) \to M (oc (K) (X) meet (K) oc (K) (Y)) = M (oc (K) (X)) \cap M (oc (K) (Y))$
36	6 14 17 35	syl3anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to M (oc (K) (X) meet (K) oc (K) (Y)) = M (oc (K) (X)) \cap M (oc (K) (Y))$
37	27 34 36	3eqtr4rd	$⊢ (K \in HL \land X \in B \land Y \in B) \to M (oc (K) (X) meet (K) oc (K) (Y)) = \underset{˙}{⊥} (M (X) \underset{˙}{+} M (Y))$
38	37	fveq2d	$⊢ (K \in HL \land X \in B \land Y \in B) \to \underset{˙}{⊥} (M (oc (K) (X) meet (K) oc (K) (Y))) = \underset{˙}{⊥} (\underset{˙}{⊥} (M (X) \underset{˙}{+} M (Y)))$
39		hlol	$⊢ K \in HL \to K \in OL$
40	1 2 18 12	oldmm4	$⊢ (K \in OL \land X \in B \land Y \in B) \to oc (K) (oc (K) (X) meet (K) oc (K) (Y)) = X \underset{˙}{\lor} Y$
41	39 40	syl3an1	$⊢ (K \in HL \land X \in B \land Y \in B) \to oc (K) (oc (K) (X) meet (K) oc (K) (Y)) = X \underset{˙}{\lor} Y$
42	41	fveq2d	$⊢ (K \in HL \land X \in B \land Y \in B) \to M (oc (K) (oc (K) (X) meet (K) oc (K) (Y))) = M (X \underset{˙}{\lor} Y)$
43	22 38 42	3eqtr3rd	$⊢ (K \in HL \land X \in B \land Y \in B) \to M (X \underset{˙}{\lor} Y) = \underset{˙}{⊥} (\underset{˙}{⊥} (M (X) \underset{˙}{+} M (Y)))$

Metamath Proof Explorer

Theorem pmapj2N

Proof