Step | Hyp | Ref
| Expression |
1 | | fex 7230 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β π) β πΉ β V) |
2 | 1 | 3adant2 1131 |
. . 3
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β πΉ β V) |
3 | | fex 7230 |
. . . 4
β’ ((πΊ:π΄βΆβ β§ π΄ β π) β πΊ β V) |
4 | 3 | 3adant1 1130 |
. . 3
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β πΊ β V) |
5 | | fdivval 47313 |
. . . 4
β’ ((πΉ β V β§ πΊ β V) β (πΉ /f πΊ) = ((πΉ βf / πΊ) βΎ (πΊ supp 0))) |
6 | | offres 7972 |
. . . 4
β’ ((πΉ β V β§ πΊ β V) β ((πΉ βf / πΊ) βΎ (πΊ supp 0)) = ((πΉ βΎ (πΊ supp 0)) βf / (πΊ βΎ (πΊ supp 0)))) |
7 | 5, 6 | eqtrd 2772 |
. . 3
β’ ((πΉ β V β§ πΊ β V) β (πΉ /f πΊ) = ((πΉ βΎ (πΊ supp 0)) βf / (πΊ βΎ (πΊ supp 0)))) |
8 | 2, 4, 7 | syl2anc 584 |
. 2
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΉ /f πΊ) = ((πΉ βΎ (πΊ supp 0)) βf / (πΊ βΎ (πΊ supp 0)))) |
9 | | ffn 6717 |
. . . . 5
β’ (πΉ:π΄βΆβ β πΉ Fn π΄) |
10 | 9 | 3ad2ant1 1133 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β πΉ Fn π΄) |
11 | | suppssdm 8164 |
. . . . 5
β’ (πΊ supp 0) β dom πΊ |
12 | | fdm 6726 |
. . . . . . 7
β’ (πΊ:π΄βΆβ β dom πΊ = π΄) |
13 | 12 | eqcomd 2738 |
. . . . . 6
β’ (πΊ:π΄βΆβ β π΄ = dom πΊ) |
14 | 13 | 3ad2ant2 1134 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β π΄ = dom πΊ) |
15 | 11, 14 | sseqtrrid 4035 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΊ supp 0) β π΄) |
16 | | fnssres 6673 |
. . . 4
β’ ((πΉ Fn π΄ β§ (πΊ supp 0) β π΄) β (πΉ βΎ (πΊ supp 0)) Fn (πΊ supp 0)) |
17 | 10, 15, 16 | syl2anc 584 |
. . 3
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΉ βΎ (πΊ supp 0)) Fn (πΊ supp 0)) |
18 | | ffn 6717 |
. . . . 5
β’ (πΊ:π΄βΆβ β πΊ Fn π΄) |
19 | 18 | 3ad2ant2 1134 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β πΊ Fn π΄) |
20 | | fnssres 6673 |
. . . 4
β’ ((πΊ Fn π΄ β§ (πΊ supp 0) β π΄) β (πΊ βΎ (πΊ supp 0)) Fn (πΊ supp 0)) |
21 | 19, 15, 20 | syl2anc 584 |
. . 3
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΊ βΎ (πΊ supp 0)) Fn (πΊ supp 0)) |
22 | | ovexd 7446 |
. . 3
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΊ supp 0) β V) |
23 | | inidm 4218 |
. . 3
β’ ((πΊ supp 0) β© (πΊ supp 0)) = (πΊ supp 0) |
24 | | fvres 6910 |
. . . 4
β’ (π₯ β (πΊ supp 0) β ((πΉ βΎ (πΊ supp 0))βπ₯) = (πΉβπ₯)) |
25 | 24 | adantl 482 |
. . 3
β’ (((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β§ π₯ β (πΊ supp 0)) β ((πΉ βΎ (πΊ supp 0))βπ₯) = (πΉβπ₯)) |
26 | | fvres 6910 |
. . . 4
β’ (π₯ β (πΊ supp 0) β ((πΊ βΎ (πΊ supp 0))βπ₯) = (πΊβπ₯)) |
27 | 26 | adantl 482 |
. . 3
β’ (((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β§ π₯ β (πΊ supp 0)) β ((πΊ βΎ (πΊ supp 0))βπ₯) = (πΊβπ₯)) |
28 | 17, 21, 22, 22, 23, 25, 27 | offval 7681 |
. 2
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β ((πΉ βΎ (πΊ supp 0)) βf / (πΊ βΎ (πΊ supp 0))) = (π₯ β (πΊ supp 0) β¦ ((πΉβπ₯) / (πΊβπ₯)))) |
29 | 8, 28 | eqtrd 2772 |
1
β’ ((πΉ:π΄βΆβ β§ πΊ:π΄βΆβ β§ π΄ β π) β (πΉ /f πΊ) = (π₯ β (πΊ supp 0) β¦ ((πΉβπ₯) / (πΊβπ₯)))) |