pl42lem1N

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	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))$

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		simp11	$⊢ ((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 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) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to K \in Lat$
10		simp12	$⊢ ((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 X \in B$
11		simp13	$⊢ ((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 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) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to X \underset{˙}{\lor} Y \in B$
14		simp21	$⊢ ((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 Z \in B$
15	1 4	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
16	9 13 14 15	syl3anc	$⊢ ((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 (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
17		simp22	$⊢ ((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 W \in B$
18	1 3	latjcl	$⊢ (K \in Lat \land (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B \land W \in B) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W \in B$
19	9 16 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) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W \in B$
20		simp23	$⊢ ((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 V \in B$
21		eqid	$⊢ Atoms (K) = Atoms (K)$
22	1 4 21 6	pmapmeet	$⊢ (K \in HL \land ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W \in B \land V \in B) \to F ((((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \underset{˙}{\land} V) = F (((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \cap F (V)$
23	8 19 20 22	syl3anc	$⊢ ((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{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) \cap F (V)$
24		hlop	$⊢ K \in HL \to K \in OP$
25	8 24	syl	$⊢ ((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 K \in OP$
26	1 5	opoccl	$⊢ (K \in OP \land W \in B) \to \underset{˙}{⊥} (W) \in B$
27	25 17 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) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to \underset{˙}{⊥} (W) \in B$
28	1 2 4	latmle2	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
29	9 13 14 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) \land (X \underset{˙}{\leq} \underset{˙}{⊥} (Y) \land Z \underset{˙}{\leq} \underset{˙}{⊥} (W))) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\leq} Z$
30		simp3r	$⊢ ((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 Z \underset{˙}{\leq} \underset{˙}{⊥} (W)$
31	1 2 9 16 14 27 29 30	lattrd	$⊢ ((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 ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\leq} \underset{˙}{⊥} (W)$
32	1 2 3 6 5 7	pmapojoinN	$⊢ ((K \in HL \land (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B \land W \in B) \land ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\leq} \underset{˙}{⊥} (W)) \to F (((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\lor} W) = F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{+} F (W)$
33	8 16 17 31 32	syl31anc	$⊢ ((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) = F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{+} F (W)$
34	1 4 21 6	pmapmeet	$⊢ (K \in HL \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) = F (X \underset{˙}{\lor} Y) \cap F (Z)$
35	8 13 14 34	syl3anc	$⊢ ((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) = F (X \underset{˙}{\lor} Y) \cap F (Z)$
36		simp3l	$⊢ ((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 X \underset{˙}{\leq} \underset{˙}{⊥} (Y)$
37	1 2 3 6 5 7	pmapojoinN	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{\leq} \underset{˙}{⊥} (Y)) \to F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y)$
38	8 10 11 36 37	syl31anc	$⊢ ((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) = F (X) \underset{˙}{+} F (Y)$
39	38	ineq1d	$⊢ ((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) \cap F (Z) = (F (X) \underset{˙}{+} F (Y)) \cap F (Z)$
40	35 39	eqtrd	$⊢ ((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) = (F (X) \underset{˙}{+} F (Y)) \cap F (Z)$
41	40	oveq1d	$⊢ ((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{˙}{+} F (W) = ((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)$
42	33 41	eqtrd	$⊢ ((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) = ((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)$
43	42	ineq1d	$⊢ ((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) \cap F (V) = (((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V)$
44	23 43	eqtrd	$⊢ ((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)$
45	44	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) = (((F (X) \underset{˙}{+} F (Y)) \cap F (Z)) \underset{˙}{+} F (W)) \cap F (V))$

Metamath Proof Explorer

Theorem pl42lem1N

Proof