pl42lem2N

Description: Lemma for pl42N . (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pl42lem.b	$⊢ B = {Base}_{K}$
	pl42lem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pl42lem.j	$⊢ \underset{˙}{\lor} = join (K)$
	pl42lem.m	$⊢ \underset{˙}{\land} = meet (K)$
	pl42lem.o	$⊢ \underset{˙}{⊥} = oc (K)$
	pl42lem.f	$⊢ F = pmap (K)$
	pl42lem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pl42lem2N	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} ((F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V))) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$

Proof

Step	Hyp	Ref	Expression
1		pl42lem.b	$⊢ B = {Base}_{K}$
2		pl42lem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pl42lem.j	$⊢ \underset{˙}{\lor} = join (K)$
4		pl42lem.m	$⊢ \underset{˙}{\land} = meet (K)$
5		pl42lem.o	$⊢ \underset{˙}{⊥} = oc (K)$
6		pl42lem.f	$⊢ F = pmap (K)$
7		pl42lem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
8		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to K \in HL$
9	8	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to K \in Lat$
10		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to X \in B$
11		simpl3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to Y \in B$
12	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
13	9 10 11 12	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to X \underset{˙}{\lor} Y \in B$
14		eqid	$⊢ Atoms (K) = Atoms (K)$
15	1 14 6	pmapssat	$⊢ (K \in HL \land X \underset{˙}{\lor} Y \in B) \to F (X \underset{˙}{\lor} Y) \subseteq Atoms (K)$
16	8 13 15	syl2anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to F (X \underset{˙}{\lor} Y) \subseteq Atoms (K)$
17		simpr2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to W \in B$
18	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\lor} W \in B$
19	9 10 17 18	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to X \underset{˙}{\lor} W \in B$
20		simpr3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to V \in B$
21	1 3	latjcl	$⊢ (K \in Lat \land Y \in B \land V \in B) \to Y \underset{˙}{\lor} V \in B$
22	9 11 20 21	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to Y \underset{˙}{\lor} V \in B$
23	1 4	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} W \in B \land Y \underset{˙}{\lor} V \in B) \to (X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V) \in B$
24	9 19 22 23	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V) \in B$
25	1 14 6	pmapssat	$⊢ (K \in HL \land (X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V) \in B) \to F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \subseteq Atoms (K)$
26	8 24 25	syl2anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \subseteq Atoms (K)$
27	8 16 26	3jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (K \in HL \land F (X \underset{˙}{\lor} Y) \subseteq Atoms (K) \land F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \subseteq Atoms (K))$
28	1 3 6 7	pmapjoin	$⊢ (K \in Lat \land X \in B \land Y \in B) \to F (X) \underset{˙}{+} F (Y) \subseteq F (X \underset{˙}{\lor} Y)$
29	9 10 11 28	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to F (X) \underset{˙}{+} F (Y) \subseteq F (X \underset{˙}{\lor} Y)$
30	1 3 6 7	pmapjoin	$⊢ (K \in Lat \land X \in B \land W \in B) \to F (X) \underset{˙}{+} F (W) \subseteq F (X \underset{˙}{\lor} W)$
31	9 10 17 30	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to F (X) \underset{˙}{+} F (W) \subseteq F (X \underset{˙}{\lor} W)$
32	1 3 6 7	pmapjoin	$⊢ (K \in Lat \land Y \in B \land V \in B) \to F (Y) \underset{˙}{+} F (V) \subseteq F (Y \underset{˙}{\lor} V)$
33	9 11 20 32	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to F (Y) \underset{˙}{+} F (V) \subseteq F (Y \underset{˙}{\lor} V)$
34		ss2in	$⊢ (F (X) \underset{˙}{+} F (W) \subseteq F (X \underset{˙}{\lor} W) \land F (Y) \underset{˙}{+} F (V) \subseteq F (Y \underset{˙}{\lor} V)) \to (F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V)) \subseteq F (X \underset{˙}{\lor} W) \cap F (Y \underset{˙}{\lor} V)$
35	31 33 34	syl2anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V)) \subseteq F (X \underset{˙}{\lor} W) \cap F (Y \underset{˙}{\lor} V)$
36	1 4 14 6	pmapmeet	$⊢ (K \in HL \land X \underset{˙}{\lor} W \in B \land Y \underset{˙}{\lor} V \in B) \to F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) = F (X \underset{˙}{\lor} W) \cap F (Y \underset{˙}{\lor} V)$
37	8 19 22 36	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) = F (X \underset{˙}{\lor} W) \cap F (Y \underset{˙}{\lor} V)$
38	35 37	sseqtrrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V)) \subseteq F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))$
39	29 38	jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (F (X) \underset{˙}{+} F (Y) \subseteq F (X \underset{˙}{\lor} Y) \land (F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V)) \subseteq F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
40	14 7	paddss12	$⊢ (K \in HL \land F (X \underset{˙}{\lor} Y) \subseteq Atoms (K) \land F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \subseteq Atoms (K)) \to ((F (X) \underset{˙}{+} F (Y) \subseteq F (X \underset{˙}{\lor} Y) \land (F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V)) \subseteq F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))) \to (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} ((F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V))) \subseteq F (X \underset{˙}{\lor} Y) \underset{˙}{+} F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
41	27 39 40	sylc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} ((F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V))) \subseteq F (X \underset{˙}{\lor} Y) \underset{˙}{+} F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))$
42	1 3 6 7	pmapjoin	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land (X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V) \in B) \to F (X \underset{˙}{\lor} Y) \underset{˙}{+} F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
43	9 13 24 42	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to F (X \underset{˙}{\lor} Y) \underset{˙}{+} F ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
44	41 43	sstrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B)) \to (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} ((F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V))) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$

Metamath Proof Explorer

Theorem pl42lem2N

Proof