Step |
Hyp |
Ref |
Expression |
1 |
|
islvol5.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
islvol5.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
islvol5.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
4 |
|
islvol5.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
islvol5.v |
⊢ 𝑉 = ( LVols ‘ 𝐾 ) |
6 |
1 5
|
lvolbase |
⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐵 ) |
7 |
6
|
pm4.71ri |
⊢ ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) |
8 |
1 2 3 4 5
|
islvol5 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) |
9 |
8
|
pm5.32da |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) |
10 |
7 9
|
syl5bb |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ) ∧ 𝑋 = ( ( ( 𝑝 ∨ 𝑞 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) ) |