| Step |
Hyp |
Ref |
Expression |
| 1 |
|
trlcone.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
| 2 |
|
trlcone.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
| 3 |
|
trlcone.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
| 4 |
|
trlcone.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
| 5 |
|
simpl3l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) |
| 6 |
|
simp11 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
| 7 |
|
simp12l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 ) |
| 8 |
2 3
|
ltrncnv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 ) |
| 9 |
6 7 8
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ◡ 𝐹 ∈ 𝑇 ) |
| 10 |
|
simp12r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 ) |
| 11 |
2 3
|
ltrnco |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) |
| 12 |
6 7 10 11
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) |
| 13 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
| 14 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 15 |
13 14 2 3 4
|
trlco |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ◡ 𝐹 ∈ 𝑇 ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ ◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 16 |
6 9 12 15
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ) ( le ‘ 𝐾 ) ( ( 𝑅 ‘ ◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 17 |
|
coass |
⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) |
| 18 |
1 2 3
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) |
| 19 |
6 7 18
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 ) |
| 20 |
|
f1ococnv1 |
⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ) |
| 21 |
19 20
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ) |
| 22 |
21
|
coeq1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ( I ↾ 𝐵 ) ∘ 𝐺 ) ) |
| 23 |
1 2 3
|
ltrn1o |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) |
| 24 |
6 10 23
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) |
| 25 |
|
f1of |
⊢ ( 𝐺 : 𝐵 –1-1-onto→ 𝐵 → 𝐺 : 𝐵 ⟶ 𝐵 ) |
| 26 |
|
fcoi2 |
⊢ ( 𝐺 : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 ) |
| 27 |
24 25 26
|
3syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 ) |
| 28 |
22 27
|
eqtrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = 𝐺 ) |
| 29 |
17 28
|
syl5reqr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ) |
| 30 |
29
|
fveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 31 |
|
simp11l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐾 ∈ HL ) |
| 32 |
|
simp2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 33 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
| 34 |
14 33
|
hlatjidm |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
| 35 |
31 32 34
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ) = ( 𝑅 ‘ 𝐹 ) ) |
| 36 |
2 3 4
|
trlcnv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) ) |
| 37 |
6 7 36
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ ◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) ) |
| 38 |
37
|
eqcomd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ◡ 𝐹 ) ) |
| 39 |
|
simp3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) |
| 40 |
38 39
|
oveq12d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ) = ( ( 𝑅 ‘ ◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 41 |
35 40
|
eqtr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑅 ‘ ◡ 𝐹 ) ( join ‘ 𝐾 ) ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 42 |
16 30 41
|
3brtr4d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ( le ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ) |
| 43 |
|
hlatl |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat ) |
| 44 |
31 43
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐾 ∈ AtLat ) |
| 45 |
|
simp13r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) ) |
| 46 |
1 33 2 3 4
|
trlnidat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 47 |
6 10 45 46
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ) |
| 48 |
13 33
|
atcmp |
⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐺 ) ( le ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) ) |
| 49 |
44 47 32 48
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ( le ‘ 𝐾 ) ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) ) |
| 50 |
42 49
|
mpbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) |
| 51 |
50
|
eqcomd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) |
| 52 |
51
|
3expia |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ) |
| 53 |
52
|
necon3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) |
| 54 |
5 53
|
mpd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) |
| 55 |
|
simpl3r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) ) |
| 56 |
|
simpl1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
| 57 |
|
simpl2r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐺 ∈ 𝑇 ) |
| 58 |
|
eqid |
⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 ) |
| 59 |
1 58 2 3 4
|
trlid0b |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝐺 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) ) |
| 60 |
56 57 59
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐺 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) ) |
| 61 |
60
|
necon3bid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐺 ≠ ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐺 ) ≠ ( 0. ‘ 𝐾 ) ) ) |
| 62 |
55 61
|
mpbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 0. ‘ 𝐾 ) ) |
| 63 |
62
|
necomd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 0. ‘ 𝐾 ) ≠ ( 𝑅 ‘ 𝐺 ) ) |
| 64 |
|
simpr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) |
| 65 |
|
simpl2l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐹 ∈ 𝑇 ) |
| 66 |
1 58 2 3 4
|
trlid0b |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) ) |
| 67 |
56 65 66
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) ) |
| 68 |
64 67
|
mpbird |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐹 = ( I ↾ 𝐵 ) ) |
| 69 |
68
|
coeq1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = ( ( I ↾ 𝐵 ) ∘ 𝐺 ) ) |
| 70 |
56 57 23
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐵 ) |
| 71 |
70 25 26
|
3syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( ( I ↾ 𝐵 ) ∘ 𝐺 ) = 𝐺 ) |
| 72 |
69 71
|
eqtrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐹 ∘ 𝐺 ) = 𝐺 ) |
| 73 |
72
|
fveq2d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝑅 ‘ 𝐺 ) ) |
| 74 |
63 64 73
|
3netr4d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) |
| 75 |
|
simp1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
| 76 |
|
simp2l |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → 𝐹 ∈ 𝑇 ) |
| 77 |
58 33 2 3 4
|
trlator0 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∨ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) ) |
| 78 |
75 76 77
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∨ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) ) |
| 79 |
54 74 78
|
mpjaodan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ) |