pl42lem3N

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	pl42lem3N	$⊢ ((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)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V) \subseteq ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W)) \cap ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (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		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$
10		eqid	$⊢ Atoms (K) = Atoms (K)$
11	1 10 6	pmapssat	$⊢ (K \in HL \land X \in B) \to F (X) \subseteq Atoms (K)$
12	8 9 11	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) \subseteq Atoms (K)$
13		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$
14	1 10 6	pmapssat	$⊢ (K \in HL \land Y \in B) \to F (Y) \subseteq Atoms (K)$
15	8 13 14	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 (Y) \subseteq Atoms (K)$
16	10 7	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)$
17	8 12 15 16	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 Atoms (K)$
18		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$
19	1 10 6	pmapssat	$⊢ (K \in HL \land W \in B) \to F (W) \subseteq Atoms (K)$
20	8 18 19	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 (W) \subseteq Atoms (K)$
21		inss1	$⊢ (F (X) \underset{˙}{+} F (Y)) \cap F (Z) \subseteq F (X) \underset{˙}{+} F (Y)$
22	10 7	paddss1	$⊢ (K \in HL \land F (X) \underset{˙}{+} F (Y) \subseteq Atoms (K) \land F (W) \subseteq Atoms (K)) \to ((F (X) \underset{˙}{+} F (Y)) \cap F (Z) \subseteq F (X) \underset{˙}{+} F (Y) \to ((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W) \subseteq (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W))$
23	21 22	mpi	$⊢ (K \in HL \land F (X) \underset{˙}{+} F (Y) \subseteq Atoms (K) \land F (W) \subseteq Atoms (K)) \to ((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W) \subseteq (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W)$
24	8 17 20 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 ((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W) \subseteq (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W)$
25		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$
26	1 10 6	pmapssat	$⊢ (K \in HL \land V \in B) \to F (V) \subseteq Atoms (K)$
27	8 25 26	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 (V) \subseteq Atoms (K)$
28	10 7	sspadd2	$⊢ (K \in HL \land F (V) \subseteq Atoms (K) \land F (X) \underset{˙}{+} F (Y) \subseteq Atoms (K)) \to F (V) \subseteq (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V)$
29	8 27 17 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 (V) \subseteq (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V)$
30		ss2in	$⊢ (((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W) \subseteq (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W) \land F (V) \subseteq (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V)) \to (((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V) \subseteq ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W)) \cap ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V))$
31	24 29 30	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 (Y)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V) \subseteq ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W)) \cap ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V))$

Metamath Proof Explorer

Theorem pl42lem3N

Proof