Metamath Proof Explorer

Theorem lhpmcvr4N

Description: Specialization of lhpmcvr2 . (Contributed by NM, 6-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lhpmcvr2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpmcvr2.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpmcvr2.j ⊢ ∨ = ( join ‘ 𝐾 )
lhpmcvr2.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpmcvr2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpmcvr2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmcvr4N ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ¬ 𝑃 ≤ 𝑌 )

Proof

Step Hyp Ref Expression
1 lhpmcvr2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhpmcvr2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lhpmcvr2.j ⊢ ∨ = ( join ‘ 𝐾 )
4 lhpmcvr2.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 lhpmcvr2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 lhpmcvr2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 simp2rr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ¬ 𝑃 ≤ 𝑊 )
8 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑃 ≤ 𝑋 )
9 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
10 9 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
11 simp2rl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐴 )
12 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
13 11 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐵 )
14 simp2ll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
15 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑌 ∈ 𝐵 )
16 1 2 4 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ↔ 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ) )
17 10 13 14 15 16 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) ↔ 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ) )
18 17 biimpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌 ) → 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ) )
19 8 18 mpand ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑃 ≤ 𝑌 → 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ) )
20 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 )
21 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
22 10 14 15 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
23 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑊 ∈ 𝐻 )
24 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
25 23 24 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → 𝑊 ∈ 𝐵 )
26 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑃 ≤ 𝑊 ) )
27 10 13 22 25 26 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ) → 𝑃 ≤ 𝑊 ) )
28 20 27 mpan2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑃 ≤ ( 𝑋 ∧ 𝑌 ) → 𝑃 ≤ 𝑊 ) )
29 19 28 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ( 𝑃 ≤ 𝑌 → 𝑃 ≤ 𝑊 ) )
30 7 29 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋 ) ) → ¬ 𝑃 ≤ 𝑌 )