Step | Hyp | Ref
| Expression |
1 | | eqop 7803 |
. . . . 5
⊢ (𝑔 ∈ (𝑇 × 𝐸) → (𝑔 = 〈(𝑠‘𝐹), 0 〉 ↔
((1st ‘𝑔)
= (𝑠‘𝐹) ∧ (2nd
‘𝑔) = 0
))) |
2 | 1 | adantl 485 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (𝑔 = 〈(𝑠‘𝐹), 0 〉 ↔
((1st ‘𝑔)
= (𝑠‘𝐹) ∧ (2nd
‘𝑔) = 0
))) |
3 | 2 | rexbidv 3216 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (∃𝑠 ∈ 𝐸 𝑔 = 〈(𝑠‘𝐹), 0 〉 ↔ ∃𝑠 ∈ 𝐸 ((1st ‘𝑔) = (𝑠‘𝐹) ∧ (2nd ‘𝑔) = 0 ))) |
4 | | r19.41v 3260 |
. . . 4
⊢
(∃𝑠 ∈
𝐸 ((1st
‘𝑔) = (𝑠‘𝐹) ∧ (2nd ‘𝑔) = 0 ) ↔ (∃𝑠 ∈ 𝐸 (1st ‘𝑔) = (𝑠‘𝐹) ∧ (2nd ‘𝑔) = 0 )) |
5 | | fvex 6730 |
. . . . . . . 8
⊢
(1st ‘𝑔) ∈ V |
6 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑓 = (1st ‘𝑔) → (𝑓 = (𝑠‘𝐹) ↔ (1st ‘𝑔) = (𝑠‘𝐹))) |
7 | 6 | rexbidv 3216 |
. . . . . . . 8
⊢ (𝑓 = (1st ‘𝑔) → (∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹) ↔ ∃𝑠 ∈ 𝐸 (1st ‘𝑔) = (𝑠‘𝐹))) |
8 | 5, 7 | elab 3587 |
. . . . . . 7
⊢
((1st ‘𝑔) ∈ {𝑓 ∣ ∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹)} ↔ ∃𝑠 ∈ 𝐸 (1st ‘𝑔) = (𝑠‘𝐹)) |
9 | | dvhb1dim.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝐾) |
10 | | dvhb1dim.h |
. . . . . . . . . 10
⊢ 𝐻 = (LHyp‘𝐾) |
11 | | dvhb1dim.t |
. . . . . . . . . 10
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
12 | | dvhb1dim.r |
. . . . . . . . . 10
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
13 | | dvhb1dim.e |
. . . . . . . . . 10
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
14 | 9, 10, 11, 12, 13 | dva1dim 38736 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → {𝑓 ∣ ∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹)} = {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ (𝑅‘𝐹)}) |
15 | 14 | adantr 484 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → {𝑓 ∣ ∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹)} = {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ (𝑅‘𝐹)}) |
16 | 15 | eleq2d 2823 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → ((1st ‘𝑔) ∈ {𝑓 ∣ ∃𝑠 ∈ 𝐸 𝑓 = (𝑠‘𝐹)} ↔ (1st ‘𝑔) ∈ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ (𝑅‘𝐹)})) |
17 | 8, 16 | bitr3id 288 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (∃𝑠 ∈ 𝐸 (1st ‘𝑔) = (𝑠‘𝐹) ↔ (1st ‘𝑔) ∈ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ (𝑅‘𝐹)})) |
18 | | xp1st 7793 |
. . . . . . . 8
⊢ (𝑔 ∈ (𝑇 × 𝐸) → (1st ‘𝑔) ∈ 𝑇) |
19 | 18 | adantl 485 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (1st ‘𝑔) ∈ 𝑇) |
20 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑓 = (1st ‘𝑔) → (𝑅‘𝑓) = (𝑅‘(1st ‘𝑔))) |
21 | 20 | breq1d 5063 |
. . . . . . . 8
⊢ (𝑓 = (1st ‘𝑔) → ((𝑅‘𝑓) ≤ (𝑅‘𝐹) ↔ (𝑅‘(1st ‘𝑔)) ≤ (𝑅‘𝐹))) |
22 | 21 | elrab3 3603 |
. . . . . . 7
⊢
((1st ‘𝑔) ∈ 𝑇 → ((1st ‘𝑔) ∈ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ (𝑅‘𝐹)} ↔ (𝑅‘(1st ‘𝑔)) ≤ (𝑅‘𝐹))) |
23 | 19, 22 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → ((1st ‘𝑔) ∈ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ (𝑅‘𝐹)} ↔ (𝑅‘(1st ‘𝑔)) ≤ (𝑅‘𝐹))) |
24 | 17, 23 | bitrd 282 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (∃𝑠 ∈ 𝐸 (1st ‘𝑔) = (𝑠‘𝐹) ↔ (𝑅‘(1st ‘𝑔)) ≤ (𝑅‘𝐹))) |
25 | 24 | anbi1d 633 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → ((∃𝑠 ∈ 𝐸 (1st ‘𝑔) = (𝑠‘𝐹) ∧ (2nd ‘𝑔) = 0 ) ↔ ((𝑅‘(1st
‘𝑔)) ≤ (𝑅‘𝐹) ∧ (2nd ‘𝑔) = 0 ))) |
26 | 4, 25 | syl5bb 286 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (∃𝑠 ∈ 𝐸 ((1st ‘𝑔) = (𝑠‘𝐹) ∧ (2nd ‘𝑔) = 0 ) ↔ ((𝑅‘(1st
‘𝑔)) ≤ (𝑅‘𝐹) ∧ (2nd ‘𝑔) = 0 ))) |
27 | 3, 26 | bitrd 282 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ 𝑔 ∈ (𝑇 × 𝐸)) → (∃𝑠 ∈ 𝐸 𝑔 = 〈(𝑠‘𝐹), 0 〉 ↔ ((𝑅‘(1st
‘𝑔)) ≤ (𝑅‘𝐹) ∧ (2nd ‘𝑔) = 0 ))) |
28 | 27 | rabbidva 3388 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → {𝑔 ∈ (𝑇 × 𝐸) ∣ ∃𝑠 ∈ 𝐸 𝑔 = 〈(𝑠‘𝐹), 0 〉} = {𝑔 ∈ (𝑇 × 𝐸) ∣ ((𝑅‘(1st ‘𝑔)) ≤ (𝑅‘𝐹) ∧ (2nd ‘𝑔) = 0 )}) |