| Step |
Hyp |
Ref |
Expression |
| 1 |
|
trljco.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
| 2 |
|
trljco.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
| 3 |
|
trljco.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
| 4 |
|
trljco.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
| 5 |
|
coeq1 |
⊢ ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) ) |
| 6 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
| 7 |
6 2 3
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
| 8 |
7
|
3adant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
| 9 |
|
f1of |
⊢ ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) ) |
| 10 |
|
fcoi2 |
⊢ ( 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) = 𝐺 ) |
| 11 |
8 9 10
|
3syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( I ↾ ( Base ‘ 𝐾 ) ) ∘ 𝐺 ) = 𝐺 ) |
| 12 |
5 11
|
sylan9eqr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ∘ 𝐺 ) = 𝐺 ) |
| 13 |
12
|
fveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑅 ‘ 𝐺 ) ) |
| 14 |
13
|
oveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 15 |
|
simp1l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐾 ∈ HL ) |
| 16 |
15
|
hllatd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐾 ∈ Lat ) |
| 17 |
6 2 3 4
|
trlcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) |
| 18 |
17
|
3adant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) |
| 19 |
6 1
|
latjidm |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
| 20 |
16 18 19
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
| 21 |
|
hlol |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL ) |
| 22 |
15 21
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐾 ∈ OL ) |
| 23 |
|
eqid |
⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 ) |
| 24 |
6 1 23
|
olj01 |
⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
| 25 |
22 18 24
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
| 26 |
20 25
|
eqtr4d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) ) |
| 27 |
26
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) ) |
| 28 |
|
coeq2 |
⊢ ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = ( 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) |
| 29 |
6 2 3
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
| 30 |
29
|
3adant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) ) |
| 31 |
|
f1of |
⊢ ( 𝐹 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐹 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) ) |
| 32 |
|
fcoi1 |
⊢ ( 𝐹 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) → ( 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = 𝐹 ) |
| 33 |
30 31 32
|
3syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ ( I ↾ ( Base ‘ 𝐾 ) ) ) = 𝐹 ) |
| 34 |
28 33
|
sylan9eqr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝐹 ∘ 𝐺 ) = 𝐹 ) |
| 35 |
34
|
fveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
| 36 |
35
|
oveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ) |
| 37 |
6 23 2 3 4
|
trlid0b |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) ) |
| 38 |
37
|
3adant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) ) |
| 39 |
38
|
biimpa |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) |
| 40 |
39
|
oveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 0. ‘ 𝐾 ) ) ) |
| 41 |
27 36 40
|
3eqtr4d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ 𝐺 = ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 42 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
| 43 |
16
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → 𝐾 ∈ Lat ) |
| 44 |
|
simp1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
| 45 |
2 3
|
ltrnco |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) |
| 46 |
6 2 3 4
|
trlcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 47 |
44 45 46
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 48 |
6 1
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 49 |
16 18 47 48
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 50 |
49
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 51 |
6 2 3 4
|
trlcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) |
| 52 |
51
|
3adant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) |
| 53 |
6 1
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 54 |
16 18 52 53
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 55 |
54
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) |
| 56 |
6 42 1
|
latlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 57 |
16 18 52 56
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 58 |
42 1 2 3 4
|
trlco |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 59 |
6 42 1
|
latjle12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) |
| 60 |
16 18 47 54 59
|
syl13anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) |
| 61 |
57 58 60
|
mpbi2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 62 |
61
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 63 |
|
simpr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) |
| 64 |
63
|
oveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 65 |
6 42 1
|
latlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 66 |
16 18 47 65
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 67 |
20 66
|
eqbrtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 68 |
67
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 69 |
64 68
|
eqbrtrrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 70 |
6 42 43 50 55 62 69
|
latasymd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 71 |
61
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 72 |
|
simpl1l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL ) |
| 73 |
|
simpl1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
| 74 |
|
simpl2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 ) |
| 75 |
|
simpr1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) |
| 76 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
| 77 |
6 76 2 3 4
|
trlnidat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 78 |
73 74 75 77
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 79 |
|
simpl3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 ) |
| 80 |
74 79
|
jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) |
| 81 |
|
simpr3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) |
| 82 |
76 2 3 4
|
trlcoat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 83 |
73 80 81 82
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 84 |
|
simpr2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) |
| 85 |
6 2 3 4
|
trlcone |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) |
| 86 |
73 80 81 84 85
|
syl112anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) |
| 87 |
6 76 2 3 4
|
trlnidat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 88 |
73 79 84 87
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 89 |
42 1 76
|
ps-1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) |
| 90 |
72 78 83 86 78 88 89
|
syl132anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) |
| 91 |
71 90
|
mpbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝐹 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ 𝐺 ≠ ( I ↾ ( Base ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |
| 92 |
14 41 70 91
|
pm2.61da3ne |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) |