Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme0.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
cdleme0.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
cdleme0.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
4 |
|
cdleme0.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
cdleme0.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
6 |
|
cdleme0.u |
⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) |
7 |
1 2 3 4 5 6
|
cdleme01N |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑈 ≠ 𝑃 ∧ 𝑈 ≠ 𝑄 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ 𝑊 ) ) |
8 |
|
simp1l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ HL ) |
9 |
|
hlcvl |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat ) |
10 |
8 9
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝐾 ∈ CvLat ) |
11 |
|
simp2ll |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ 𝐴 ) |
12 |
|
simp2rl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑄 ∈ 𝐴 ) |
13 |
|
simp1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
14 |
|
simp2l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) |
15 |
|
simp3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ≠ 𝑄 ) |
16 |
1 2 3 4 5 6
|
lhpat2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑈 ∈ 𝐴 ) |
17 |
13 14 12 15 16
|
syl112anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑈 ∈ 𝐴 ) |
18 |
4 1 2
|
cvlsupr2 |
⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑈 ) = ( 𝑄 ∨ 𝑈 ) ↔ ( 𝑈 ≠ 𝑃 ∧ 𝑈 ≠ 𝑄 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) |
19 |
10 11 12 17 15 18
|
syl131anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑈 ) = ( 𝑄 ∨ 𝑈 ) ↔ ( 𝑈 ≠ 𝑃 ∧ 𝑈 ≠ 𝑄 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ) |
20 |
19
|
anbi1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( ( 𝑃 ∨ 𝑈 ) = ( 𝑄 ∨ 𝑈 ) ∧ 𝑈 ≤ 𝑊 ) ↔ ( ( 𝑈 ≠ 𝑃 ∧ 𝑈 ≠ 𝑄 ∧ 𝑈 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ 𝑊 ) ) ) |
21 |
7 20
|
mpbird |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑈 ) = ( 𝑄 ∨ 𝑈 ) ∧ 𝑈 ≤ 𝑊 ) ) |