Metamath Proof Explorer

Theorem lhpmcvr3

Description: Specialization of lhpmcvr2 . TODO: Use this to simplify many uses of ( P .\/ ( X ./\ W ) ) = X to become P .<_ X . (Contributed by NM, 6-Apr-2014)

Ref Expression
Hypotheses lhpmcvr2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpmcvr2.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpmcvr2.j ⊢ ∨ = ( join ‘ 𝐾 )
lhpmcvr2.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpmcvr2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpmcvr2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmcvr3 ( ( ( 𝐾 ∈ 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 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → 𝐾 ∈ HL )
8 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ∈ 𝐴 )
9 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
10 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → 𝑊 ∈ 𝐻 )
11 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
12 10 11 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → 𝑊 ∈ 𝐵 )
13 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ≤ 𝑋 )
14 1 2 3 4 5 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑊 ) ) )
15 7 8 9 12 13 14 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑋 ∧ ( 𝑃 ∨ 𝑊 ) ) )
16 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
18 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
19 2 3 18 5 6 lhpjat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
20 16 17 19 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
21 20 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑋 ∧ ( 𝑃 ∨ 𝑊 ) ) = ( 𝑋 ∧ ( 1. ‘ 𝐾 ) ) )
22 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
23 7 22 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → 𝐾 ∈ OL )
24 1 4 18 olm11 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ ( 1. ‘ 𝐾 ) ) = 𝑋 )
25 23 9 24 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑋 ∧ ( 1. ‘ 𝐾 ) ) = 𝑋 )
26 15 21 25 3eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
27 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝐾 ∈ HL )
28 27 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝐾 ∈ Lat )
29 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑃 ∈ 𝐴 )
30 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
31 29 30 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑃 ∈ 𝐵 )
32 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑋 ∈ 𝐵 )
33 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑊 ∈ 𝐻 )
34 33 11 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑊 ∈ 𝐵 )
35 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
36 28 32 34 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
37 1 2 3 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → 𝑃 ≤ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) )
38 28 31 36 37 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑃 ≤ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) )
39 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 )
40 38 39 breqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑃 ≤ 𝑋 )
41 26 40 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )