Step | Hyp | Ref
| Expression |
1 | | dibval3.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
2 | | dibval3.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
3 | | dibval3.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
4 | | dibval3.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
5 | | dibval3.o |
. . . 4
⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
6 | | eqid 2610 |
. . . 4
⊢
((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊) |
7 | | dibval3.i |
. . . 4
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
8 | 1, 2, 3, 4, 5, 6, 7 | dibval2 35451 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 })) |
9 | 8 | eleq2d 2673 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑋) ↔ 𝑌 ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 }))) |
10 | | dibval3.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
11 | 1, 2, 3, 4, 10, 6 | diaelval 35340 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
12 | 11 | anbi1d 737 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋) ∧ 𝑌 = 〈𝑓, 0 〉))) |
13 | | an13 836 |
. . . . . . . 8
⊢ ((𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
14 | | velsn 4141 |
. . . . . . . . 9
⊢ (𝑠 ∈ { 0 } ↔ 𝑠 = 0 ) |
15 | 14 | anbi1i 727 |
. . . . . . . 8
⊢ ((𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉)) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
16 | 13, 15 | bitri 263 |
. . . . . . 7
⊢ ((𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
17 | 16 | exbii 1764 |
. . . . . 6
⊢
(∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ ∃𝑠(𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
18 | | fvex 6113 |
. . . . . . . . . 10
⊢
((LTrn‘𝐾)‘𝑊) ∈ V |
19 | 4, 18 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝑇 ∈ V |
20 | 19 | mptex 6390 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V |
21 | 5, 20 | eqeltri 2684 |
. . . . . . 7
⊢ 0 ∈
V |
22 | | opeq2 4341 |
. . . . . . . . 9
⊢ (𝑠 = 0 → 〈𝑓, 𝑠〉 = 〈𝑓, 0 〉) |
23 | 22 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑠 = 0 → (𝑌 = 〈𝑓, 𝑠〉 ↔ 𝑌 = 〈𝑓, 0 〉)) |
24 | 23 | anbi2d 736 |
. . . . . . 7
⊢ (𝑠 = 0 → ((𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉) ↔ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉))) |
25 | 21, 24 | ceqsexv 3215 |
. . . . . 6
⊢
(∃𝑠(𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉)) ↔ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
26 | 17, 25 | bitri 263 |
. . . . 5
⊢
(∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
27 | | anass 679 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑇 ∧ 𝑌 = 〈𝑓, 0 〉) ∧ (𝑅‘𝑓) ≤ 𝑋) ↔ (𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
28 | | an32 835 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑇 ∧ 𝑌 = 〈𝑓, 0 〉) ∧ (𝑅‘𝑓) ≤ 𝑋) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
29 | 27, 28 | bitr3i 265 |
. . . . 5
⊢ ((𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
30 | 12, 26, 29 | 3bitr4g 302 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋)))) |
31 | 30 | exbidv 1837 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (∃𝑓∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ ∃𝑓(𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋)))) |
32 | | elxp 5055 |
. . 3
⊢ (𝑌 ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 }) ↔ ∃𝑓∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 }))) |
33 | | df-rex 2902 |
. . 3
⊢
(∃𝑓 ∈
𝑇 (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋) ↔ ∃𝑓(𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
34 | 31, 32, 33 | 3bitr4g 302 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 }) ↔ ∃𝑓 ∈ 𝑇 (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
35 | 9, 34 | bitrd 267 |
1
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑋) ↔ ∃𝑓 ∈ 𝑇 (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |