Metamath Proof Explorer

Theorem pl42lem3N

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 pl42lem3N ( ( ( 𝐾 ∈ 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 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
10 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
11 1 10 6 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
12 8 9 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) )
13 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
14 1 10 6 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
15 8 13 14 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
16 10 7 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
17 8 12 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
18 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑊 ∈ 𝐵 )
19 1 10 6 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) )
20 8 18 19 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) )
21 inss1 ⊢ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) ⊆ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) )
22 10 7 paddss1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) ⊆ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ⊆ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ) )
23 21 22 mpi ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝐹 ‘ 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ⊆ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) )
24 8 17 20 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ⊆ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) )
25 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → 𝑉 ∈ 𝐵 )
26 1 10 6 pmapssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑉 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑉 ) ⊆ ( Atoms ‘ 𝐾 ) )
27 8 25 26 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑉 ) ⊆ ( Atoms ‘ 𝐾 ) )
28 10 7 sspadd2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑉 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝐹 ‘ 𝑉 ) ⊆ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) )
29 8 27 17 28 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑉 ) ⊆ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) )
30 ss2in ⊢ ( ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ⊆ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑉 ) ⊆ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) ) → ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ⊆ ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) ) )
31 24 29 30 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵 ) ) → ( ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) ∩ ( 𝐹 ‘ 𝑍 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( 𝐹 ‘ 𝑉 ) ) ⊆ ( ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑊 ) ) ∩ ( ( ( 𝐹 ‘ 𝑋 ) + ( 𝐹 ‘ 𝑌 ) ) + ( 𝐹 ‘ 𝑉 ) ) ) )