Step | Hyp | Ref
| Expression |
1 | | 0cn 11155 |
. . 3
β’ 0 β
β |
2 | 1 | fconst6 6736 |
. 2
β’ ( β
Γ {0}): ββΆβ |
3 | | hvmulcl 30004 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β (π₯
Β·β π¦) β β) |
4 | | hvaddcl 30003 |
. . . . . . 7
β’ (((π₯
Β·β π¦) β β β§ π§ β β) β ((π₯ Β·β π¦) +β π§) β
β) |
5 | 3, 4 | sylan 581 |
. . . . . 6
β’ (((π₯ β β β§ π¦ β β) β§ π§ β β) β ((π₯
Β·β π¦) +β π§) β β) |
6 | | c0ex 11157 |
. . . . . . 7
β’ 0 β
V |
7 | 6 | fvconst2 7157 |
. . . . . 6
β’ (((π₯
Β·β π¦) +β π§) β β β (( β Γ
{0})β((π₯
Β·β π¦) +β π§)) = 0) |
8 | 5, 7 | syl 17 |
. . . . 5
β’ (((π₯ β β β§ π¦ β β) β§ π§ β β) β ((
β Γ {0})β((π₯ Β·β π¦) +β π§)) = 0) |
9 | 6 | fvconst2 7157 |
. . . . . . . . 9
β’ (π¦ β β β ((
β Γ {0})βπ¦) = 0) |
10 | 9 | oveq2d 7377 |
. . . . . . . 8
β’ (π¦ β β β (π₯ Β· (( β Γ
{0})βπ¦)) = (π₯ Β· 0)) |
11 | | mul01 11342 |
. . . . . . . 8
β’ (π₯ β β β (π₯ Β· 0) =
0) |
12 | 10, 11 | sylan9eqr 2795 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· (( β Γ
{0})βπ¦)) =
0) |
13 | 6 | fvconst2 7157 |
. . . . . . 7
β’ (π§ β β β ((
β Γ {0})βπ§) = 0) |
14 | 12, 13 | oveqan12d 7380 |
. . . . . 6
β’ (((π₯ β β β§ π¦ β β) β§ π§ β β) β ((π₯ Β· (( β Γ
{0})βπ¦)) + (( β
Γ {0})βπ§)) = (0
+ 0)) |
15 | | 00id 11338 |
. . . . . 6
β’ (0 + 0) =
0 |
16 | 14, 15 | eqtrdi 2789 |
. . . . 5
β’ (((π₯ β β β§ π¦ β β) β§ π§ β β) β ((π₯ Β· (( β Γ
{0})βπ¦)) + (( β
Γ {0})βπ§)) =
0) |
17 | 8, 16 | eqtr4d 2776 |
. . . 4
β’ (((π₯ β β β§ π¦ β β) β§ π§ β β) β ((
β Γ {0})β((π₯ Β·β π¦) +β π§)) = ((π₯ Β· (( β Γ {0})βπ¦)) + (( β Γ
{0})βπ§))) |
18 | 17 | 3impa 1111 |
. . 3
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((
β Γ {0})β((π₯ Β·β π¦) +β π§)) = ((π₯ Β· (( β Γ {0})βπ¦)) + (( β Γ
{0})βπ§))) |
19 | 18 | rgen3 3196 |
. 2
β’
βπ₯ β
β βπ¦ β
β βπ§ β
β (( β Γ {0})β((π₯ Β·β π¦) +β π§)) = ((π₯ Β· (( β Γ {0})βπ¦)) + (( β Γ
{0})βπ§)) |
20 | | ellnfn 30874 |
. 2
β’ ((
β Γ {0}) β LinFn β (( β Γ {0}):
ββΆβ β§ βπ₯ β β βπ¦ β β βπ§ β β (( β Γ
{0})β((π₯
Β·β π¦) +β π§)) = ((π₯ Β· (( β Γ {0})βπ¦)) + (( β Γ
{0})βπ§)))) |
21 | 2, 19, 20 | mpbir2an 710 |
1
β’ ( β
Γ {0}) β LinFn |