pmapjat2

Description: The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012)

	Ref	Expression
Hypotheses	pmapjat.b	$⊢ B = {Base}_{K}$
	pmapjat.j	$⊢ \underset{˙}{\lor} = join (K)$
	pmapjat.a	$⊢ A = Atoms (K)$
	pmapjat.m	$⊢ M = pmap (K)$
	pmapjat.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmapjat2	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (Q \underset{˙}{\lor} X) = M (Q) \underset{˙}{+} M (X)$

Proof

Step	Hyp	Ref	Expression
1		pmapjat.b	$⊢ B = {Base}_{K}$
2		pmapjat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pmapjat.a	$⊢ A = Atoms (K)$
4		pmapjat.m	$⊢ M = pmap (K)$
5		pmapjat.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
6	1 2 3 4 5	pmapjat1	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (X \underset{˙}{\lor} Q) = M (X) \underset{˙}{+} M (Q)$
7		hllat	$⊢ K \in HL \to K \in Lat$
8	7	3ad2ant1	$⊢ (K \in HL \land X \in B \land Q \in A) \to K \in Lat$
9	1 3	atbase	$⊢ Q \in A \to Q \in B$
10	9	3ad2ant3	$⊢ (K \in HL \land X \in B \land Q \in A) \to Q \in B$
11		simp2	$⊢ (K \in HL \land X \in B \land Q \in A) \to X \in B$
12	1 2	latjcom	$⊢ (K \in Lat \land Q \in B \land X \in B) \to Q \underset{˙}{\lor} X = X \underset{˙}{\lor} Q$
13	8 10 11 12	syl3anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to Q \underset{˙}{\lor} X = X \underset{˙}{\lor} Q$
14	13	fveq2d	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (Q \underset{˙}{\lor} X) = M (X \underset{˙}{\lor} Q)$
15		simp1	$⊢ (K \in HL \land X \in B \land Q \in A) \to K \in HL$
16	1 3 4	pmapssat	$⊢ (K \in HL \land Q \in B) \to M (Q) \subseteq A$
17	15 10 16	syl2anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (Q) \subseteq A$
18	1 3 4	pmapssat	$⊢ (K \in HL \land X \in B) \to M (X) \subseteq A$
19	18	3adant3	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (X) \subseteq A$
20	3 5	paddcom	$⊢ (K \in Lat \land M (Q) \subseteq A \land M (X) \subseteq A) \to M (Q) \underset{˙}{+} M (X) = M (X) \underset{˙}{+} M (Q)$
21	8 17 19 20	syl3anc	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (Q) \underset{˙}{+} M (X) = M (X) \underset{˙}{+} M (Q)$
22	6 14 21	3eqtr4d	$⊢ (K \in HL \land X \in B \land Q \in A) \to M (Q \underset{˙}{\lor} X) = M (Q) \underset{˙}{+} M (X)$

Metamath Proof Explorer

Theorem pmapjat2

Proof