pl42lem4N

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	pl42lem4N	$⊢ ((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{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W)) \to F ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} 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	1 2 3 4 5 6 7	pl42lem1N	$⊢ ((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{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W)) \to F ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) = (((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V))$
9	8	3impia	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to F ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) = (((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V)$
10	1 2 3 4 5 6 7	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))$
11		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$
12	11	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$
13		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$
14		eqid	$⊢ PSubSp (K) = PSubSp (K)$
15	1 14 6	pmapsub	$⊢ (K \in Lat \land X \in B) \to F (X) \in PSubSp (K)$
16	12 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) \in PSubSp (K)$
17		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$
18	1 14 6	pmapsub	$⊢ (K \in Lat \land Y \in B) \to F (Y) \in PSubSp (K)$
19	12 17 18	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) \in PSubSp (K)$
20		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$
21	1 14 6	pmapsub	$⊢ (K \in Lat \land W \in B) \to F (W) \in PSubSp (K)$
22	12 20 21	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) \in PSubSp (K)$
23		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$
24	1 14 6	pmapsub	$⊢ (K \in Lat \land V \in B) \to F (V) \in PSubSp (K)$
25	12 23 24	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) \in PSubSp (K)$
26	14 7	pmodl42N	$⊢ ((K \in HL \land F (X) \in PSubSp (K) \land F (Y) \in PSubSp (K)) \land (F (W) \in PSubSp (K) \land F (V) \in PSubSp (K))) \to ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (W)) \cap ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V)) = (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} ((F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V)))$
27	11 16 19 22 25 26	syl32anc	$⊢ ((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 (W)) \cap ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V)) = (F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} ((F (X) \underset{˙}{+} F (W)) \cap (F (Y) \underset{˙}{+} F (V)))$
28	1 2 3 4 5 6 7	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)))$
29	27 28	eqsstrd	$⊢ ((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 (W)) \cap ((F (X) \underset{˙}{+} F (Y)) \underset{˙}{+} F (V)) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
30	10 29	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)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
31	30	3adant3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to (((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
32	9 31	eqsstrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (Z \in B \land W \in B \land V \in B) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to F ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V)))$
33	32	3expia	$⊢ ((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{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W)) \to F ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) \subseteq F ((X \underset{˙}{\lor} Y) \underset{˙}{\lor} ((X \underset{˙}{\lor} W) \underset{˙}{\land} (Y \underset{˙}{\lor} V))))$

Metamath Proof Explorer

Theorem pl42lem4N

Proof