Step | Hyp | Ref
| Expression |
1 | | dvdivf.s |
. . 3
β’ (π β π β {β, β}) |
2 | | dvdivf.f |
. . . 4
β’ (π β πΉ:πβΆβ) |
3 | 2 | ffvelcdmda 7039 |
. . 3
β’ ((π β§ π₯ β π) β (πΉβπ₯) β β) |
4 | | dvfg 25293 |
. . . . . 6
β’ (π β {β, β}
β (π D πΉ):dom (π D πΉ)βΆβ) |
5 | 1, 4 | syl 17 |
. . . . 5
β’ (π β (π D πΉ):dom (π D πΉ)βΆβ) |
6 | | dvdivf.fdv |
. . . . . 6
β’ (π β dom (π D πΉ) = π) |
7 | 6 | feq2d 6658 |
. . . . 5
β’ (π β ((π D πΉ):dom (π D πΉ)βΆβ β (π D πΉ):πβΆβ)) |
8 | 5, 7 | mpbid 231 |
. . . 4
β’ (π β (π D πΉ):πβΆβ) |
9 | 8 | ffvelcdmda 7039 |
. . 3
β’ ((π β§ π₯ β π) β ((π D πΉ)βπ₯) β β) |
10 | 2 | feqmptd 6914 |
. . . . 5
β’ (π β πΉ = (π₯ β π β¦ (πΉβπ₯))) |
11 | 10 | oveq2d 7377 |
. . . 4
β’ (π β (π D πΉ) = (π D (π₯ β π β¦ (πΉβπ₯)))) |
12 | 8 | feqmptd 6914 |
. . . 4
β’ (π β (π D πΉ) = (π₯ β π β¦ ((π D πΉ)βπ₯))) |
13 | 11, 12 | eqtr3d 2775 |
. . 3
β’ (π β (π D (π₯ β π β¦ (πΉβπ₯))) = (π₯ β π β¦ ((π D πΉ)βπ₯))) |
14 | | dvdivf.g |
. . . 4
β’ (π β πΊ:πβΆ(β β
{0})) |
15 | 14 | ffvelcdmda 7039 |
. . 3
β’ ((π β§ π₯ β π) β (πΊβπ₯) β (β β
{0})) |
16 | | dvfg 25293 |
. . . . . 6
β’ (π β {β, β}
β (π D πΊ):dom (π D πΊ)βΆβ) |
17 | 1, 16 | syl 17 |
. . . . 5
β’ (π β (π D πΊ):dom (π D πΊ)βΆβ) |
18 | | dvdivf.gdv |
. . . . . 6
β’ (π β dom (π D πΊ) = π) |
19 | 18 | feq2d 6658 |
. . . . 5
β’ (π β ((π D πΊ):dom (π D πΊ)βΆβ β (π D πΊ):πβΆβ)) |
20 | 17, 19 | mpbid 231 |
. . . 4
β’ (π β (π D πΊ):πβΆβ) |
21 | 20 | ffvelcdmda 7039 |
. . 3
β’ ((π β§ π₯ β π) β ((π D πΊ)βπ₯) β β) |
22 | 14 | feqmptd 6914 |
. . . . 5
β’ (π β πΊ = (π₯ β π β¦ (πΊβπ₯))) |
23 | 22 | oveq2d 7377 |
. . . 4
β’ (π β (π D πΊ) = (π D (π₯ β π β¦ (πΊβπ₯)))) |
24 | 20 | feqmptd 6914 |
. . . 4
β’ (π β (π D πΊ) = (π₯ β π β¦ ((π D πΊ)βπ₯))) |
25 | 23, 24 | eqtr3d 2775 |
. . 3
β’ (π β (π D (π₯ β π β¦ (πΊβπ₯))) = (π₯ β π β¦ ((π D πΊ)βπ₯))) |
26 | 1, 3, 9, 13, 15, 21, 25 | dvmptdiv 25361 |
. 2
β’ (π β (π D (π₯ β π β¦ ((πΉβπ₯) / (πΊβπ₯)))) = (π₯ β π β¦ (((((π D πΉ)βπ₯) Β· (πΊβπ₯)) β (((π D πΊ)βπ₯) Β· (πΉβπ₯))) / ((πΊβπ₯)β2)))) |
27 | | ovex 7394 |
. . . . . 6
β’ (π D πΉ) β V |
28 | 27 | dmex 7852 |
. . . . 5
β’ dom
(π D πΉ) β V |
29 | 6, 28 | eqeltrrdi 2843 |
. . . 4
β’ (π β π β V) |
30 | 29, 3, 15, 10, 22 | offval2 7641 |
. . 3
β’ (π β (πΉ βf / πΊ) = (π₯ β π β¦ ((πΉβπ₯) / (πΊβπ₯)))) |
31 | 30 | oveq2d 7377 |
. 2
β’ (π β (π D (πΉ βf / πΊ)) = (π D (π₯ β π β¦ ((πΉβπ₯) / (πΊβπ₯))))) |
32 | | ovexd 7396 |
. . 3
β’ ((π β§ π₯ β π) β ((((π D πΉ)βπ₯) Β· (πΊβπ₯)) β (((π D πΊ)βπ₯) Β· (πΉβπ₯))) β V) |
33 | 15 | eldifad 3926 |
. . . 4
β’ ((π β§ π₯ β π) β (πΊβπ₯) β β) |
34 | 33 | sqcld 14058 |
. . 3
β’ ((π β§ π₯ β π) β ((πΊβπ₯)β2) β β) |
35 | 9, 33 | mulcld 11183 |
. . . 4
β’ ((π β§ π₯ β π) β (((π D πΉ)βπ₯) Β· (πΊβπ₯)) β β) |
36 | 21, 3 | mulcld 11183 |
. . . 4
β’ ((π β§ π₯ β π) β (((π D πΊ)βπ₯) Β· (πΉβπ₯)) β β) |
37 | 29, 9, 33, 12, 22 | offval2 7641 |
. . . 4
β’ (π β ((π D πΉ) βf Β· πΊ) = (π₯ β π β¦ (((π D πΉ)βπ₯) Β· (πΊβπ₯)))) |
38 | 29, 21, 3, 24, 10 | offval2 7641 |
. . . 4
β’ (π β ((π D πΊ) βf Β· πΉ) = (π₯ β π β¦ (((π D πΊ)βπ₯) Β· (πΉβπ₯)))) |
39 | 29, 35, 36, 37, 38 | offval2 7641 |
. . 3
β’ (π β (((π D πΉ) βf Β· πΊ) βf β
((π D πΊ) βf Β· πΉ)) = (π₯ β π β¦ ((((π D πΉ)βπ₯) Β· (πΊβπ₯)) β (((π D πΊ)βπ₯) Β· (πΉβπ₯))))) |
40 | 29, 15, 15, 22, 22 | offval2 7641 |
. . . 4
β’ (π β (πΊ βf Β· πΊ) = (π₯ β π β¦ ((πΊβπ₯) Β· (πΊβπ₯)))) |
41 | 33 | sqvald 14057 |
. . . . 5
β’ ((π β§ π₯ β π) β ((πΊβπ₯)β2) = ((πΊβπ₯) Β· (πΊβπ₯))) |
42 | 41 | mpteq2dva 5209 |
. . . 4
β’ (π β (π₯ β π β¦ ((πΊβπ₯)β2)) = (π₯ β π β¦ ((πΊβπ₯) Β· (πΊβπ₯)))) |
43 | 40, 42 | eqtr4d 2776 |
. . 3
β’ (π β (πΊ βf Β· πΊ) = (π₯ β π β¦ ((πΊβπ₯)β2))) |
44 | 29, 32, 34, 39, 43 | offval2 7641 |
. 2
β’ (π β ((((π D πΉ) βf Β· πΊ) βf β
((π D πΊ) βf Β· πΉ)) βf / (πΊ βf Β·
πΊ)) = (π₯ β π β¦ (((((π D πΉ)βπ₯) Β· (πΊβπ₯)) β (((π D πΊ)βπ₯) Β· (πΉβπ₯))) / ((πΊβπ₯)β2)))) |
45 | 26, 31, 44 | 3eqtr4d 2783 |
1
β’ (π β (π D (πΉ βf / πΊ)) = ((((π D πΉ) βf Β· πΊ) βf β
((π D πΊ) βf Β· πΉ)) βf / (πΊ βf Β·
πΊ))) |