Step |
Hyp |
Ref |
Expression |
1 |
|
cphsubrglem.k |
โข ๐พ = ( Base โ ๐น ) |
2 |
|
cphsubrglem.1 |
โข ( ๐ โ ๐น = ( โfld โพs ๐ด ) ) |
3 |
|
cphsubrglem.2 |
โข ( ๐ โ ๐น โ DivRing ) |
4 |
2
|
fveq2d |
โข ( ๐ โ ( Base โ ๐น ) = ( Base โ ( โfld โพs ๐ด ) ) ) |
5 |
|
drngring |
โข ( ๐น โ DivRing โ ๐น โ Ring ) |
6 |
3 5
|
syl |
โข ( ๐ โ ๐น โ Ring ) |
7 |
2 6
|
eqeltrrd |
โข ( ๐ โ ( โfld โพs ๐ด ) โ Ring ) |
8 |
|
eqid |
โข ( Base โ ( โfld โพs ๐ด ) ) = ( Base โ ( โfld โพs ๐ด ) ) |
9 |
|
eqid |
โข ( 0g โ ( โfld โพs ๐ด ) ) = ( 0g โ ( โfld โพs ๐ด ) ) |
10 |
8 9
|
ring0cl |
โข ( ( โfld โพs ๐ด ) โ Ring โ ( 0g โ ( โfld โพs ๐ด ) ) โ ( Base โ ( โfld โพs ๐ด ) ) ) |
11 |
|
reldmress |
โข Rel dom โพs |
12 |
|
eqid |
โข ( โfld โพs ๐ด ) = ( โfld โพs ๐ด ) |
13 |
11 12 8
|
elbasov |
โข ( ( 0g โ ( โfld โพs ๐ด ) ) โ ( Base โ ( โfld โพs ๐ด ) ) โ ( โfld โ V โง ๐ด โ V ) ) |
14 |
7 10 13
|
3syl |
โข ( ๐ โ ( โfld โ V โง ๐ด โ V ) ) |
15 |
14
|
simprd |
โข ( ๐ โ ๐ด โ V ) |
16 |
|
cnfldbas |
โข โ = ( Base โ โfld ) |
17 |
12 16
|
ressbas |
โข ( ๐ด โ V โ ( ๐ด โฉ โ ) = ( Base โ ( โfld โพs ๐ด ) ) ) |
18 |
15 17
|
syl |
โข ( ๐ โ ( ๐ด โฉ โ ) = ( Base โ ( โfld โพs ๐ด ) ) ) |
19 |
4 18
|
eqtr4d |
โข ( ๐ โ ( Base โ ๐น ) = ( ๐ด โฉ โ ) ) |
20 |
1 19
|
eqtrid |
โข ( ๐ โ ๐พ = ( ๐ด โฉ โ ) ) |
21 |
20
|
oveq2d |
โข ( ๐ โ ( โfld โพs ๐พ ) = ( โfld โพs ( ๐ด โฉ โ ) ) ) |
22 |
16
|
ressinbas |
โข ( ๐ด โ V โ ( โfld โพs ๐ด ) = ( โfld โพs ( ๐ด โฉ โ ) ) ) |
23 |
15 22
|
syl |
โข ( ๐ โ ( โfld โพs ๐ด ) = ( โfld โพs ( ๐ด โฉ โ ) ) ) |
24 |
21 23
|
eqtr4d |
โข ( ๐ โ ( โfld โพs ๐พ ) = ( โfld โพs ๐ด ) ) |
25 |
2 24
|
eqtr4d |
โข ( ๐ โ ๐น = ( โfld โพs ๐พ ) ) |
26 |
25 6
|
eqeltrrd |
โข ( ๐ โ ( โfld โพs ๐พ ) โ Ring ) |
27 |
|
cnring |
โข โfld โ Ring |
28 |
26 27
|
jctil |
โข ( ๐ โ ( โfld โ Ring โง ( โfld โพs ๐พ ) โ Ring ) ) |
29 |
12 16
|
ressbasss |
โข ( Base โ ( โfld โพs ๐ด ) ) โ โ |
30 |
4 29
|
eqsstrdi |
โข ( ๐ โ ( Base โ ๐น ) โ โ ) |
31 |
1 30
|
eqsstrid |
โข ( ๐ โ ๐พ โ โ ) |
32 |
|
eqid |
โข ( 0g โ ๐น ) = ( 0g โ ๐น ) |
33 |
|
eqid |
โข ( 1r โ ๐น ) = ( 1r โ ๐น ) |
34 |
32 33
|
drngunz |
โข ( ๐น โ DivRing โ ( 1r โ ๐น ) โ ( 0g โ ๐น ) ) |
35 |
3 34
|
syl |
โข ( ๐ โ ( 1r โ ๐น ) โ ( 0g โ ๐น ) ) |
36 |
25
|
fveq2d |
โข ( ๐ โ ( 0g โ ๐น ) = ( 0g โ ( โfld โพs ๐พ ) ) ) |
37 |
|
ringgrp |
โข ( โfld โ Ring โ โfld โ Grp ) |
38 |
27 37
|
mp1i |
โข ( ๐ โ โfld โ Grp ) |
39 |
|
ringgrp |
โข ( ( โfld โพs ๐พ ) โ Ring โ ( โfld โพs ๐พ ) โ Grp ) |
40 |
26 39
|
syl |
โข ( ๐ โ ( โfld โพs ๐พ ) โ Grp ) |
41 |
16
|
issubg |
โข ( ๐พ โ ( SubGrp โ โfld ) โ ( โfld โ Grp โง ๐พ โ โ โง ( โfld โพs ๐พ ) โ Grp ) ) |
42 |
38 31 40 41
|
syl3anbrc |
โข ( ๐ โ ๐พ โ ( SubGrp โ โfld ) ) |
43 |
|
eqid |
โข ( โfld โพs ๐พ ) = ( โfld โพs ๐พ ) |
44 |
|
cnfld0 |
โข 0 = ( 0g โ โfld ) |
45 |
43 44
|
subg0 |
โข ( ๐พ โ ( SubGrp โ โfld ) โ 0 = ( 0g โ ( โfld โพs ๐พ ) ) ) |
46 |
42 45
|
syl |
โข ( ๐ โ 0 = ( 0g โ ( โfld โพs ๐พ ) ) ) |
47 |
36 46
|
eqtr4d |
โข ( ๐ โ ( 0g โ ๐น ) = 0 ) |
48 |
35 47
|
neeqtrd |
โข ( ๐ โ ( 1r โ ๐น ) โ 0 ) |
49 |
48
|
neneqd |
โข ( ๐ โ ยฌ ( 1r โ ๐น ) = 0 ) |
50 |
1 33
|
ringidcl |
โข ( ๐น โ Ring โ ( 1r โ ๐น ) โ ๐พ ) |
51 |
6 50
|
syl |
โข ( ๐ โ ( 1r โ ๐น ) โ ๐พ ) |
52 |
31 51
|
sseldd |
โข ( ๐ โ ( 1r โ ๐น ) โ โ ) |
53 |
52
|
sqvald |
โข ( ๐ โ ( ( 1r โ ๐น ) โ 2 ) = ( ( 1r โ ๐น ) ยท ( 1r โ ๐น ) ) ) |
54 |
25
|
fveq2d |
โข ( ๐ โ ( 1r โ ๐น ) = ( 1r โ ( โfld โพs ๐พ ) ) ) |
55 |
54
|
oveq1d |
โข ( ๐ โ ( ( 1r โ ๐น ) ยท ( 1r โ ๐น ) ) = ( ( 1r โ ( โfld โพs ๐พ ) ) ยท ( 1r โ ๐น ) ) ) |
56 |
25
|
fveq2d |
โข ( ๐ โ ( Base โ ๐น ) = ( Base โ ( โfld โพs ๐พ ) ) ) |
57 |
1 56
|
eqtrid |
โข ( ๐ โ ๐พ = ( Base โ ( โfld โพs ๐พ ) ) ) |
58 |
51 57
|
eleqtrd |
โข ( ๐ โ ( 1r โ ๐น ) โ ( Base โ ( โfld โพs ๐พ ) ) ) |
59 |
|
eqid |
โข ( Base โ ( โfld โพs ๐พ ) ) = ( Base โ ( โfld โพs ๐พ ) ) |
60 |
1
|
fvexi |
โข ๐พ โ V |
61 |
|
cnfldmul |
โข ยท = ( .r โ โfld ) |
62 |
43 61
|
ressmulr |
โข ( ๐พ โ V โ ยท = ( .r โ ( โfld โพs ๐พ ) ) ) |
63 |
60 62
|
ax-mp |
โข ยท = ( .r โ ( โfld โพs ๐พ ) ) |
64 |
|
eqid |
โข ( 1r โ ( โfld โพs ๐พ ) ) = ( 1r โ ( โfld โพs ๐พ ) ) |
65 |
59 63 64
|
ringlidm |
โข ( ( ( โfld โพs ๐พ ) โ Ring โง ( 1r โ ๐น ) โ ( Base โ ( โfld โพs ๐พ ) ) ) โ ( ( 1r โ ( โfld โพs ๐พ ) ) ยท ( 1r โ ๐น ) ) = ( 1r โ ๐น ) ) |
66 |
26 58 65
|
syl2anc |
โข ( ๐ โ ( ( 1r โ ( โfld โพs ๐พ ) ) ยท ( 1r โ ๐น ) ) = ( 1r โ ๐น ) ) |
67 |
53 55 66
|
3eqtrd |
โข ( ๐ โ ( ( 1r โ ๐น ) โ 2 ) = ( 1r โ ๐น ) ) |
68 |
|
sq01 |
โข ( ( 1r โ ๐น ) โ โ โ ( ( ( 1r โ ๐น ) โ 2 ) = ( 1r โ ๐น ) โ ( ( 1r โ ๐น ) = 0 โจ ( 1r โ ๐น ) = 1 ) ) ) |
69 |
52 68
|
syl |
โข ( ๐ โ ( ( ( 1r โ ๐น ) โ 2 ) = ( 1r โ ๐น ) โ ( ( 1r โ ๐น ) = 0 โจ ( 1r โ ๐น ) = 1 ) ) ) |
70 |
67 69
|
mpbid |
โข ( ๐ โ ( ( 1r โ ๐น ) = 0 โจ ( 1r โ ๐น ) = 1 ) ) |
71 |
70
|
ord |
โข ( ๐ โ ( ยฌ ( 1r โ ๐น ) = 0 โ ( 1r โ ๐น ) = 1 ) ) |
72 |
49 71
|
mpd |
โข ( ๐ โ ( 1r โ ๐น ) = 1 ) |
73 |
72 51
|
eqeltrrd |
โข ( ๐ โ 1 โ ๐พ ) |
74 |
31 73
|
jca |
โข ( ๐ โ ( ๐พ โ โ โง 1 โ ๐พ ) ) |
75 |
|
cnfld1 |
โข 1 = ( 1r โ โfld ) |
76 |
16 75
|
issubrg |
โข ( ๐พ โ ( SubRing โ โfld ) โ ( ( โfld โ Ring โง ( โfld โพs ๐พ ) โ Ring ) โง ( ๐พ โ โ โง 1 โ ๐พ ) ) ) |
77 |
28 74 76
|
sylanbrc |
โข ( ๐ โ ๐พ โ ( SubRing โ โfld ) ) |
78 |
25 20 77
|
3jca |
โข ( ๐ โ ( ๐น = ( โfld โพs ๐พ ) โง ๐พ = ( ๐ด โฉ โ ) โง ๐พ โ ( SubRing โ โfld ) ) ) |