Step |
Hyp |
Ref |
Expression |
1 |
|
cdlemg12.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
cdlemg12.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
cdlemg12.m |
⊢ ∧ = ( meet ‘ 𝐾 ) |
4 |
|
cdlemg12.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
5 |
|
cdlemg12.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
6 |
|
cdlemg12.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
7 |
|
cdlemg12b.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
8 |
|
cdlemg12e.z |
⊢ 0 = ( 0. ‘ 𝐾 ) |
9 |
|
simp33 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) |
10 |
|
simpl1 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) |
11 |
|
simpl21 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝐹 ∈ 𝑇 ) |
12 |
|
simpl22 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝐺 ∈ 𝑇 ) |
13 |
|
simpl23 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝑃 ≠ 𝑄 ) |
14 |
|
simpl31 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ) |
15 |
|
simpl32 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ) |
16 |
1 2 3 4 5 6 7
|
cdlemg12d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) ) ) |
17 |
10 11 12 13 14 15 16
|
syl123anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐺 ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) ) ) |
18 |
|
simpr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) |
19 |
18
|
oveq2d |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ 0 ) ) |
20 |
|
simp11l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL ) |
21 |
20
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝐾 ∈ HL ) |
22 |
|
hlol |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL ) |
23 |
21 22
|
syl |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝐾 ∈ OL ) |
24 |
|
simpl11 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
25 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
26 |
25 5 6 7
|
trlcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) |
27 |
24 11 26
|
syl2anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) |
28 |
25 2 8
|
olj01 |
⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ 0 ) = ( 𝑅 ‘ 𝐹 ) ) |
29 |
23 27 28
|
syl2anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ 0 ) = ( 𝑅 ‘ 𝐹 ) ) |
30 |
19 29
|
eqtrd |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) ) = ( 𝑅 ‘ 𝐹 ) ) |
31 |
17 30
|
breqtrd |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑅 ‘ 𝐹 ) ) |
32 |
|
hlatl |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat ) |
33 |
21 32
|
syl |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝐾 ∈ AtLat ) |
34 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
35 |
21 34
|
syl |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝐾 ∈ OP ) |
36 |
25 5 6 7
|
trlcl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) |
37 |
24 12 36
|
syl2anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) |
38 |
|
simp12l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐴 ) |
39 |
38
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝑃 ∈ 𝐴 ) |
40 |
|
simp13l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ∈ 𝐴 ) |
41 |
40
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝑄 ∈ 𝐴 ) |
42 |
25 2 4
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) |
43 |
21 39 41 42
|
syl3anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) |
44 |
25 1 8
|
opnlen0 |
⊢ ( ( ( 𝐾 ∈ OP ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑅 ‘ 𝐺 ) ≠ 0 ) |
45 |
35 37 43 15 44
|
syl31anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐺 ) ≠ 0 ) |
46 |
|
simp11r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑊 ∈ 𝐻 ) |
47 |
46
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → 𝑊 ∈ 𝐻 ) |
48 |
8 4 5 6 7
|
trlatn0 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ↔ ( 𝑅 ‘ 𝐺 ) ≠ 0 ) ) |
49 |
21 47 12 48
|
syl21anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ↔ ( 𝑅 ‘ 𝐺 ) ≠ 0 ) ) |
50 |
45 49
|
mpbird |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ) |
51 |
25 1 8
|
opnlen0 |
⊢ ( ( ( 𝐾 ∈ OP ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 0 ) |
52 |
35 27 43 14 51
|
syl31anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐹 ) ≠ 0 ) |
53 |
8 4 5 6 7
|
trlatn0 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ↔ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ) |
54 |
21 47 11 53
|
syl21anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ↔ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ) |
55 |
52 54
|
mpbird |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) |
56 |
1 4
|
atcmp |
⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) → ( ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) ) |
57 |
33 50 55 56
|
syl3anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) ) |
58 |
31 57
|
mpbid |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐺 ) = ( 𝑅 ‘ 𝐹 ) ) |
59 |
58
|
eqcomd |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 ) → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) |
60 |
59
|
ex |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) = 0 → ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝐺 ) ) ) |
61 |
60
|
necon3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) ≠ 0 ) ) |
62 |
9 61
|
mpd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ) ∧ ( ¬ ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ ( 𝑅 ‘ 𝐺 ) ≤ ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑃 ) ) ∨ 𝑃 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑄 ) ) ∨ 𝑄 ) ) ≠ 0 ) |