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

Metamath Proof Explorer

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