Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ๐ฅ โ โค ) |
2 |
|
ax-1cn |
โข 1 โ โ |
3 |
|
cnfldmulg |
โข ( ( ๐ฅ โ โค โง 1 โ โ ) โ ( ๐ฅ ( .g โ โfld ) 1 ) = ( ๐ฅ ยท 1 ) ) |
4 |
1 2 3
|
sylancl |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ( ๐ฅ ( .g โ โfld ) 1 ) = ( ๐ฅ ยท 1 ) ) |
5 |
|
zcn |
โข ( ๐ฅ โ โค โ ๐ฅ โ โ ) |
6 |
5
|
adantl |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ๐ฅ โ โ ) |
7 |
6
|
mulridd |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ( ๐ฅ ยท 1 ) = ๐ฅ ) |
8 |
4 7
|
eqtrd |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ( ๐ฅ ( .g โ โfld ) 1 ) = ๐ฅ ) |
9 |
|
subrgsubg |
โข ( ๐
โ ( SubRing โ โfld ) โ ๐
โ ( SubGrp โ โfld ) ) |
10 |
9
|
adantr |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ๐
โ ( SubGrp โ โfld ) ) |
11 |
|
cnfld1 |
โข 1 = ( 1r โ โfld ) |
12 |
11
|
subrg1cl |
โข ( ๐
โ ( SubRing โ โfld ) โ 1 โ ๐
) |
13 |
12
|
adantr |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ 1 โ ๐
) |
14 |
|
eqid |
โข ( .g โ โfld ) = ( .g โ โfld ) |
15 |
14
|
subgmulgcl |
โข ( ( ๐
โ ( SubGrp โ โfld ) โง ๐ฅ โ โค โง 1 โ ๐
) โ ( ๐ฅ ( .g โ โfld ) 1 ) โ ๐
) |
16 |
10 1 13 15
|
syl3anc |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ( ๐ฅ ( .g โ โfld ) 1 ) โ ๐
) |
17 |
8 16
|
eqeltrrd |
โข ( ( ๐
โ ( SubRing โ โfld ) โง ๐ฅ โ โค ) โ ๐ฅ โ ๐
) |
18 |
17
|
ex |
โข ( ๐
โ ( SubRing โ โfld ) โ ( ๐ฅ โ โค โ ๐ฅ โ ๐
) ) |
19 |
18
|
ssrdv |
โข ( ๐
โ ( SubRing โ โfld ) โ โค โ ๐
) |