Theorem pl42lem4N

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	pl42lem4N	⊢ ( ( ( 𝐾 ∈ 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	1 2 3 4 5 6 7	pl42lem1N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ) )
9	8	3impia	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) )
10	1 2 3 4 5 6 7	pl42lem3N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ⊆ ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) ) )
11		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝐾 ∈ HL )
12	11	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
13		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
14		eqid	⊢ ( PSubSp ‘ 𝐾 ) = ( PSubSp ‘ 𝐾 )
15	1 14 6	pmapsub	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( PSubSp ‘ 𝐾 ) )
16	12 13 15	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( PSubSp ‘ 𝐾 ) )
17		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
18	1 14 6	pmapsub	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ ( PSubSp ‘ 𝐾 ) )
19	12 17 18	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ ( PSubSp ‘ 𝐾 ) )
20		simpr2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
21	1 14 6	pmapsub	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑊 ) ∈ ( PSubSp ‘ 𝐾 ) )
22	12 20 21	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑊 ) ∈ ( PSubSp ‘ 𝐾 ) )
23		simpr3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑉 ∈ 𝐵 )
24	1 14 6	pmapsub	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑉 ) ∈ ( PSubSp ‘ 𝐾 ) )
25	12 23 24	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑉 ) ∈ ( PSubSp ‘ 𝐾 ) )
26	14 7	pmodl42N	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( PSubSp ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑌 ) ∈ ( PSubSp ‘ 𝐾 ) ) ∧ ( ( 𝐹 ‘ 𝑊 ) ∈ ( PSubSp ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑉 ) ∈ ( PSubSp ‘ 𝐾 ) ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) ) = ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) )
27	11 16 19 22 25 26	syl32anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) ) = ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) )
28	1 2 3 4 5 6 7	pl42lem2N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
29	27 28	eqsstrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
30	10 29	sstrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
31	30	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
32	9 31	eqsstrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ∧ ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )
33	32	3expia	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( ⊥ ‘ 𝑌 ) ∧ 𝑍 ≤ ( ⊥ ‘ 𝑊 ) ) → ( 𝐹 ‘ ( ( ( ( 𝑋 ∨ 𝑌 ) ∧ 𝑍 ) ∨ 𝑊 ) ∧ 𝑉 ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) ) )