Step | Hyp | Ref
| Expression |
1 | | dvaddf.f |
. . . . 5
β’ (π β πΉ:πβΆβ) |
2 | 1 | adantr 480 |
. . . 4
β’ ((π β§ π₯ β π) β πΉ:πβΆβ) |
3 | | dvaddf.df |
. . . . . 6
β’ (π β dom (π D πΉ) = π) |
4 | | dvbsss 25782 |
. . . . . 6
β’ dom
(π D πΉ) β π |
5 | 3, 4 | eqsstrrdi 4032 |
. . . . 5
β’ (π β π β π) |
6 | 5 | adantr 480 |
. . . 4
β’ ((π β§ π₯ β π) β π β π) |
7 | | dvaddf.g |
. . . . 5
β’ (π β πΊ:πβΆβ) |
8 | 7 | adantr 480 |
. . . 4
β’ ((π β§ π₯ β π) β πΊ:πβΆβ) |
9 | | dvaddf.s |
. . . . 5
β’ (π β π β {β, β}) |
10 | 9 | adantr 480 |
. . . 4
β’ ((π β§ π₯ β π) β π β {β, β}) |
11 | 3 | eleq2d 2813 |
. . . . 5
β’ (π β (π₯ β dom (π D πΉ) β π₯ β π)) |
12 | 11 | biimpar 477 |
. . . 4
β’ ((π β§ π₯ β π) β π₯ β dom (π D πΉ)) |
13 | | dvaddf.dg |
. . . . . 6
β’ (π β dom (π D πΊ) = π) |
14 | 13 | eleq2d 2813 |
. . . . 5
β’ (π β (π₯ β dom (π D πΊ) β π₯ β π)) |
15 | 14 | biimpar 477 |
. . . 4
β’ ((π β§ π₯ β π) β π₯ β dom (π D πΊ)) |
16 | 2, 6, 8, 6, 10, 12, 15 | dvmul 25823 |
. . 3
β’ ((π β§ π₯ β π) β ((π D (πΉ βf Β· πΊ))βπ₯) = ((((π D πΉ)βπ₯) Β· (πΊβπ₯)) + (((π D πΊ)βπ₯) Β· (πΉβπ₯)))) |
17 | 16 | mpteq2dva 5241 |
. 2
β’ (π β (π₯ β π β¦ ((π D (πΉ βf Β· πΊ))βπ₯)) = (π₯ β π β¦ ((((π D πΉ)βπ₯) Β· (πΊβπ₯)) + (((π D πΊ)βπ₯) Β· (πΉβπ₯))))) |
18 | | dvfg 25786 |
. . . . 5
β’ (π β {β, β}
β (π D (πΉ βf Β·
πΊ)):dom (π D (πΉ βf Β· πΊ))βΆβ) |
19 | 9, 18 | syl 17 |
. . . 4
β’ (π β (π D (πΉ βf Β· πΊ)):dom (π D (πΉ βf Β· πΊ))βΆβ) |
20 | | recnprss 25784 |
. . . . . . . 8
β’ (π β {β, β}
β π β
β) |
21 | 9, 20 | syl 17 |
. . . . . . 7
β’ (π β π β β) |
22 | | mulcl 11193 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
23 | 22 | adantl 481 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
24 | 9, 5 | ssexd 5317 |
. . . . . . . 8
β’ (π β π β V) |
25 | | inidm 4213 |
. . . . . . . 8
β’ (π β© π) = π |
26 | 23, 1, 7, 24, 24, 25 | off 7684 |
. . . . . . 7
β’ (π β (πΉ βf Β· πΊ):πβΆβ) |
27 | 21, 26, 5 | dvbss 25781 |
. . . . . 6
β’ (π β dom (π D (πΉ βf Β· πΊ)) β π) |
28 | 21 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π β β) |
29 | | dvfg 25786 |
. . . . . . . . . . . 12
β’ (π β {β, β}
β (π D πΉ):dom (π D πΉ)βΆβ) |
30 | 9, 29 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π D πΉ):dom (π D πΉ)βΆβ) |
31 | 30 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (π D πΉ):dom (π D πΉ)βΆβ) |
32 | | ffun 6713 |
. . . . . . . . . 10
β’ ((π D πΉ):dom (π D πΉ)βΆβ β Fun (π D πΉ)) |
33 | | funfvbrb 7045 |
. . . . . . . . . 10
β’ (Fun
(π D πΉ) β (π₯ β dom (π D πΉ) β π₯(π D πΉ)((π D πΉ)βπ₯))) |
34 | 31, 32, 33 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (π₯ β dom (π D πΉ) β π₯(π D πΉ)((π D πΉ)βπ₯))) |
35 | 12, 34 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π₯(π D πΉ)((π D πΉ)βπ₯)) |
36 | | dvfg 25786 |
. . . . . . . . . . . 12
β’ (π β {β, β}
β (π D πΊ):dom (π D πΊ)βΆβ) |
37 | 9, 36 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π D πΊ):dom (π D πΊ)βΆβ) |
38 | 37 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (π D πΊ):dom (π D πΊ)βΆβ) |
39 | | ffun 6713 |
. . . . . . . . . 10
β’ ((π D πΊ):dom (π D πΊ)βΆβ β Fun (π D πΊ)) |
40 | | funfvbrb 7045 |
. . . . . . . . . 10
β’ (Fun
(π D πΊ) β (π₯ β dom (π D πΊ) β π₯(π D πΊ)((π D πΊ)βπ₯))) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (π₯ β dom (π D πΊ) β π₯(π D πΊ)((π D πΊ)βπ₯))) |
42 | 15, 41 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β π₯(π D πΊ)((π D πΊ)βπ₯)) |
43 | | eqid 2726 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
44 | 2, 6, 8, 6, 28, 35, 42, 43 | dvmulbr 25820 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π₯(π D (πΉ βf Β· πΊ))((((π D πΉ)βπ₯) Β· (πΊβπ₯)) + (((π D πΊ)βπ₯) Β· (πΉβπ₯)))) |
45 | | reldv 25750 |
. . . . . . . 8
β’ Rel
(π D (πΉ βf Β· πΊ)) |
46 | 45 | releldmi 5940 |
. . . . . . 7
β’ (π₯(π D (πΉ βf Β· πΊ))((((π D πΉ)βπ₯) Β· (πΊβπ₯)) + (((π D πΊ)βπ₯) Β· (πΉβπ₯))) β π₯ β dom (π D (πΉ βf Β· πΊ))) |
47 | 44, 46 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β π) β π₯ β dom (π D (πΉ βf Β· πΊ))) |
48 | 27, 47 | eqelssd 3998 |
. . . . 5
β’ (π β dom (π D (πΉ βf Β· πΊ)) = π) |
49 | 48 | feq2d 6696 |
. . . 4
β’ (π β ((π D (πΉ βf Β· πΊ)):dom (π D (πΉ βf Β· πΊ))βΆβ β (π D (πΉ βf Β· πΊ)):πβΆβ)) |
50 | 19, 49 | mpbid 231 |
. . 3
β’ (π β (π D (πΉ βf Β· πΊ)):πβΆβ) |
51 | 50 | feqmptd 6953 |
. 2
β’ (π β (π D (πΉ βf Β· πΊ)) = (π₯ β π β¦ ((π D (πΉ βf Β· πΊ))βπ₯))) |
52 | | ovexd 7439 |
. . 3
β’ ((π β§ π₯ β π) β (((π D πΉ)βπ₯) Β· (πΊβπ₯)) β V) |
53 | | ovexd 7439 |
. . 3
β’ ((π β§ π₯ β π) β (((π D πΊ)βπ₯) Β· (πΉβπ₯)) β V) |
54 | | fvexd 6899 |
. . . 4
β’ ((π β§ π₯ β π) β ((π D πΉ)βπ₯) β V) |
55 | | fvexd 6899 |
. . . 4
β’ ((π β§ π₯ β π) β (πΊβπ₯) β V) |
56 | 3 | feq2d 6696 |
. . . . . 6
β’ (π β ((π D πΉ):dom (π D πΉ)βΆβ β (π D πΉ):πβΆβ)) |
57 | 30, 56 | mpbid 231 |
. . . . 5
β’ (π β (π D πΉ):πβΆβ) |
58 | 57 | feqmptd 6953 |
. . . 4
β’ (π β (π D πΉ) = (π₯ β π β¦ ((π D πΉ)βπ₯))) |
59 | 7 | feqmptd 6953 |
. . . 4
β’ (π β πΊ = (π₯ β π β¦ (πΊβπ₯))) |
60 | 24, 54, 55, 58, 59 | offval2 7686 |
. . 3
β’ (π β ((π D πΉ) βf Β· πΊ) = (π₯ β π β¦ (((π D πΉ)βπ₯) Β· (πΊβπ₯)))) |
61 | | fvexd 6899 |
. . . 4
β’ ((π β§ π₯ β π) β ((π D πΊ)βπ₯) β V) |
62 | | fvexd 6899 |
. . . 4
β’ ((π β§ π₯ β π) β (πΉβπ₯) β V) |
63 | 13 | feq2d 6696 |
. . . . . 6
β’ (π β ((π D πΊ):dom (π D πΊ)βΆβ β (π D πΊ):πβΆβ)) |
64 | 37, 63 | mpbid 231 |
. . . . 5
β’ (π β (π D πΊ):πβΆβ) |
65 | 64 | feqmptd 6953 |
. . . 4
β’ (π β (π D πΊ) = (π₯ β π β¦ ((π D πΊ)βπ₯))) |
66 | 1 | feqmptd 6953 |
. . . 4
β’ (π β πΉ = (π₯ β π β¦ (πΉβπ₯))) |
67 | 24, 61, 62, 65, 66 | offval2 7686 |
. . 3
β’ (π β ((π D πΊ) βf Β· πΉ) = (π₯ β π β¦ (((π D πΊ)βπ₯) Β· (πΉβπ₯)))) |
68 | 24, 52, 53, 60, 67 | offval2 7686 |
. 2
β’ (π β (((π D πΉ) βf Β· πΊ) βf + ((π D πΊ) βf Β· πΉ)) = (π₯ β π β¦ ((((π D πΉ)βπ₯) Β· (πΊβπ₯)) + (((π D πΊ)βπ₯) Β· (πΉβπ₯))))) |
69 | 17, 51, 68 | 3eqtr4d 2776 |
1
β’ (π β (π D (πΉ βf Β· πΊ)) = (((π D πΉ) βf Β· πΊ) βf + ((π D πΊ) βf Β· πΉ))) |