| Step | Hyp | Ref
| Expression |
|---|
| 1 | | dvcof.f |
. . . . 5
β’ (π β πΉ:πβΆβ) |
| 2 | 1 | adantr 479 |
. . . 4
β’ ((π β§ π₯ β π) β πΉ:πβΆβ) |
| 3 | | dvcof.df |
. . . . . 6
β’ (π β dom (π D πΉ) = π) |
| 4 | | dvbsss 25653 |
. . . . . 6
β’ dom
(π D πΉ) β π |
| 5 | 3, 4 | eqsstrrdi 4038 |
. . . . 5
β’ (π β π β π) |
| 6 | 5 | adantr 479 |
. . . 4
β’ ((π β§ π₯ β π) β π β π) |
| 7 | | dvcof.g |
. . . . 5
β’ (π β πΊ:πβΆπ) |
| 8 | 7 | adantr 479 |
. . . 4
β’ ((π β§ π₯ β π) β πΊ:πβΆπ) |
| 9 | | dvcof.dg |
. . . . . 6
β’ (π β dom (π D πΊ) = π) |
| 10 | | dvbsss 25653 |
. . . . . 6
β’ dom
(π D πΊ) β π |
| 11 | 9, 10 | eqsstrrdi 4038 |
. . . . 5
β’ (π β π β π) |
| 12 | 11 | adantr 479 |
. . . 4
β’ ((π β§ π₯ β π) β π β π) |
| 13 | | dvcof.s |
. . . . 5
β’ (π β π β {β, β}) |
| 14 | 13 | adantr 479 |
. . . 4
β’ ((π β§ π₯ β π) β π β {β, β}) |
| 15 | | dvcof.t |
. . . . 5
β’ (π β π β {β, β}) |
| 16 | 15 | adantr 479 |
. . . 4
β’ ((π β§ π₯ β π) β π β {β, β}) |
| 17 | 7 | ffvelcdmda 7087 |
. . . . 5
β’ ((π β§ π₯ β π) β (πΊβπ₯) β π) |
| 18 | 3 | adantr 479 |
. . . . 5
β’ ((π β§ π₯ β π) β dom (π D πΉ) = π) |
| 19 | 17, 18 | eleqtrrd 2834 |
. . . 4
β’ ((π β§ π₯ β π) β (πΊβπ₯) β dom (π D πΉ)) |
| 20 | 9 | eleq2d 2817 |
. . . . 5
β’ (π β (π₯ β dom (π D πΊ) β π₯ β π)) |
| 21 | 20 | biimpar 476 |
. . . 4
β’ ((π β§ π₯ β π) β π₯ β dom (π D πΊ)) |
| 22 | 2, 6, 8, 12, 14, 16, 19, 21 | dvco 25698 |
. . 3
β’ ((π β§ π₯ β π) β ((π D (πΉ β πΊ))βπ₯) = (((π D πΉ)β(πΊβπ₯)) Β· ((π D πΊ)βπ₯))) |
| 23 | 22 | mpteq2dva 5249 |
. 2
β’ (π β (π₯ β π β¦ ((π D (πΉ β πΊ))βπ₯)) = (π₯ β π β¦ (((π D πΉ)β(πΊβπ₯)) Β· ((π D πΊ)βπ₯)))) |
| 24 | | dvfg 25657 |
. . . . 5
β’ (π β {β, β}
β (π D (πΉ β πΊ)):dom (π D (πΉ β πΊ))βΆβ) |
| 25 | 15, 24 | syl 17 |
. . . 4
β’ (π β (π D (πΉ β πΊ)):dom (π D (πΉ β πΊ))βΆβ) |
| 26 | | recnprss 25655 |
. . . . . . . 8
β’ (π β {β, β}
β π β
β) |
| 27 | 15, 26 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
| 28 | | fco 6742 |
. . . . . . . 8
β’ ((πΉ:πβΆβ β§ πΊ:πβΆπ) β (πΉ β πΊ):πβΆβ) |
| 29 | 1, 7, 28 | syl2anc 582 |
. . . . . . 7
β’ (π β (πΉ β πΊ):πβΆβ) |
| 30 | 27, 29, 11 | dvbss 25652 |
. . . . . 6
β’ (π β dom (π D (πΉ β πΊ)) β π) |
| 31 | | recnprss 25655 |
. . . . . . . . 9
β’ (π β {β, β}
β π β
β) |
| 32 | 14, 31 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π β β) |
| 33 | 16, 26 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π β β) |
| 34 | | fvexd 6907 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((π D πΉ)β(πΊβπ₯)) β V) |
| 35 | | fvexd 6907 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((π D πΊ)βπ₯) β V) |
| 36 | | dvfg 25657 |
. . . . . . . . . 10
β’ (π β {β, β}
β (π D πΉ):dom (π D πΉ)βΆβ) |
| 37 | | ffun 6721 |
. . . . . . . . . 10
β’ ((π D πΉ):dom (π D πΉ)βΆβ β Fun (π D πΉ)) |
| 38 | | funfvbrb 7053 |
. . . . . . . . . 10
β’ (Fun
(π D πΉ) β ((πΊβπ₯) β dom (π D πΉ) β (πΊβπ₯)(π D πΉ)((π D πΉ)β(πΊβπ₯)))) |
| 39 | 14, 36, 37, 38 | 4syl 19 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β ((πΊβπ₯) β dom (π D πΉ) β (πΊβπ₯)(π D πΉ)((π D πΉ)β(πΊβπ₯)))) |
| 40 | 19, 39 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (πΊβπ₯)(π D πΉ)((π D πΉ)β(πΊβπ₯))) |
| 41 | | dvfg 25657 |
. . . . . . . . . 10
β’ (π β {β, β}
β (π D πΊ):dom (π D πΊ)βΆβ) |
| 42 | | ffun 6721 |
. . . . . . . . . 10
β’ ((π D πΊ):dom (π D πΊ)βΆβ β Fun (π D πΊ)) |
| 43 | | funfvbrb 7053 |
. . . . . . . . . 10
β’ (Fun
(π D πΊ) β (π₯ β dom (π D πΊ) β π₯(π D πΊ)((π D πΊ)βπ₯))) |
| 44 | 16, 41, 42, 43 | 4syl 19 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (π₯ β dom (π D πΊ) β π₯(π D πΊ)((π D πΊ)βπ₯))) |
| 45 | 21, 44 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π₯(π D πΊ)((π D πΊ)βπ₯)) |
| 46 | | eqid 2730 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
| 47 | 2, 6, 8, 12, 32, 33, 34, 35, 40, 45, 46 | dvcobr 25697 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π₯(π D (πΉ β πΊ))(((π D πΉ)β(πΊβπ₯)) Β· ((π D πΊ)βπ₯))) |
| 48 | | reldv 25621 |
. . . . . . . 8
β’ Rel
(π D (πΉ β πΊ)) |
| 49 | 48 | releldmi 5948 |
. . . . . . 7
β’ (π₯(π D (πΉ β πΊ))(((π D πΉ)β(πΊβπ₯)) Β· ((π D πΊ)βπ₯)) β π₯ β dom (π D (πΉ β πΊ))) |
| 50 | 47, 49 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β π) β π₯ β dom (π D (πΉ β πΊ))) |
| 51 | 30, 50 | eqelssd 4004 |
. . . . 5
β’ (π β dom (π D (πΉ β πΊ)) = π) |
| 52 | 51 | feq2d 6704 |
. . . 4
β’ (π β ((π D (πΉ β πΊ)):dom (π D (πΉ β πΊ))βΆβ β (π D (πΉ β πΊ)):πβΆβ)) |
| 53 | 25, 52 | mpbid 231 |
. . 3
β’ (π β (π D (πΉ β πΊ)):πβΆβ) |
| 54 | 53 | feqmptd 6961 |
. 2
β’ (π β (π D (πΉ β πΊ)) = (π₯ β π β¦ ((π D (πΉ β πΊ))βπ₯))) |
| 55 | 15, 11 | ssexd 5325 |
. . 3
β’ (π β π β V) |
| 56 | 7 | feqmptd 6961 |
. . . 4
β’ (π β πΊ = (π₯ β π β¦ (πΊβπ₯))) |
| 57 | 13, 36 | syl 17 |
. . . . . 6
β’ (π β (π D πΉ):dom (π D πΉ)βΆβ) |
| 58 | 3 | feq2d 6704 |
. . . . . 6
β’ (π β ((π D πΉ):dom (π D πΉ)βΆβ β (π D πΉ):πβΆβ)) |
| 59 | 57, 58 | mpbid 231 |
. . . . 5
β’ (π β (π D πΉ):πβΆβ) |
| 60 | 59 | feqmptd 6961 |
. . . 4
β’ (π β (π D πΉ) = (π¦ β π β¦ ((π D πΉ)βπ¦))) |
| 61 | | fveq2 6892 |
. . . 4
β’ (π¦ = (πΊβπ₯) β ((π D πΉ)βπ¦) = ((π D πΉ)β(πΊβπ₯))) |
| 62 | 17, 56, 60, 61 | fmptco 7130 |
. . 3
β’ (π β ((π D πΉ) β πΊ) = (π₯ β π β¦ ((π D πΉ)β(πΊβπ₯)))) |
| 63 | 15, 41 | syl 17 |
. . . . 5
β’ (π β (π D πΊ):dom (π D πΊ)βΆβ) |
| 64 | 9 | feq2d 6704 |
. . . . 5
β’ (π β ((π D πΊ):dom (π D πΊ)βΆβ β (π D πΊ):πβΆβ)) |
| 65 | 63, 64 | mpbid 231 |
. . . 4
β’ (π β (π D πΊ):πβΆβ) |
| 66 | 65 | feqmptd 6961 |
. . 3
β’ (π β (π D πΊ) = (π₯ β π β¦ ((π D πΊ)βπ₯))) |
| 67 | 55, 34, 35, 62, 66 | offval2 7694 |
. 2
β’ (π β (((π D πΉ) β πΊ) βf Β· (π D πΊ)) = (π₯ β π β¦ (((π D πΉ)β(πΊβπ₯)) Β· ((π D πΊ)βπ₯)))) |
| 68 | 23, 54, 67 | 3eqtr4d 2780 |
1
β’ (π β (π D (πΉ β πΊ)) = (((π D πΉ) β πΊ) βf Β· (π D πΊ))) |
