This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lhp2at0

Description: Join and meet with different atoms under co-atom W . (Contributed by NM, 15-Jun-2013)

Ref Expression
Hypotheses lhp2at0.l ⊢ ≤ = ( le ‘ 𝐾 )
lhp2at0.j ⊢ ∨ = ( join ‘ 𝐾 )
lhp2at0.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhp2at0.z ⊢ 0 = ( 0. ‘ 𝐾 )
lhp2at0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhp2at0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhp2at0 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑉 ) = 0 )

Proof

Step Hyp Ref Expression
1 lhp2at0.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhp2at0.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lhp2at0.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 lhp2at0.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 lhp2at0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 lhp2at0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
8 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
9 7 8 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
10 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
11 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑈 ∈ 𝐴 )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 2 5 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
14 7 10 11 13 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
15 simp11r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
16 12 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
17 15 16 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
18 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ∈ 𝐴 )
19 12 5 atbase ⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
20 18 19 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ∈ ( Base ‘ 𝐾 ) )
21 12 3 latmassOLD ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) ∧ 𝑉 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑊 ∧ 𝑉 ) ) )
22 9 14 17 20 21 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) ∧ 𝑉 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑊 ∧ 𝑉 ) ) )
23 1 3 4 5 6 lhpmat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = 0 )
24 23 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) → ( 𝑃 ∧ 𝑊 ) = 0 )
25 24 3ad2ant1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑃 ∧ 𝑊 ) = 0 )
26 25 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∧ 𝑊 ) ∨ 𝑈 ) = ( 0 ∨ 𝑈 ) )
27 12 5 atbase ⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
28 11 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
29 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑈 ≤ 𝑊 )
30 12 1 2 3 5 atmod4i2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( ( 𝑃 ∧ 𝑊 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) )
31 7 10 28 17 29 30 syl131anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∧ 𝑊 ) ∨ 𝑈 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) )
32 12 2 4 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → ( 0 ∨ 𝑈 ) = 𝑈 )
33 9 28 32 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 0 ∨ 𝑈 ) = 𝑈 )
34 26 31 33 3eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) = 𝑈 )
35 34 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑊 ) ∧ 𝑉 ) = ( 𝑈 ∧ 𝑉 ) )
36 22 35 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑊 ∧ 𝑉 ) ) = ( 𝑈 ∧ 𝑉 ) )
37 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ≤ 𝑊 )
38 7 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
39 12 1 3 latleeqm2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑉 ≤ 𝑊 ↔ ( 𝑊 ∧ 𝑉 ) = 𝑉 ) )
40 38 20 17 39 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑉 ≤ 𝑊 ↔ ( 𝑊 ∧ 𝑉 ) = 𝑉 ) )
41 37 40 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑊 ∧ 𝑉 ) = 𝑉 )
42 41 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑊 ∧ 𝑉 ) ) = ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑉 ) )
43 simp13 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑈 ≠ 𝑉 )
44 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
45 7 44 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ AtLat )
46 3 4 5 atnem0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑈 ≠ 𝑉 ↔ ( 𝑈 ∧ 𝑉 ) = 0 ) )
47 45 11 18 46 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑈 ≠ 𝑉 ↔ ( 𝑈 ∧ 𝑉 ) = 0 ) )
48 43 47 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑈 ∧ 𝑉 ) = 0 )
49 36 42 48 3eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑉 ) = 0 )