pmapjlln1

Description: The projective map of the join of a lattice element and a lattice line (expressed as the join Q .\/ R of two atoms). (Contributed by NM, 16-Sep-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	pmapjlln1	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (X \underset{˙}{\lor} (Q \underset{˙}{\lor} R)) = M (X) \underset{˙}{+} M (Q \underset{˙}{\lor} R)$

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		simpl	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to K \in HL$
7	1 3 4	pmapssat	$⊢ (K \in HL \land X \in B) \to M (X) \subseteq A$
8	7	3ad2antr1	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (X) \subseteq A$
9		simpr2	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to Q \in A$
10	1 3	atbase	$⊢ Q \in A \to Q \in B$
11	9 10	syl	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to Q \in B$
12	1 3 4	pmapssat	$⊢ (K \in HL \land Q \in B) \to M (Q) \subseteq A$
13	11 12	syldan	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (Q) \subseteq A$
14		simpr3	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to R \in A$
15	1 3	atbase	$⊢ R \in A \to R \in B$
16	14 15	syl	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to R \in B$
17	1 3 4	pmapssat	$⊢ (K \in HL \land R \in B) \to M (R) \subseteq A$
18	16 17	syldan	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (R) \subseteq A$
19	3 5	paddass	$⊢ (K \in HL \land (M (X) \subseteq A \land M (Q) \subseteq A \land M (R) \subseteq A)) \to (M (X) \underset{˙}{+} M (Q)) \underset{˙}{+} M (R) = M (X) \underset{˙}{+} (M (Q) \underset{˙}{+} M (R))$
20	6 8 13 18 19	syl13anc	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to (M (X) \underset{˙}{+} M (Q)) \underset{˙}{+} M (R) = M (X) \underset{˙}{+} (M (Q) \underset{˙}{+} M (R))$
21		hllat	$⊢ K \in HL \to K \in Lat$
22	21	adantr	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to K \in Lat$
23		simpr1	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to X \in B$
24	1 2	latjcl	$⊢ (K \in Lat \land X \in B \land Q \in B) \to X \underset{˙}{\lor} Q \in B$
25	22 23 11 24	syl3anc	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to X \underset{˙}{\lor} Q \in B$
26	1 2 3 4 5	pmapjat1	$⊢ (K \in HL \land X \underset{˙}{\lor} Q \in B \land R \in A) \to M ((X \underset{˙}{\lor} Q) \underset{˙}{\lor} R) = M (X \underset{˙}{\lor} Q) \underset{˙}{+} M (R)$
27	6 25 14 26	syl3anc	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M ((X \underset{˙}{\lor} Q) \underset{˙}{\lor} R) = M (X \underset{˙}{\lor} Q) \underset{˙}{+} M (R)$
28	1 2	latjass	$⊢ (K \in Lat \land (X \in B \land Q \in B \land R \in B)) \to (X \underset{˙}{\lor} Q) \underset{˙}{\lor} R = X \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
29	22 23 11 16 28	syl13anc	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to (X \underset{˙}{\lor} Q) \underset{˙}{\lor} R = X \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
30	29	fveq2d	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M ((X \underset{˙}{\lor} Q) \underset{˙}{\lor} R) = M (X \underset{˙}{\lor} (Q \underset{˙}{\lor} R))$
31	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)$
32	31	3adant3r3	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (X \underset{˙}{\lor} Q) = M (X) \underset{˙}{+} M (Q)$
33	32	oveq1d	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (X \underset{˙}{\lor} Q) \underset{˙}{+} M (R) = (M (X) \underset{˙}{+} M (Q)) \underset{˙}{+} M (R)$
34	27 30 33	3eqtr3d	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (X \underset{˙}{\lor} (Q \underset{˙}{\lor} R)) = (M (X) \underset{˙}{+} M (Q)) \underset{˙}{+} M (R)$
35	1 2 3 4 5	pmapjat1	$⊢ (K \in HL \land Q \in B \land R \in A) \to M (Q \underset{˙}{\lor} R) = M (Q) \underset{˙}{+} M (R)$
36	6 11 14 35	syl3anc	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (Q \underset{˙}{\lor} R) = M (Q) \underset{˙}{+} M (R)$
37	36	oveq2d	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (X) \underset{˙}{+} M (Q \underset{˙}{\lor} R) = M (X) \underset{˙}{+} (M (Q) \underset{˙}{+} M (R))$
38	20 34 37	3eqtr4d	$⊢ (K \in HL \land (X \in B \land Q \in A \land R \in A)) \to M (X \underset{˙}{\lor} (Q \underset{˙}{\lor} R)) = M (X) \underset{˙}{+} M (Q \underset{˙}{\lor} R)$

Metamath Proof Explorer

Theorem pmapjlln1

Proof