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