Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . . . . . 9
β’ (π β πΉ β dom
β«1) |
2 | | i1ff 25056 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
4 | 3 | ffnd 6674 |
. . . . . . 7
β’ (π β πΉ Fn β) |
5 | | i1fadd.2 |
. . . . . . . . 9
β’ (π β πΊ β dom
β«1) |
6 | | i1ff 25056 |
. . . . . . . . 9
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
β’ (π β πΊ:ββΆβ) |
8 | 7 | ffnd 6674 |
. . . . . . 7
β’ (π β πΊ Fn β) |
9 | | reex 11149 |
. . . . . . . 8
β’ β
β V |
10 | 9 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
11 | | inidm 4183 |
. . . . . . 7
β’ (β
β© β) = β |
12 | 4, 8, 10, 10, 11 | offn 7635 |
. . . . . 6
β’ (π β (πΉ βf Β· πΊ) Fn β) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ π΄ β (β β {0})) β (πΉ βf Β·
πΊ) Fn
β) |
14 | | fniniseg 7015 |
. . . . 5
β’ ((πΉ βf Β·
πΊ) Fn β β (π§ β (β‘(πΉ βf Β· πΊ) β {π΄}) β (π§ β β β§ ((πΉ βf Β· πΊ)βπ§) = π΄))) |
15 | 13, 14 | syl 17 |
. . . 4
β’ ((π β§ π΄ β (β β {0})) β (π§ β (β‘(πΉ βf Β· πΊ) β {π΄}) β (π§ β β β§ ((πΉ βf Β· πΊ)βπ§) = π΄))) |
16 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β (β β {0})) β πΉ Fn β) |
17 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β (β β {0})) β πΊ Fn β) |
18 | 9 | a1i 11 |
. . . . . . 7
β’ ((π β§ π΄ β (β β {0})) β
β β V) |
19 | | eqidd 2738 |
. . . . . . 7
β’ (((π β§ π΄ β (β β {0})) β§ π§ β β) β (πΉβπ§) = (πΉβπ§)) |
20 | | eqidd 2738 |
. . . . . . 7
β’ (((π β§ π΄ β (β β {0})) β§ π§ β β) β (πΊβπ§) = (πΊβπ§)) |
21 | 16, 17, 18, 18, 11, 19, 20 | ofval 7633 |
. . . . . 6
β’ (((π β§ π΄ β (β β {0})) β§ π§ β β) β ((πΉ βf Β·
πΊ)βπ§) = ((πΉβπ§) Β· (πΊβπ§))) |
22 | 21 | eqeq1d 2739 |
. . . . 5
β’ (((π β§ π΄ β (β β {0})) β§ π§ β β) β (((πΉ βf Β·
πΊ)βπ§) = π΄ β ((πΉβπ§) Β· (πΊβπ§)) = π΄)) |
23 | 22 | pm5.32da 580 |
. . . 4
β’ ((π β§ π΄ β (β β {0})) β
((π§ β β β§
((πΉ βf
Β· πΊ)βπ§) = π΄) β (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄))) |
24 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β πΊ Fn β) |
25 | | simprl 770 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β π§ β β) |
26 | | fnfvelrn 7036 |
. . . . . . . . 9
β’ ((πΊ Fn β β§ π§ β β) β (πΊβπ§) β ran πΊ) |
27 | 24, 25, 26 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΊβπ§) β ran πΊ) |
28 | | eldifsni 4755 |
. . . . . . . . . . 11
β’ (π΄ β (β β {0})
β π΄ β
0) |
29 | 28 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β π΄ β 0) |
30 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β ((πΉβπ§) Β· (πΊβπ§)) = π΄) |
31 | 3 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β πΉ:ββΆβ) |
32 | 31, 25 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΉβπ§) β β) |
33 | 32 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΉβπ§) β β) |
34 | 33 | mul01d 11361 |
. . . . . . . . . 10
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β ((πΉβπ§) Β· 0) = 0) |
35 | 29, 30, 34 | 3netr4d 3022 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β ((πΉβπ§) Β· (πΊβπ§)) β ((πΉβπ§) Β· 0)) |
36 | | oveq2 7370 |
. . . . . . . . . 10
β’ ((πΊβπ§) = 0 β ((πΉβπ§) Β· (πΊβπ§)) = ((πΉβπ§) Β· 0)) |
37 | 36 | necon3i 2977 |
. . . . . . . . 9
β’ (((πΉβπ§) Β· (πΊβπ§)) β ((πΉβπ§) Β· 0) β (πΊβπ§) β 0) |
38 | 35, 37 | syl 17 |
. . . . . . . 8
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΊβπ§) β 0) |
39 | | eldifsn 4752 |
. . . . . . . 8
β’ ((πΊβπ§) β (ran πΊ β {0}) β ((πΊβπ§) β ran πΊ β§ (πΊβπ§) β 0)) |
40 | 27, 38, 39 | sylanbrc 584 |
. . . . . . 7
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΊβπ§) β (ran πΊ β {0})) |
41 | 7 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β πΊ:ββΆβ) |
42 | 41, 25 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΊβπ§) β β) |
43 | 42 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΊβπ§) β β) |
44 | 33, 43, 38 | divcan4d 11944 |
. . . . . . . . . 10
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (((πΉβπ§) Β· (πΊβπ§)) / (πΊβπ§)) = (πΉβπ§)) |
45 | 30 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (((πΉβπ§) Β· (πΊβπ§)) / (πΊβπ§)) = (π΄ / (πΊβπ§))) |
46 | 44, 45 | eqtr3d 2779 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΉβπ§) = (π΄ / (πΊβπ§))) |
47 | 31 | ffnd 6674 |
. . . . . . . . . 10
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β πΉ Fn β) |
48 | | fniniseg 7015 |
. . . . . . . . . 10
β’ (πΉ Fn β β (π§ β (β‘πΉ β {(π΄ / (πΊβπ§))}) β (π§ β β β§ (πΉβπ§) = (π΄ / (πΊβπ§))))) |
49 | 47, 48 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (π§ β (β‘πΉ β {(π΄ / (πΊβπ§))}) β (π§ β β β§ (πΉβπ§) = (π΄ / (πΊβπ§))))) |
50 | 25, 46, 49 | mpbir2and 712 |
. . . . . . . 8
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β π§ β (β‘πΉ β {(π΄ / (πΊβπ§))})) |
51 | | eqidd 2738 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (πΊβπ§) = (πΊβπ§)) |
52 | | fniniseg 7015 |
. . . . . . . . . 10
β’ (πΊ Fn β β (π§ β (β‘πΊ β {(πΊβπ§)}) β (π§ β β β§ (πΊβπ§) = (πΊβπ§)))) |
53 | 24, 52 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β (π§ β (β‘πΊ β {(πΊβπ§)}) β (π§ β β β§ (πΊβπ§) = (πΊβπ§)))) |
54 | 25, 51, 53 | mpbir2and 712 |
. . . . . . . 8
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β π§ β (β‘πΊ β {(πΊβπ§)})) |
55 | 50, 54 | elind 4159 |
. . . . . . 7
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β π§ β ((β‘πΉ β {(π΄ / (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)}))) |
56 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π¦ = (πΊβπ§) β (π΄ / π¦) = (π΄ / (πΊβπ§))) |
57 | 56 | sneqd 4603 |
. . . . . . . . . . 11
β’ (π¦ = (πΊβπ§) β {(π΄ / π¦)} = {(π΄ / (πΊβπ§))}) |
58 | 57 | imaeq2d 6018 |
. . . . . . . . . 10
β’ (π¦ = (πΊβπ§) β (β‘πΉ β {(π΄ / π¦)}) = (β‘πΉ β {(π΄ / (πΊβπ§))})) |
59 | | sneq 4601 |
. . . . . . . . . . 11
β’ (π¦ = (πΊβπ§) β {π¦} = {(πΊβπ§)}) |
60 | 59 | imaeq2d 6018 |
. . . . . . . . . 10
β’ (π¦ = (πΊβπ§) β (β‘πΊ β {π¦}) = (β‘πΊ β {(πΊβπ§)})) |
61 | 58, 60 | ineq12d 4178 |
. . . . . . . . 9
β’ (π¦ = (πΊβπ§) β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) = ((β‘πΉ β {(π΄ / (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)}))) |
62 | 61 | eleq2d 2824 |
. . . . . . . 8
β’ (π¦ = (πΊβπ§) β (π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) β π§ β ((β‘πΉ β {(π΄ / (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)})))) |
63 | 62 | rspcev 3584 |
. . . . . . 7
β’ (((πΊβπ§) β (ran πΊ β {0}) β§ π§ β ((β‘πΉ β {(π΄ / (πΊβπ§))}) β© (β‘πΊ β {(πΊβπ§)}))) β βπ¦ β (ran πΊ β {0})π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦}))) |
64 | 40, 55, 63 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π΄ β (β β {0})) β§ (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄)) β βπ¦ β (ran πΊ β {0})π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦}))) |
65 | 64 | ex 414 |
. . . . 5
β’ ((π β§ π΄ β (β β {0})) β
((π§ β β β§
((πΉβπ§) Β· (πΊβπ§)) = π΄) β βπ¦ β (ran πΊ β {0})π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})))) |
66 | | fniniseg 7015 |
. . . . . . . . . . 11
β’ (πΉ Fn β β (π§ β (β‘πΉ β {(π΄ / π¦)}) β (π§ β β β§ (πΉβπ§) = (π΄ / π¦)))) |
67 | 16, 66 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π΄ β (β β {0})) β (π§ β (β‘πΉ β {(π΄ / π¦)}) β (π§ β β β§ (πΉβπ§) = (π΄ / π¦)))) |
68 | | fniniseg 7015 |
. . . . . . . . . . 11
β’ (πΊ Fn β β (π§ β (β‘πΊ β {π¦}) β (π§ β β β§ (πΊβπ§) = π¦))) |
69 | 17, 68 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π΄ β (β β {0})) β (π§ β (β‘πΊ β {π¦}) β (π§ β β β§ (πΊβπ§) = π¦))) |
70 | 67, 69 | anbi12d 632 |
. . . . . . . . 9
β’ ((π β§ π΄ β (β β {0})) β
((π§ β (β‘πΉ β {(π΄ / π¦)}) β§ π§ β (β‘πΊ β {π¦})) β ((π§ β β β§ (πΉβπ§) = (π΄ / π¦)) β§ (π§ β β β§ (πΊβπ§) = π¦)))) |
71 | | elin 3931 |
. . . . . . . . 9
β’ (π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) β (π§ β (β‘πΉ β {(π΄ / π¦)}) β§ π§ β (β‘πΊ β {π¦}))) |
72 | | anandi 675 |
. . . . . . . . 9
β’ ((π§ β β β§ ((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦)) β ((π§ β β β§ (πΉβπ§) = (π΄ / π¦)) β§ (π§ β β β§ (πΊβπ§) = π¦))) |
73 | 70, 71, 72 | 3bitr4g 314 |
. . . . . . . 8
β’ ((π β§ π΄ β (β β {0})) β (π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) β (π§ β β β§ ((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦)))) |
74 | 73 | adantr 482 |
. . . . . . 7
β’ (((π β§ π΄ β (β β {0})) β§ π¦ β (ran πΊ β {0})) β (π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) β (π§ β β β§ ((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦)))) |
75 | | eldifi 4091 |
. . . . . . . . . . . 12
β’ (π΄ β (β β {0})
β π΄ β
β) |
76 | 75 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β π΄ β β) |
77 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β πΊ:ββΆβ) |
78 | 77 | frnd 6681 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β ran πΊ β
β) |
79 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β π¦ β (ran πΊ β {0})) |
80 | | eldifsn 4752 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (ran πΊ β {0}) β (π¦ β ran πΊ β§ π¦ β 0)) |
81 | 79, 80 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β (π¦ β ran πΊ β§ π¦ β 0)) |
82 | 81 | simpld 496 |
. . . . . . . . . . . . 13
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β π¦ β ran πΊ) |
83 | 78, 82 | sseldd 3950 |
. . . . . . . . . . . 12
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β π¦ β β) |
84 | 83 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β π¦ β β) |
85 | 81 | simprd 497 |
. . . . . . . . . . 11
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β π¦ β 0) |
86 | 76, 84, 85 | divcan1d 11939 |
. . . . . . . . . 10
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β ((π΄ / π¦) Β· π¦) = π΄) |
87 | | oveq12 7371 |
. . . . . . . . . . 11
β’ (((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦) β ((πΉβπ§) Β· (πΊβπ§)) = ((π΄ / π¦) Β· π¦)) |
88 | 87 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦) β (((πΉβπ§) Β· (πΊβπ§)) = π΄ β ((π΄ / π¦) Β· π¦) = π΄)) |
89 | 86, 88 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (((π β§ π΄ β (β β {0})) β§ (π¦ β (ran πΊ β {0}) β§ π§ β β)) β (((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦) β ((πΉβπ§) Β· (πΊβπ§)) = π΄)) |
90 | 89 | anassrs 469 |
. . . . . . . 8
β’ ((((π β§ π΄ β (β β {0})) β§ π¦ β (ran πΊ β {0})) β§ π§ β β) β (((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦) β ((πΉβπ§) Β· (πΊβπ§)) = π΄)) |
91 | 90 | imdistanda 573 |
. . . . . . 7
β’ (((π β§ π΄ β (β β {0})) β§ π¦ β (ran πΊ β {0})) β ((π§ β β β§ ((πΉβπ§) = (π΄ / π¦) β§ (πΊβπ§) = π¦)) β (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄))) |
92 | 74, 91 | sylbid 239 |
. . . . . 6
β’ (((π β§ π΄ β (β β {0})) β§ π¦ β (ran πΊ β {0})) β (π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) β (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄))) |
93 | 92 | rexlimdva 3153 |
. . . . 5
β’ ((π β§ π΄ β (β β {0})) β
(βπ¦ β (ran πΊ β {0})π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) β (π§ β β β§ ((πΉβπ§) Β· (πΊβπ§)) = π΄))) |
94 | 65, 93 | impbid 211 |
. . . 4
β’ ((π β§ π΄ β (β β {0})) β
((π§ β β β§
((πΉβπ§) Β· (πΊβπ§)) = π΄) β βπ¦ β (ran πΊ β {0})π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})))) |
95 | 15, 23, 94 | 3bitrd 305 |
. . 3
β’ ((π β§ π΄ β (β β {0})) β (π§ β (β‘(πΉ βf Β· πΊ) β {π΄}) β βπ¦ β (ran πΊ β {0})π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})))) |
96 | | eliun 4963 |
. . 3
β’ (π§ β βͺ π¦ β (ran πΊ β {0})((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})) β βπ¦ β (ran πΊ β {0})π§ β ((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦}))) |
97 | 95, 96 | bitr4di 289 |
. 2
β’ ((π β§ π΄ β (β β {0})) β (π§ β (β‘(πΉ βf Β· πΊ) β {π΄}) β π§ β βͺ
π¦ β (ran πΊ β {0})((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦})))) |
98 | 97 | eqrdv 2735 |
1
β’ ((π β§ π΄ β (β β {0})) β (β‘(πΉ βf Β· πΊ) β {π΄}) = βͺ
π¦ β (ran πΊ β {0})((β‘πΉ β {(π΄ / π¦)}) β© (β‘πΊ β {π¦}))) |