Step |
Hyp |
Ref |
Expression |
1 |
|
mulgnncl.b |
โข ๐ต = ( Base โ ๐บ ) |
2 |
|
mulgnncl.t |
โข ยท = ( .g โ ๐บ ) |
3 |
|
eqid |
โข ( +g โ ๐บ ) = ( +g โ ๐บ ) |
4 |
|
id |
โข ( ๐บ โ Grp โ ๐บ โ Grp ) |
5 |
|
ssidd |
โข ( ๐บ โ Grp โ ๐ต โ ๐ต ) |
6 |
1 3
|
grpcl |
โข ( ( ๐บ โ Grp โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต ) โ ( ๐ฅ ( +g โ ๐บ ) ๐ฆ ) โ ๐ต ) |
7 |
|
eqid |
โข ( 0g โ ๐บ ) = ( 0g โ ๐บ ) |
8 |
1 7
|
grpidcl |
โข ( ๐บ โ Grp โ ( 0g โ ๐บ ) โ ๐ต ) |
9 |
|
eqid |
โข ( invg โ ๐บ ) = ( invg โ ๐บ ) |
10 |
1 9
|
grpinvcl |
โข ( ( ๐บ โ Grp โง ๐ฅ โ ๐ต ) โ ( ( invg โ ๐บ ) โ ๐ฅ ) โ ๐ต ) |
11 |
1 2 3 4 5 6 7 8 9 10
|
mulgsubcl |
โข ( ( ๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต ) โ ( ๐ ยท ๐ ) โ ๐ต ) |