Step | Hyp | Ref
| Expression |
1 | | ax-hv0cl 29994 |
. . 3
β’
0β β β |
2 | | nlelsh.1 |
. . . 4
β’ π β LinFn |
3 | 2 | lnfn0i 31033 |
. . 3
β’ (πβ0β) =
0 |
4 | 2 | lnfnfi 31032 |
. . . 4
β’ π:
ββΆβ |
5 | | elnlfn 30919 |
. . . 4
β’ (π: ββΆβ β
(0β β (nullβπ) β (0β β
β β§ (πβ0β) =
0))) |
6 | 4, 5 | ax-mp 5 |
. . 3
β’
(0β β (nullβπ) β (0β β
β β§ (πβ0β) =
0)) |
7 | 1, 3, 6 | mpbir2an 710 |
. 2
β’
0β β (nullβπ) |
8 | | nlfnval 30872 |
. . . . . . . . . 10
β’ (π: ββΆβ β
(nullβπ) = (β‘π β {0})) |
9 | 4, 8 | ax-mp 5 |
. . . . . . . . 9
β’
(nullβπ) =
(β‘π β {0}) |
10 | | cnvimass 6037 |
. . . . . . . . 9
β’ (β‘π β {0}) β dom π |
11 | 9, 10 | eqsstri 3982 |
. . . . . . . 8
β’
(nullβπ)
β dom π |
12 | 4 | fdmi 6684 |
. . . . . . . 8
β’ dom π = β |
13 | 11, 12 | sseqtri 3984 |
. . . . . . 7
β’
(nullβπ)
β β |
14 | 13 | sseli 3944 |
. . . . . 6
β’ (π₯ β (nullβπ) β π₯ β β) |
15 | 13 | sseli 3944 |
. . . . . 6
β’ (π¦ β (nullβπ) β π¦ β β) |
16 | | hvaddcl 30003 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β (π₯ +β π¦) β
β) |
17 | 14, 15, 16 | syl2an 597 |
. . . . 5
β’ ((π₯ β (nullβπ) β§ π¦ β (nullβπ)) β (π₯ +β π¦) β β) |
18 | 2 | lnfnaddi 31034 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β (πβ(π₯ +β π¦)) = ((πβπ₯) + (πβπ¦))) |
19 | 14, 15, 18 | syl2an 597 |
. . . . . . 7
β’ ((π₯ β (nullβπ) β§ π¦ β (nullβπ)) β (πβ(π₯ +β π¦)) = ((πβπ₯) + (πβπ¦))) |
20 | | elnlfn 30919 |
. . . . . . . . . 10
β’ (π: ββΆβ β
(π₯ β (nullβπ) β (π₯ β β β§ (πβπ₯) = 0))) |
21 | 4, 20 | ax-mp 5 |
. . . . . . . . 9
β’ (π₯ β (nullβπ) β (π₯ β β β§ (πβπ₯) = 0)) |
22 | 21 | simprbi 498 |
. . . . . . . 8
β’ (π₯ β (nullβπ) β (πβπ₯) = 0) |
23 | | elnlfn 30919 |
. . . . . . . . . 10
β’ (π: ββΆβ β
(π¦ β (nullβπ) β (π¦ β β β§ (πβπ¦) = 0))) |
24 | 4, 23 | ax-mp 5 |
. . . . . . . . 9
β’ (π¦ β (nullβπ) β (π¦ β β β§ (πβπ¦) = 0)) |
25 | 24 | simprbi 498 |
. . . . . . . 8
β’ (π¦ β (nullβπ) β (πβπ¦) = 0) |
26 | 22, 25 | oveqan12d 7380 |
. . . . . . 7
β’ ((π₯ β (nullβπ) β§ π¦ β (nullβπ)) β ((πβπ₯) + (πβπ¦)) = (0 + 0)) |
27 | 19, 26 | eqtrd 2773 |
. . . . . 6
β’ ((π₯ β (nullβπ) β§ π¦ β (nullβπ)) β (πβ(π₯ +β π¦)) = (0 + 0)) |
28 | | 00id 11338 |
. . . . . 6
β’ (0 + 0) =
0 |
29 | 27, 28 | eqtrdi 2789 |
. . . . 5
β’ ((π₯ β (nullβπ) β§ π¦ β (nullβπ)) β (πβ(π₯ +β π¦)) = 0) |
30 | | elnlfn 30919 |
. . . . . 6
β’ (π: ββΆβ β
((π₯ +β
π¦) β (nullβπ) β ((π₯ +β π¦) β β β§ (πβ(π₯ +β π¦)) = 0))) |
31 | 4, 30 | ax-mp 5 |
. . . . 5
β’ ((π₯ +β π¦) β (nullβπ) β ((π₯ +β π¦) β β β§ (πβ(π₯ +β π¦)) = 0)) |
32 | 17, 29, 31 | sylanbrc 584 |
. . . 4
β’ ((π₯ β (nullβπ) β§ π¦ β (nullβπ)) β (π₯ +β π¦) β (nullβπ)) |
33 | 32 | rgen2 3191 |
. . 3
β’
βπ₯ β
(nullβπ)βπ¦ β (nullβπ)(π₯ +β π¦) β (nullβπ) |
34 | | hvmulcl 30004 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β (π₯
Β·β π¦) β β) |
35 | 15, 34 | sylan2 594 |
. . . . 5
β’ ((π₯ β β β§ π¦ β (nullβπ)) β (π₯ Β·β π¦) β
β) |
36 | 2 | lnfnmuli 31035 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β (πβ(π₯ Β·β π¦)) = (π₯ Β· (πβπ¦))) |
37 | 15, 36 | sylan2 594 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β (nullβπ)) β (πβ(π₯ Β·β π¦)) = (π₯ Β· (πβπ¦))) |
38 | 25 | oveq2d 7377 |
. . . . . . 7
β’ (π¦ β (nullβπ) β (π₯ Β· (πβπ¦)) = (π₯ Β· 0)) |
39 | | mul01 11342 |
. . . . . . 7
β’ (π₯ β β β (π₯ Β· 0) =
0) |
40 | 38, 39 | sylan9eqr 2795 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β (nullβπ)) β (π₯ Β· (πβπ¦)) = 0) |
41 | 37, 40 | eqtrd 2773 |
. . . . 5
β’ ((π₯ β β β§ π¦ β (nullβπ)) β (πβ(π₯ Β·β π¦)) = 0) |
42 | | elnlfn 30919 |
. . . . . 6
β’ (π: ββΆβ β
((π₯
Β·β π¦) β (nullβπ) β ((π₯ Β·β π¦) β β β§ (πβ(π₯ Β·β π¦)) = 0))) |
43 | 4, 42 | ax-mp 5 |
. . . . 5
β’ ((π₯
Β·β π¦) β (nullβπ) β ((π₯ Β·β π¦) β β β§ (πβ(π₯ Β·β π¦)) = 0)) |
44 | 35, 41, 43 | sylanbrc 584 |
. . . 4
β’ ((π₯ β β β§ π¦ β (nullβπ)) β (π₯ Β·β π¦) β (nullβπ)) |
45 | 44 | rgen2 3191 |
. . 3
β’
βπ₯ β
β βπ¦ β
(nullβπ)(π₯
Β·β π¦) β (nullβπ) |
46 | 33, 45 | pm3.2i 472 |
. 2
β’
(βπ₯ β
(nullβπ)βπ¦ β (nullβπ)(π₯ +β π¦) β (nullβπ) β§ βπ₯ β β βπ¦ β (nullβπ)(π₯ Β·β π¦) β (nullβπ)) |
47 | | issh3 30210 |
. . 3
β’
((nullβπ)
β β β ((nullβπ) β Sβ
β (0β β (nullβπ) β§ (βπ₯ β (nullβπ)βπ¦ β (nullβπ)(π₯ +β π¦) β (nullβπ) β§ βπ₯ β β βπ¦ β (nullβπ)(π₯ Β·β π¦) β (nullβπ))))) |
48 | 13, 47 | ax-mp 5 |
. 2
β’
((nullβπ)
β Sβ β (0β β
(nullβπ) β§
(βπ₯ β
(nullβπ)βπ¦ β (nullβπ)(π₯ +β π¦) β (nullβπ) β§ βπ₯ β β βπ¦ β (nullβπ)(π₯ Β·β π¦) β (nullβπ)))) |
49 | 7, 46, 48 | mpbir2an 710 |
1
β’
(nullβπ)
β Sβ |