Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΎ β HL β§ π β π»)) |
2 | | dib1dim.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | dib1dim.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | dib1dim.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
5 | | dib1dim.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
6 | 2, 3, 4, 5 | trlcl 39035 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β π΅) |
7 | | eqid 2733 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
8 | 7, 3, 4, 5 | trlle 39055 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ)(leβπΎ)π) |
9 | | dib1dim.o |
. . . . 5
β’ π = (β β π β¦ ( I βΎ π΅)) |
10 | | eqid 2733 |
. . . . 5
β’
((DIsoAβπΎ)βπ) = ((DIsoAβπΎ)βπ) |
11 | | dib1dim.i |
. . . . 5
β’ πΌ = ((DIsoBβπΎ)βπ) |
12 | 2, 7, 3, 4, 9, 10,
11 | dibval2 40015 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π
βπΉ) β π΅ β§ (π
βπΉ)(leβπΎ)π)) β (πΌβ(π
βπΉ)) = ((((DIsoAβπΎ)βπ)β(π
βπΉ)) Γ {π})) |
13 | 1, 6, 8, 12 | syl12anc 836 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΌβ(π
βπΉ)) = ((((DIsoAβπΎ)βπ)β(π
βπΉ)) Γ {π})) |
14 | | relxp 5695 |
. . . 4
β’ Rel
((((DIsoAβπΎ)βπ)β(π
βπΉ)) Γ {π}) |
15 | | opelxp 5713 |
. . . . 5
β’
(β¨π, π‘β© β
((((DIsoAβπΎ)βπ)β(π
βπΉ)) Γ {π}) β (π β (((DIsoAβπΎ)βπ)β(π
βπΉ)) β§ π‘ β {π})) |
16 | | dib1dim.e |
. . . . . . . . 9
β’ πΈ = ((TEndoβπΎ)βπ) |
17 | 3, 4, 5, 16, 10 | dia1dim 39932 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (((DIsoAβπΎ)βπ)β(π
βπΉ)) = {π β£ βπ β πΈ π = (π βπΉ)}) |
18 | 17 | eqabrd 2877 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π β (((DIsoAβπΎ)βπ)β(π
βπΉ)) β βπ β πΈ π = (π βπΉ))) |
19 | 18 | anbi1d 631 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π β (((DIsoAβπΎ)βπ)β(π
βπΉ)) β§ π‘ β {π}) β (βπ β πΈ π = (π βπΉ) β§ π‘ β {π}))) |
20 | 3, 4, 16 | tendocl 39638 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π βπΉ) β π) |
21 | 20 | 3expa 1119 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ) β§ πΉ β π) β (π βπΉ) β π) |
22 | 21 | an32s 651 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β (π βπΉ) β π) |
23 | 2, 3, 4, 16, 9 | tendo0cl 39661 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π») β π β πΈ) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β π β πΈ) |
25 | 22, 24 | jca 513 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β ((π βπΉ) β π β§ π β πΈ)) |
26 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = (π βπΉ) β (π β π β (π βπΉ) β π)) |
27 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π‘ = π β (π‘ β πΈ β π β πΈ)) |
28 | 26, 27 | bi2anan9 638 |
. . . . . . . . . 10
β’ ((π = (π βπΉ) β§ π‘ = π) β ((π β π β§ π‘ β πΈ) β ((π βπΉ) β π β§ π β πΈ))) |
29 | 25, 28 | syl5ibrcom 246 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β ((π = (π βπΉ) β§ π‘ = π) β (π β π β§ π‘ β πΈ))) |
30 | 29 | rexlimdva 3156 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β πΈ (π = (π βπΉ) β§ π‘ = π) β (π β π β§ π‘ β πΈ))) |
31 | 30 | pm4.71rd 564 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β πΈ (π = (π βπΉ) β§ π‘ = π) β ((π β π β§ π‘ β πΈ) β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π)))) |
32 | | velsn 4645 |
. . . . . . . . 9
β’ (π‘ β {π} β π‘ = π) |
33 | 32 | anbi2i 624 |
. . . . . . . 8
β’
((βπ β
πΈ π = (π βπΉ) β§ π‘ β {π}) β (βπ β πΈ π = (π βπΉ) β§ π‘ = π)) |
34 | | r19.41v 3189 |
. . . . . . . 8
β’
(βπ β
πΈ (π = (π βπΉ) β§ π‘ = π) β (βπ β πΈ π = (π βπΉ) β§ π‘ = π)) |
35 | 33, 34 | bitr4i 278 |
. . . . . . 7
β’
((βπ β
πΈ π = (π βπΉ) β§ π‘ β {π}) β βπ β πΈ (π = (π βπΉ) β§ π‘ = π)) |
36 | | df-3an 1090 |
. . . . . . 7
β’ ((π β π β§ π‘ β πΈ β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π)) β ((π β π β§ π‘ β πΈ) β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π))) |
37 | 31, 35, 36 | 3bitr4g 314 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((βπ β πΈ π = (π βπΉ) β§ π‘ β {π}) β (π β π β§ π‘ β πΈ β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π)))) |
38 | 19, 37 | bitrd 279 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π β (((DIsoAβπΎ)βπ)β(π
βπΉ)) β§ π‘ β {π}) β (π β π β§ π‘ β πΈ β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π)))) |
39 | 15, 38 | bitrid 283 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (β¨π, π‘β© β ((((DIsoAβπΎ)βπ)β(π
βπΉ)) Γ {π}) β (π β π β§ π‘ β πΈ β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π)))) |
40 | 14, 39 | opabbi2dv 5850 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((((DIsoAβπΎ)βπ)β(π
βπΉ)) Γ {π}) = {β¨π, π‘β© β£ (π β π β§ π‘ β πΈ β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π))}) |
41 | 13, 40 | eqtrd 2773 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΌβ(π
βπΉ)) = {β¨π, π‘β© β£ (π β π β§ π‘ β πΈ β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π))}) |
42 | | eqeq1 2737 |
. . . . 5
β’ (π = β¨π, π‘β© β (π = β¨(π βπΉ), πβ© β β¨π, π‘β© = β¨(π βπΉ), πβ©)) |
43 | | vex 3479 |
. . . . . 6
β’ π β V |
44 | | vex 3479 |
. . . . . 6
β’ π‘ β V |
45 | 43, 44 | opth 5477 |
. . . . 5
β’
(β¨π, π‘β© = β¨(π βπΉ), πβ© β (π = (π βπΉ) β§ π‘ = π)) |
46 | 42, 45 | bitrdi 287 |
. . . 4
β’ (π = β¨π, π‘β© β (π = β¨(π βπΉ), πβ© β (π = (π βπΉ) β§ π‘ = π))) |
47 | 46 | rexbidv 3179 |
. . 3
β’ (π = β¨π, π‘β© β (βπ β πΈ π = β¨(π βπΉ), πβ© β βπ β πΈ (π = (π βπΉ) β§ π‘ = π))) |
48 | 47 | rabxp 5725 |
. 2
β’ {π β (π Γ πΈ) β£ βπ β πΈ π = β¨(π βπΉ), πβ©} = {β¨π, π‘β© β£ (π β π β§ π‘ β πΈ β§ βπ β πΈ (π = (π βπΉ) β§ π‘ = π))} |
49 | 41, 48 | eqtr4di 2791 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΌβ(π
βπΉ)) = {π β (π Γ πΈ) β£ βπ β πΈ π = β¨(π βπΉ), πβ©}) |