This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( 𝐹 ‘ 𝑌 ) + ( 𝐹 ‘ 𝑉 ) ) ) ) ⊆ ( 𝐹 ‘ ( ( 𝑋 ∨ 𝑌 ) ∨ ( ( 𝑋 ∨ 𝑊 ) ∧ ( 𝑌 ∨ 𝑉 ) ) ) ) )