Step |
Hyp |
Ref |
Expression |
1 |
|
trl0a.z |
⊢ 0 = ( 0. ‘ 𝐾 ) |
2 |
|
trl0a.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
3 |
|
trl0a.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
4 |
|
trl0a.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
trl0a.r |
⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
|
df-ne |
⊢ ( ( 𝑅 ‘ 𝐹 ) ≠ 0 ↔ ¬ ( 𝑅 ‘ 𝐹 ) = 0 ) |
7 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
8 |
7 2 3
|
lhpexnle |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) |
9 |
8
|
ad2antrr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) |
10 |
|
simplll |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
11 |
|
simpr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) |
12 |
|
simpllr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → 𝐹 ∈ 𝑇 ) |
13 |
|
simplr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 0 ) |
14 |
10
|
adantr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
15 |
|
simplr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) |
16 |
12
|
adantr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → 𝐹 ∈ 𝑇 ) |
17 |
|
simpr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) |
18 |
7 1 2 3 4 5
|
trl0 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → ( 𝑅 ‘ 𝐹 ) = 0 ) |
19 |
14 15 16 17 18
|
syl112anc |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑅 ‘ 𝐹 ) = 0 ) |
20 |
19
|
ex |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐹 ‘ 𝑝 ) = 𝑝 → ( 𝑅 ‘ 𝐹 ) = 0 ) ) |
21 |
20
|
necon3d |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝑅 ‘ 𝐹 ) ≠ 0 → ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) |
22 |
13 21
|
mpd |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) |
23 |
7 2 3 4 5
|
trlat |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) |
24 |
10 11 12 22 23
|
syl112anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) |
25 |
9 24
|
rexlimddv |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) |
26 |
25
|
ex |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ≠ 0 → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) ) |
27 |
6 26
|
syl5bir |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ¬ ( 𝑅 ‘ 𝐹 ) = 0 → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) ) |
28 |
27
|
orrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) = 0 ∨ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) ) |
29 |
28
|
orcomd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∨ ( 𝑅 ‘ 𝐹 ) = 0 ) ) |