Metamath Proof Explorer

Theorem 2atm2atN

Description: Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2atm2at.j ⊢ ∨ = ( join ‘ 𝐾 )
2atm2at.m ⊢ ∧ = ( meet ‘ 𝐾 )
2atm2at.z ⊢ 0 = ( 0. ‘ 𝐾 )
2atm2at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2atm2atN ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 2atm2at.j ⊢ ∨ = ( join ‘ 𝐾 )
2 2atm2at.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 2atm2at.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 2atm2at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
6 5 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ OP )
7 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
8 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
9 3 8 4 0ltat ⊢ ( ( 𝐾 ∈ OP ∧ 𝑅 ∈ 𝐴 ) → 0 ( lt ‘ 𝐾 ) 𝑅 )
10 6 7 9 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 0 ( lt ‘ 𝐾 ) 𝑅 )
11 simpl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
12 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
13 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
14 13 1 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑃 ) )
15 11 7 12 14 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑃 ) )
16 simpr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
17 13 1 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑄 ) )
18 11 7 16 17 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑄 ) )
19 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
20 19 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
23 7 22 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
24 21 1 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
25 11 7 12 24 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) )
26 21 1 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
27 11 7 16 26 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
28 21 13 2 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑃 ) ∧ 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑄 ) ) ↔ 𝑅 ( le ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ) )
29 20 23 25 27 28 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑃 ) ∧ 𝑅 ( le ‘ 𝐾 ) ( 𝑅 ∨ 𝑄 ) ) ↔ 𝑅 ( le ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ) )
30 15 18 29 mpbi2and ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ( le ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) )
31 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
32 31 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ Poset )
33 21 3 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
34 6 33 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 0 ∈ ( Base ‘ 𝐾 ) )
35 21 2 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∨ 𝑃 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
36 20 25 27 35 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
37 21 13 8 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 0 ( lt ‘ 𝐾 ) 𝑅 ∧ 𝑅 ( le ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ) → 0 ( lt ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ) )
38 32 34 23 36 37 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 0 ( lt ‘ 𝐾 ) 𝑅 ∧ 𝑅 ( le ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ) → 0 ( lt ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ) )
39 10 30 38 mp2and ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 0 ( lt ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) )
40 21 8 3 opltn0 ⊢ ( ( 𝐾 ∈ OP ∧ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 0 ( lt ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ↔ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ≠ 0 ) )
41 6 36 40 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 0 ( lt ‘ 𝐾 ) ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ↔ ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ≠ 0 ) )
42 39 41 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑅 ∨ 𝑃 ) ∧ ( 𝑅 ∨ 𝑄 ) ) ≠ 0 )