Step |
Hyp |
Ref |
Expression |
1 |
|
ltrnset.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
ltrnset.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
ltrnset.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
4 |
|
ltrnset.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
ltrnset.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
6 |
|
ltrnset.d |
⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) |
7 |
|
ltrnset.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
1 2 3 4 5 6 7
|
isltrn |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) ) |
9 |
|
3simpa |
⊢ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) |
10 |
9
|
imim1i |
⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
11 |
|
3anass |
⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) ) |
12 |
|
3anrot |
⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ↔ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) ) |
13 |
|
df-ne |
⊢ ( 𝑝 ≠ 𝑞 ↔ ¬ 𝑝 = 𝑞 ) |
14 |
13
|
anbi1i |
⊢ ( ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) ) |
15 |
11 12 14
|
3bitr3i |
⊢ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) ↔ ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) ) |
16 |
15
|
imbi1i |
⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
17 |
|
impexp |
⊢ ( ( ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) |
18 |
16 17
|
bitri |
⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) |
19 |
|
id |
⊢ ( 𝑝 = 𝑞 → 𝑝 = 𝑞 ) |
20 |
|
fveq2 |
⊢ ( 𝑝 = 𝑞 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ) |
21 |
19 20
|
oveq12d |
⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) = ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ) |
22 |
21
|
oveq1d |
⊢ ( 𝑝 = 𝑞 → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) |
23 |
22
|
a1d |
⊢ ( 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
24 |
|
pm2.61 |
⊢ ( ( 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) → ( ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) |
25 |
23 24
|
ax-mp |
⊢ ( ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
26 |
18 25
|
sylbi |
⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
27 |
10 26
|
impbii |
⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
28 |
27
|
2ralbii |
⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) |
29 |
28
|
anbi2i |
⊢ ( ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) |
30 |
8 29
|
bitrdi |
⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) ) |