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 ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝑄𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄𝑆 ( 𝑃 𝑄 ) ) ) → ( ¬ 𝑆 𝑊𝑆𝑅 ) )