Step |
Hyp |
Ref |
Expression |
1 |
|
imasaddf.f |
โข ( ๐ โ ๐น : ๐ โontoโ ๐ต ) |
2 |
|
imasaddf.e |
โข ( ( ๐ โง ( ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( ( ( ๐น โ ๐ ) = ( ๐น โ ๐ ) โง ( ๐น โ ๐ ) = ( ๐น โ ๐ ) ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) ) |
3 |
|
imasaddf.u |
โข ( ๐ โ ๐ = ( ๐น โs ๐
) ) |
4 |
|
imasaddf.v |
โข ( ๐ โ ๐ = ( Base โ ๐
) ) |
5 |
|
imasaddf.r |
โข ( ๐ โ ๐
โ ๐ ) |
6 |
|
imasaddf.p |
โข ยท = ( +g โ ๐
) |
7 |
|
imasaddf.a |
โข โ = ( +g โ ๐ ) |
8 |
|
imasaddf.c |
โข ( ( ๐ โง ( ๐ โ ๐ โง ๐ โ ๐ ) ) โ ( ๐ ยท ๐ ) โ ๐ ) |
9 |
3 4 1 5 6 7
|
imasplusg |
โข ( ๐ โ โ = โช ๐ โ ๐ โช ๐ โ ๐ { โจ โจ ( ๐น โ ๐ ) , ( ๐น โ ๐ ) โฉ , ( ๐น โ ( ๐ ยท ๐ ) ) โฉ } ) |
10 |
1 2 9 8
|
imasaddflem |
โข ( ๐ โ โ : ( ๐ต ร ๐ต ) โถ ๐ต ) |