Metamath Proof Explorer

Theorem lhpat3

Description: There is only one atom under both P .\/ Q and co-atom W . (Contributed by NM, 21-Nov-2012)

Ref Expression
Hypotheses lhpat.l ⊢ ≤ = ( le ‘ 𝐾 )
lhpat.j ⊢ ∨ = ( join ‘ 𝐾 )
lhpat.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lhpat2.r ⊢ 𝑅 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion lhpat3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑆 ≤ 𝑊 ↔ 𝑆 ≠ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 lhpat.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhpat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lhpat.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 lhpat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lhpat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 lhpat2.r ⊢ 𝑅 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 simpl3r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
8 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑆 ≤ 𝑊 )
9 simp1ll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
10 9 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ Lat )
11 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ 𝐴 )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
14 11 13 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
15 simp1rl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
16 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
17 12 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
18 9 15 16 17 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
19 simp1lr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ 𝐻 )
20 12 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 19 20 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
22 12 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ 𝑊 ) ↔ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
23 10 14 18 21 22 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ 𝑊 ) ↔ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
24 23 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → ( ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ 𝑊 ) ↔ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
25 7 8 24 mpbi2and ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
26 25 6 breqtrrdi ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑆 ≤ 𝑅 )
27 9 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝐾 ∈ HL )
28 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
29 27 28 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝐾 ∈ AtLat )
30 simpl2r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑆 ∈ 𝐴 )
31 simpl1l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32 simpl1r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
33 simpl2l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑄 ∈ 𝐴 )
34 simpl3l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑃 ≠ 𝑄 )
35 1 2 3 4 5 6 lhpat2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑅 ∈ 𝐴 )
36 31 32 33 34 35 syl112anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑅 ∈ 𝐴 )
37 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑆 ≤ 𝑅 ↔ 𝑆 = 𝑅 ) )
38 29 30 36 37 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → ( 𝑆 ≤ 𝑅 ↔ 𝑆 = 𝑅 ) )
39 26 38 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑆 ≤ 𝑊 ) → 𝑆 = 𝑅 )
40 39 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ≤ 𝑊 → 𝑆 = 𝑅 ) )
41 12 1 3 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
42 10 18 21 41 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
43 6 42 eqbrtrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑅 ≤ 𝑊 )
44 breq1 ⊢ ( 𝑆 = 𝑅 → ( 𝑆 ≤ 𝑊 ↔ 𝑅 ≤ 𝑊 ) )
45 43 44 syl5ibrcom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 = 𝑅 → 𝑆 ≤ 𝑊 ) )
46 40 45 impbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑆 ≤ 𝑊 ↔ 𝑆 = 𝑅 ) )
47 46 necon3bbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑆 ≤ 𝑊 ↔ 𝑆 ≠ 𝑅 ) )