Step | Hyp | Ref
| Expression |
1 | | mbfmulc2.3 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |
2 | | mbfmulc2.2 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π΅ β π) |
3 | 1, 2 | mbfdm2 25017 |
. . . . 5
β’ (π β π΄ β dom vol) |
4 | | mbfmulc2.1 |
. . . . . . . . 9
β’ (π β πΆ β β) |
5 | 4 | recld 15086 |
. . . . . . . 8
β’ (π β (ββπΆ) β
β) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (ββπΆ) β β) |
7 | 6 | recnd 11190 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββπΆ) β β) |
8 | 1, 2 | mbfmptcl 25016 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β π΅ β β) |
9 | 8 | recld 15086 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
10 | 9 | recnd 11190 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
11 | 7, 10 | mulcld 11182 |
. . . . 5
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β β) |
12 | | ovexd 7397 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (-(ββπΆ) Β· (ββπ΅)) β V) |
13 | | fconstmpt 5699 |
. . . . . . 7
β’ (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ)) |
14 | 13 | a1i 11 |
. . . . . 6
β’ (π β (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ))) |
15 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) = (π₯ β π΄ β¦ (ββπ΅))) |
16 | 3, 6, 9, 14, 15 | offval2 7642 |
. . . . 5
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅)))) |
17 | 4 | imcld 15087 |
. . . . . . . 8
β’ (π β (ββπΆ) β
β) |
18 | 17 | renegcld 11589 |
. . . . . . 7
β’ (π β -(ββπΆ) β
β) |
19 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β -(ββπΆ) β β) |
20 | 8 | imcld 15087 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
21 | | fconstmpt 5699 |
. . . . . . 7
β’ (π΄ Γ {-(ββπΆ)}) = (π₯ β π΄ β¦ -(ββπΆ)) |
22 | 21 | a1i 11 |
. . . . . 6
β’ (π β (π΄ Γ {-(ββπΆ)}) = (π₯ β π΄ β¦ -(ββπΆ))) |
23 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) = (π₯ β π΄ β¦ (ββπ΅))) |
24 | 3, 19, 20, 22, 23 | offval2 7642 |
. . . . 5
β’ (π β ((π΄ Γ {-(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ (-(ββπΆ) Β· (ββπ΅)))) |
25 | 3, 11, 12, 16, 24 | offval2 7642 |
. . . 4
β’ (π β (((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) βf + ((π΄ Γ {-(ββπΆ)}) βf Β·
(π₯ β π΄ β¦ (ββπ΅)))) = (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) + (-(ββπΆ) Β· (ββπ΅))))) |
26 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (ββπΆ) β β) |
27 | 26 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (ββπΆ) β β) |
28 | 20 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (ββπ΅) β β) |
29 | 27, 28 | mulcld 11182 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β β) |
30 | 11, 29 | negsubd 11525 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (((ββπΆ) Β· (ββπ΅)) + -((ββπΆ) Β· (ββπ΅))) = (((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅)))) |
31 | 27, 28 | mulneg1d 11615 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (-(ββπΆ) Β· (ββπ΅)) = -((ββπΆ) Β· (ββπ΅))) |
32 | 31 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (((ββπΆ) Β· (ββπ΅)) + (-(ββπΆ) Β· (ββπ΅))) = (((ββπΆ) Β· (ββπ΅)) + -((ββπΆ) Β· (ββπ΅)))) |
33 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β πΆ β β) |
34 | 33, 8 | remuld 15110 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (ββ(πΆ Β· π΅)) = (((ββπΆ) Β· (ββπ΅)) β ((ββπΆ) Β· (ββπ΅)))) |
35 | 30, 32, 34 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (((ββπΆ) Β· (ββπ΅)) + (-(ββπΆ) Β· (ββπ΅))) = (ββ(πΆ Β· π΅))) |
36 | 35 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) + (-(ββπΆ) Β· (ββπ΅)))) = (π₯ β π΄ β¦ (ββ(πΆ Β· π΅)))) |
37 | 25, 36 | eqtrd 2777 |
. . 3
β’ (π β (((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) βf + ((π΄ Γ {-(ββπΆ)}) βf Β·
(π₯ β π΄ β¦ (ββπ΅)))) = (π₯ β π΄ β¦ (ββ(πΆ Β· π΅)))) |
38 | 8 | ismbfcn2 25018 |
. . . . . . 7
β’ (π β ((π₯ β π΄ β¦ π΅) β MblFn β ((π₯ β π΄ β¦ (ββπ΅)) β MblFn β§ (π₯ β π΄ β¦ (ββπ΅)) β MblFn))) |
39 | 1, 38 | mpbid 231 |
. . . . . 6
β’ (π β ((π₯ β π΄ β¦ (ββπ΅)) β MblFn β§ (π₯ β π΄ β¦ (ββπ΅)) β MblFn)) |
40 | 39 | simpld 496 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
41 | 10 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββπ΅)):π΄βΆβ) |
42 | 40, 5, 41 | mbfmulc2re 25028 |
. . . 4
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
43 | 39 | simprd 497 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββπ΅)) β MblFn) |
44 | 28 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (ββπ΅)):π΄βΆβ) |
45 | 43, 18, 44 | mbfmulc2re 25028 |
. . . 4
β’ (π β ((π΄ Γ {-(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
46 | 42, 45 | mbfadd 25041 |
. . 3
β’ (π β (((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) βf + ((π΄ Γ {-(ββπΆ)}) βf Β·
(π₯ β π΄ β¦ (ββπ΅)))) β MblFn) |
47 | 37, 46 | eqeltrrd 2839 |
. 2
β’ (π β (π₯ β π΄ β¦ (ββ(πΆ Β· π΅))) β MblFn) |
48 | | ovexd 7397 |
. . . . 5
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β V) |
49 | | ovexd 7397 |
. . . . 5
β’ ((π β§ π₯ β π΄) β ((ββπΆ) Β· (ββπ΅)) β V) |
50 | 3, 6, 20, 14, 23 | offval2 7642 |
. . . . 5
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅)))) |
51 | | fconstmpt 5699 |
. . . . . . 7
β’ (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ)) |
52 | 51 | a1i 11 |
. . . . . 6
β’ (π β (π΄ Γ {(ββπΆ)}) = (π₯ β π΄ β¦ (ββπΆ))) |
53 | 3, 26, 9, 52, 15 | offval2 7642 |
. . . . 5
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) = (π₯ β π΄ β¦ ((ββπΆ) Β· (ββπ΅)))) |
54 | 3, 48, 49, 50, 53 | offval2 7642 |
. . . 4
β’ (π β (((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) βf + ((π΄ Γ {(ββπΆ)}) βf Β·
(π₯ β π΄ β¦ (ββπ΅)))) = (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅))))) |
55 | 33, 8 | immuld 15111 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (ββ(πΆ Β· π΅)) = (((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅)))) |
56 | 55 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β π΄ β¦ (ββ(πΆ Β· π΅))) = (π₯ β π΄ β¦ (((ββπΆ) Β· (ββπ΅)) + ((ββπΆ) Β· (ββπ΅))))) |
57 | 54, 56 | eqtr4d 2780 |
. . 3
β’ (π β (((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) βf + ((π΄ Γ {(ββπΆ)}) βf Β·
(π₯ β π΄ β¦ (ββπ΅)))) = (π₯ β π΄ β¦ (ββ(πΆ Β· π΅)))) |
58 | 43, 5, 44 | mbfmulc2re 25028 |
. . . 4
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
59 | 40, 17, 41 | mbfmulc2re 25028 |
. . . 4
β’ (π β ((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) β MblFn) |
60 | 58, 59 | mbfadd 25041 |
. . 3
β’ (π β (((π΄ Γ {(ββπΆ)}) βf Β· (π₯ β π΄ β¦ (ββπ΅))) βf + ((π΄ Γ {(ββπΆ)}) βf Β·
(π₯ β π΄ β¦ (ββπ΅)))) β MblFn) |
61 | 57, 60 | eqeltrrd 2839 |
. 2
β’ (π β (π₯ β π΄ β¦ (ββ(πΆ Β· π΅))) β MblFn) |
62 | 33, 8 | mulcld 11182 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΆ Β· π΅) β β) |
63 | 62 | ismbfcn2 25018 |
. 2
β’ (π β ((π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn β ((π₯ β π΄ β¦ (ββ(πΆ Β· π΅))) β MblFn β§ (π₯ β π΄ β¦ (ββ(πΆ Β· π΅))) β MblFn))) |
64 | 47, 61, 63 | mpbir2and 712 |
1
β’ (π β (π₯ β π΄ β¦ (πΆ Β· π΅)) β MblFn) |