Step | Hyp | Ref
| Expression |
1 | | simp2 1138 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β πΉ:π΄βΆβ) |
2 | 1 | ffnd 6716 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β πΉ Fn π΄) |
3 | | simp3 1139 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β πΊ:π΄βΆβ) |
4 | 3 | ffnd 6716 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β πΊ Fn π΄) |
5 | | simp1 1137 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β π΄ β π) |
6 | | inidm 4218 |
. . . . . 6
β’ (π΄ β© π΄) = π΄ |
7 | | eqidd 2734 |
. . . . . 6
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β (πΉβπ₯) = (πΉβπ₯)) |
8 | | eqidd 2734 |
. . . . . 6
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β (πΊβπ₯) = (πΊβπ₯)) |
9 | 2, 4, 5, 5, 6, 7, 8 | ofval 7678 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β ((πΉ βf β πΊ)βπ₯) = ((πΉβπ₯) β (πΊβπ₯))) |
10 | | c0ex 11205 |
. . . . . . 7
β’ 0 β
V |
11 | 10 | fvconst2 7202 |
. . . . . 6
β’ (π₯ β π΄ β ((π΄ Γ {0})βπ₯) = 0) |
12 | 11 | adantl 483 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β ((π΄ Γ {0})βπ₯) = 0) |
13 | 9, 12 | eqeq12d 2749 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β (((πΉ βf β πΊ)βπ₯) = ((π΄ Γ {0})βπ₯) β ((πΉβπ₯) β (πΊβπ₯)) = 0)) |
14 | 1 | ffvelcdmda 7084 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β (πΉβπ₯) β β) |
15 | 3 | ffvelcdmda 7084 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β (πΊβπ₯) β β) |
16 | 14, 15 | subeq0ad 11578 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β (((πΉβπ₯) β (πΊβπ₯)) = 0 β (πΉβπ₯) = (πΊβπ₯))) |
17 | 13, 16 | bitrd 279 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β§ π₯ β π΄) β (((πΉ βf β πΊ)βπ₯) = ((π΄ Γ {0})βπ₯) β (πΉβπ₯) = (πΊβπ₯))) |
18 | 17 | ralbidva 3176 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β (βπ₯ β π΄ ((πΉ βf β πΊ)βπ₯) = ((π΄ Γ {0})βπ₯) β βπ₯ β π΄ (πΉβπ₯) = (πΊβπ₯))) |
19 | 2, 4, 5, 5, 6 | offn 7680 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β (πΉ βf β πΊ) Fn π΄) |
20 | 10 | fconst 6775 |
. . . 4
β’ (π΄ Γ {0}):π΄βΆ{0} |
21 | | ffn 6715 |
. . . 4
β’ ((π΄ Γ {0}):π΄βΆ{0} β (π΄ Γ {0}) Fn π΄) |
22 | 20, 21 | ax-mp 5 |
. . 3
β’ (π΄ Γ {0}) Fn π΄ |
23 | | eqfnfv 7030 |
. . 3
β’ (((πΉ βf β
πΊ) Fn π΄ β§ (π΄ Γ {0}) Fn π΄) β ((πΉ βf β πΊ) = (π΄ Γ {0}) β βπ₯ β π΄ ((πΉ βf β πΊ)βπ₯) = ((π΄ Γ {0})βπ₯))) |
24 | 19, 22, 23 | sylancl 587 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β ((πΉ βf β πΊ) = (π΄ Γ {0}) β βπ₯ β π΄ ((πΉ βf β πΊ)βπ₯) = ((π΄ Γ {0})βπ₯))) |
25 | | eqfnfv 7030 |
. . 3
β’ ((πΉ Fn π΄ β§ πΊ Fn π΄) β (πΉ = πΊ β βπ₯ β π΄ (πΉβπ₯) = (πΊβπ₯))) |
26 | 2, 4, 25 | syl2anc 585 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β (πΉ = πΊ β βπ₯ β π΄ (πΉβπ₯) = (πΊβπ₯))) |
27 | 18, 24, 26 | 3bitr4d 311 |
1
β’ ((π΄ β π β§ πΉ:π΄βΆβ β§ πΊ:π΄βΆβ) β ((πΉ βf β πΊ) = (π΄ Γ {0}) β πΉ = πΊ)) |