| Step |
Hyp |
Ref |
Expression |
| 1 |
|
trlcl.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
trlcl.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
| 3 |
|
trlcl.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
| 4 |
|
trlcl.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
| 5 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
| 6 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
| 7 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
| 8 |
5 6 7 2
|
lhpocnel |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) |
| 9 |
8
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) |
| 10 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 11 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
| 12 |
5 10 11 7 2 3 4
|
trlval2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) |
| 13 |
9 12
|
mpd3an3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) ) |
| 14 |
|
hllat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat ) |
| 15 |
14
|
ad2antrr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐾 ∈ Lat ) |
| 16 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
| 17 |
16
|
ad2antrr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐾 ∈ OP ) |
| 18 |
1 2
|
lhpbase |
⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 ) |
| 19 |
18
|
ad2antlr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝑊 ∈ 𝐵 ) |
| 20 |
1 6
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐵 ) |
| 21 |
17 19 20
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐵 ) |
| 22 |
1 2 3
|
ltrncl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ 𝐵 ) |
| 23 |
21 22
|
mpd3an3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ 𝐵 ) |
| 24 |
1 10
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ 𝐵 ) |
| 25 |
15 21 23 24
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ 𝐵 ) |
| 26 |
1 11
|
latmcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ) |
| 27 |
15 25 19 26
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( join ‘ 𝐾 ) ( 𝐹 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( meet ‘ 𝐾 ) 𝑊 ) ∈ 𝐵 ) |
| 28 |
13 27
|
eqeltrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ) |