| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lplncvrlvol2.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
| 2 |
|
lplncvrlvol2.c |
⊢ 𝐶 = ( ⋖ ‘ 𝐾 ) |
| 3 |
|
lplncvrlvol2.p |
⊢ 𝑃 = ( LPlanes ‘ 𝐾 ) |
| 4 |
|
lplncvrlvol2.v |
⊢ 𝑉 = ( LVols ‘ 𝐾 ) |
| 5 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 ) |
| 6 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ HL ) |
| 7 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝑉 ) |
| 8 |
3 4
|
lvolnelpln |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑌 ∈ 𝑃 ) |
| 9 |
6 7 8
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → ¬ 𝑌 ∈ 𝑃 ) |
| 10 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝑃 ) |
| 11 |
|
eleq1 |
⊢ ( 𝑋 = 𝑌 → ( 𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑃 ) ) |
| 12 |
10 11
|
syl5ibcom |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 = 𝑌 → 𝑌 ∈ 𝑃 ) ) |
| 13 |
12
|
necon3bd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → ( ¬ 𝑌 ∈ 𝑃 → 𝑋 ≠ 𝑌 ) ) |
| 14 |
9 13
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≠ 𝑌 ) |
| 15 |
|
eqid |
⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 ) |
| 16 |
1 15
|
pltval |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
| 17 |
16
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
| 18 |
5 14 17
|
mpbir2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) |
| 19 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝐾 ∈ HL ) |
| 20 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ 𝑃 ) |
| 21 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
| 22 |
21 3
|
lplnbase |
⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
| 23 |
20 22
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
| 24 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ 𝑉 ) |
| 25 |
21 4
|
lvolbase |
⊢ ( 𝑌 ∈ 𝑉 → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
| 26 |
24 25
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
| 27 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) |
| 28 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 29 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
| 30 |
21 1 15 28 2 29
|
hlrelat3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) |
| 31 |
19 23 26 27 30
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) |
| 32 |
21 1 28 29 4
|
islvol2 |
⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑉 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) ) ) |
| 33 |
32
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( 𝑌 ∈ 𝑉 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) ) ) |
| 34 |
|
simpr |
⊢ ( ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) |
| 35 |
21 1 28 29 3
|
islpln2 |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ) ) |
| 36 |
|
simp3rl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ) |
| 37 |
|
simp3rr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) |
| 38 |
|
simp133 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) |
| 39 |
38
|
oveq1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) |
| 40 |
|
simp23 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) |
| 41 |
37 39 40
|
3brtr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ≤ ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) |
| 42 |
|
simp11 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ) |
| 43 |
|
simp12 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) |
| 44 |
|
simp3l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) |
| 45 |
|
simp21l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) |
| 46 |
43 44 45
|
3jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) |
| 47 |
|
simp21r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) |
| 48 |
|
simp22l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑣 ∈ ( Atoms ‘ 𝐾 ) ) |
| 49 |
|
simp22r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) |
| 50 |
47 48 49
|
3jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ) |
| 51 |
|
simp131 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑝 ≠ 𝑞 ) |
| 52 |
|
simp132 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) |
| 53 |
36 38 39
|
3brtr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) 𝐶 ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) |
| 54 |
|
simp111 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝐾 ∈ HL ) |
| 55 |
54
|
hllatd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝐾 ∈ Lat ) |
| 56 |
21 28 29
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) |
| 57 |
42 56
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) |
| 58 |
21 29
|
atbase |
⊢ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → 𝑟 ∈ ( Base ‘ 𝐾 ) ) |
| 59 |
43 58
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) ) |
| 60 |
21 28
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ ( Base ‘ 𝐾 ) ) |
| 61 |
55 57 59 60
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ ( Base ‘ 𝐾 ) ) |
| 62 |
21 1 28 2 29
|
cvr1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) 𝐶 ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) |
| 63 |
54 61 44 62
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) 𝐶 ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) |
| 64 |
53 63
|
mpbird |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) |
| 65 |
1 28 29
|
4at2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ≤ ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ↔ ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) |
| 66 |
42 46 50 51 52 64 65
|
syl33anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ≤ ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ↔ ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) |
| 67 |
41 66
|
mpbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) |
| 68 |
67 39 40
|
3eqtr4d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) = 𝑌 ) |
| 69 |
36 68
|
breqtrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) ∧ ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) ) → 𝑋 𝐶 𝑌 ) |
| 70 |
69
|
3exp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 ) ) ) |
| 71 |
70
|
exp4a |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 72 |
71
|
3expd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) |
| 73 |
72
|
rexlimdv3a |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 74 |
73
|
3expib |
⊢ ( 𝐾 ∈ HL → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) ) |
| 75 |
74
|
rexlimdvv |
⊢ ( 𝐾 ∈ HL → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 76 |
75
|
adantld |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑋 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 77 |
35 76
|
sylbid |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 → ( ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 78 |
77
|
imp31 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) |
| 79 |
34 78
|
syl7 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) |
| 80 |
79
|
rexlimdvv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 81 |
80
|
rexlimdvva |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 82 |
81
|
adantld |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑣 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑤 ∈ ( Atoms ‘ 𝐾 ) ( ( 𝑡 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ) ∧ 𝑌 = ( ( ( 𝑡 ( join ‘ 𝐾 ) 𝑢 ) ( join ‘ 𝐾 ) 𝑣 ) ( join ‘ 𝐾 ) 𝑤 ) ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 83 |
33 82
|
sylbid |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ( 𝑌 ∈ 𝑉 → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 84 |
83
|
3impia |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) |
| 85 |
84
|
rexlimdv |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) |
| 86 |
85
|
imp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑠 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 ) |
| 87 |
31 86
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) |
| 88 |
18 87
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) |