Step |
Hyp |
Ref |
Expression |
1 |
|
drnginvrl.b |
โข ๐ต = ( Base โ ๐
) |
2 |
|
drnginvrl.z |
โข 0 = ( 0g โ ๐
) |
3 |
|
drnginvrl.t |
โข ยท = ( .r โ ๐
) |
4 |
|
drnginvrl.u |
โข 1 = ( 1r โ ๐
) |
5 |
|
drnginvrl.i |
โข ๐ผ = ( invr โ ๐
) |
6 |
|
eqid |
โข ( Unit โ ๐
) = ( Unit โ ๐
) |
7 |
1 6 2
|
drngunit |
โข ( ๐
โ DivRing โ ( ๐ โ ( Unit โ ๐
) โ ( ๐ โ ๐ต โง ๐ โ 0 ) ) ) |
8 |
|
drngring |
โข ( ๐
โ DivRing โ ๐
โ Ring ) |
9 |
6 5 3 4
|
unitrinv |
โข ( ( ๐
โ Ring โง ๐ โ ( Unit โ ๐
) ) โ ( ๐ ยท ( ๐ผ โ ๐ ) ) = 1 ) |
10 |
9
|
ex |
โข ( ๐
โ Ring โ ( ๐ โ ( Unit โ ๐
) โ ( ๐ ยท ( ๐ผ โ ๐ ) ) = 1 ) ) |
11 |
8 10
|
syl |
โข ( ๐
โ DivRing โ ( ๐ โ ( Unit โ ๐
) โ ( ๐ ยท ( ๐ผ โ ๐ ) ) = 1 ) ) |
12 |
7 11
|
sylbird |
โข ( ๐
โ DivRing โ ( ( ๐ โ ๐ต โง ๐ โ 0 ) โ ( ๐ ยท ( ๐ผ โ ๐ ) ) = 1 ) ) |
13 |
12
|
3impib |
โข ( ( ๐
โ DivRing โง ๐ โ ๐ต โง ๐ โ 0 ) โ ( ๐ ยท ( ๐ผ โ ๐ ) ) = 1 ) |