Theorem pl42lem2N

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

	Ref	Expression
Hypotheses	pl42lem.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pl42lem.l	⊢ ≤ = ( le ‘ 𝐾 )
	pl42lem.j	⊢ ∨ = ( join ‘ 𝐾 )
	pl42lem.m	⊢ ∧ = ( meet ‘ 𝐾 )
	pl42lem.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	pl42lem.f	⊢ 𝐹 = ( pmap ‘ 𝐾 )
	pl42lem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	pl42lem2N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pl42lem.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pl42lem.l	⊢ ≤ = ( le ‘ 𝐾 )
3		pl42lem.j	⊢ ∨ = ( join ‘ 𝐾 )
4		pl42lem.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		pl42lem.o	⊢ ⊥ = ( oc ‘ 𝐾 )
6		pl42lem.f	⊢ 𝐹 = ( pmap ‘ 𝐾 )
7		pl42lem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
8		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝐾 ∈ HL )
9	8	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
10		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
12	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
13	9 10 11 12	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
14		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
15	1 14 6	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
16	8 13 15	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
17		simpr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
18	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑊 ) ∈ 𝐵 )
19	9 10 17 18	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑊 ) ∈ 𝐵 )
20		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑉 ∈ 𝐵 )
21	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑉 ) ∈ 𝐵 )
22	9 11 20 21	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝑌 ∨ 𝑉 ) ∈ 𝐵 )
23	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑉 ) ∈ 𝐵 ) → ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ∈ 𝐵 )
24	9 19 22 23	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ∈ 𝐵 )
25	1 14 6	pmapssat	⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ⊆ ( Atoms ‘ 𝐾 ) )
26	8 24 25	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ⊆ ( Atoms ‘ 𝐾 ) )
27	8 16 26	3jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ⊆ ( Atoms ‘ 𝐾 ) ) )
28	1 3 6 7	pmapjoin	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) )
29	9 10 11 28	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) )
30	1 3 6 7	pmapjoin	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ 𝑊 ) ) )
31	9 10 17 30	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ 𝑊 ) ) )
32	1 3 6 7	pmapjoin	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ⊆ ( 𝐹 ‘ ( 𝑌 ∨ 𝑉 ) ) )
33	9 11 20 32	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ⊆ ( 𝐹 ‘ ( 𝑌 ∨ 𝑉 ) ) )
34		ss2in	⊢ ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ 𝑊 ) ) ∧ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ⊆ ( 𝐹 ‘ ( 𝑌 ∨ 𝑉 ) ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ⊆ ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑊 ) ) ∩ ( 𝐹 ‘ ( 𝑌 ∨ 𝑉 ) ) ) )
35	31 33 34	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ⊆ ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑊 ) ) ∩ ( 𝐹 ‘ ( 𝑌 ∨ 𝑉 ) ) ) )
36	1 4 14 6	pmapmeet	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑊 ) ∈ 𝐵 ∧ ( 𝑌 ∨ 𝑉 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑊 ) ) ∩ ( 𝐹 ‘ ( 𝑌 ∨ 𝑉 ) ) ) )
37	8 19 22 36	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) = ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑊 ) ) ∩ ( 𝐹 ‘ ( 𝑌 ∨ 𝑉 ) ) ) )
38	35 37	sseqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) )
39	29 38	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
40	14 7	paddss12	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) ⊆ ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) + ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) ) )
41	27 39 40	sylc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) ⊆ ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) + ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
42	1 3 6 7	pmapjoin	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) + ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
43	9 13 24 42	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) + ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
44	41 43	sstrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )