Step | Hyp | Ref
| Expression |
1 | | cphsubrglem.1 |
. . 3
β’ (π β πΉ = (βfld
βΎs π΄)) |
2 | | cphsubrglem.k |
. . . . . 6
β’ πΎ = (BaseβπΉ) |
3 | 1 | fveq2d 6850 |
. . . . . . 7
β’ (π β (BaseβπΉ) =
(Baseβ(βfld βΎs π΄))) |
4 | | cphsubrglem.2 |
. . . . . . . . . . . 12
β’ (π β πΉ β DivRing) |
5 | | drngring 20226 |
. . . . . . . . . . . 12
β’ (πΉ β DivRing β πΉ β Ring) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ β Ring) |
7 | 1, 6 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (π β (βfld
βΎs π΄)
β Ring) |
8 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβ(βfld βΎs π΄)) = (Baseβ(βfld
βΎs π΄)) |
9 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβ(βfld βΎs π΄)) =
(0gβ(βfld βΎs π΄)) |
10 | 8, 9 | ring0cl 19998 |
. . . . . . . . . 10
β’
((βfld βΎs π΄) β Ring β
(0gβ(βfld βΎs π΄)) β
(Baseβ(βfld βΎs π΄))) |
11 | | reldmress 17122 |
. . . . . . . . . . 11
β’ Rel dom
βΎs |
12 | | eqid 2733 |
. . . . . . . . . . 11
β’
(βfld βΎs π΄) = (βfld
βΎs π΄) |
13 | 11, 12, 8 | elbasov 17098 |
. . . . . . . . . 10
β’
((0gβ(βfld βΎs π΄)) β
(Baseβ(βfld βΎs π΄)) β (βfld β V
β§ π΄ β
V)) |
14 | 7, 10, 13 | 3syl 18 |
. . . . . . . . 9
β’ (π β (βfld
β V β§ π΄ β
V)) |
15 | 14 | simprd 497 |
. . . . . . . 8
β’ (π β π΄ β V) |
16 | | cnfldbas 20823 |
. . . . . . . . 9
β’ β =
(Baseββfld) |
17 | 12, 16 | ressbas 17126 |
. . . . . . . 8
β’ (π΄ β V β (π΄ β© β) =
(Baseβ(βfld βΎs π΄))) |
18 | 15, 17 | syl 17 |
. . . . . . 7
β’ (π β (π΄ β© β) =
(Baseβ(βfld βΎs π΄))) |
19 | 3, 18 | eqtr4d 2776 |
. . . . . 6
β’ (π β (BaseβπΉ) = (π΄ β© β)) |
20 | 2, 19 | eqtrid 2785 |
. . . . 5
β’ (π β πΎ = (π΄ β© β)) |
21 | 20 | oveq2d 7377 |
. . . 4
β’ (π β (βfld
βΎs πΎ) =
(βfld βΎs (π΄ β© β))) |
22 | 16 | ressinbas 17134 |
. . . . 5
β’ (π΄ β V β
(βfld βΎs π΄) = (βfld
βΎs (π΄
β© β))) |
23 | 15, 22 | syl 17 |
. . . 4
β’ (π β (βfld
βΎs π΄) =
(βfld βΎs (π΄ β© β))) |
24 | 21, 23 | eqtr4d 2776 |
. . 3
β’ (π β (βfld
βΎs πΎ) =
(βfld βΎs π΄)) |
25 | 1, 24 | eqtr4d 2776 |
. 2
β’ (π β πΉ = (βfld
βΎs πΎ)) |
26 | 25, 6 | eqeltrrd 2835 |
. . . 4
β’ (π β (βfld
βΎs πΎ)
β Ring) |
27 | | cnring 20842 |
. . . 4
β’
βfld β Ring |
28 | 26, 27 | jctil 521 |
. . 3
β’ (π β (βfld
β Ring β§ (βfld βΎs πΎ) β Ring)) |
29 | 12, 16 | ressbasss 17129 |
. . . . . 6
β’
(Baseβ(βfld βΎs π΄)) β β |
30 | 3, 29 | eqsstrdi 4002 |
. . . . 5
β’ (π β (BaseβπΉ) β
β) |
31 | 2, 30 | eqsstrid 3996 |
. . . 4
β’ (π β πΎ β β) |
32 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβπΉ) = (0gβπΉ) |
33 | | eqid 2733 |
. . . . . . . . . 10
β’
(1rβπΉ) = (1rβπΉ) |
34 | 32, 33 | drngunz 20237 |
. . . . . . . . 9
β’ (πΉ β DivRing β
(1rβπΉ)
β (0gβπΉ)) |
35 | 4, 34 | syl 17 |
. . . . . . . 8
β’ (π β (1rβπΉ) β
(0gβπΉ)) |
36 | 25 | fveq2d 6850 |
. . . . . . . . 9
β’ (π β (0gβπΉ) =
(0gβ(βfld βΎs πΎ))) |
37 | | ringgrp 19977 |
. . . . . . . . . . . 12
β’
(βfld β Ring β βfld β
Grp) |
38 | 27, 37 | mp1i 13 |
. . . . . . . . . . 11
β’ (π β βfld
β Grp) |
39 | | ringgrp 19977 |
. . . . . . . . . . . 12
β’
((βfld βΎs πΎ) β Ring β (βfld
βΎs πΎ)
β Grp) |
40 | 26, 39 | syl 17 |
. . . . . . . . . . 11
β’ (π β (βfld
βΎs πΎ)
β Grp) |
41 | 16 | issubg 18936 |
. . . . . . . . . . 11
β’ (πΎ β
(SubGrpββfld) β (βfld β Grp
β§ πΎ β β
β§ (βfld βΎs πΎ) β Grp)) |
42 | 38, 31, 40, 41 | syl3anbrc 1344 |
. . . . . . . . . 10
β’ (π β πΎ β
(SubGrpββfld)) |
43 | | eqid 2733 |
. . . . . . . . . . 11
β’
(βfld βΎs πΎ) = (βfld
βΎs πΎ) |
44 | | cnfld0 20844 |
. . . . . . . . . . 11
β’ 0 =
(0gββfld) |
45 | 43, 44 | subg0 18942 |
. . . . . . . . . 10
β’ (πΎ β
(SubGrpββfld) β 0 =
(0gβ(βfld βΎs πΎ))) |
46 | 42, 45 | syl 17 |
. . . . . . . . 9
β’ (π β 0 =
(0gβ(βfld βΎs πΎ))) |
47 | 36, 46 | eqtr4d 2776 |
. . . . . . . 8
β’ (π β (0gβπΉ) = 0) |
48 | 35, 47 | neeqtrd 3010 |
. . . . . . 7
β’ (π β (1rβπΉ) β 0) |
49 | 48 | neneqd 2945 |
. . . . . 6
β’ (π β Β¬
(1rβπΉ) =
0) |
50 | 2, 33 | ringidcl 19997 |
. . . . . . . . . . . 12
β’ (πΉ β Ring β
(1rβπΉ)
β πΎ) |
51 | 6, 50 | syl 17 |
. . . . . . . . . . 11
β’ (π β (1rβπΉ) β πΎ) |
52 | 31, 51 | sseldd 3949 |
. . . . . . . . . 10
β’ (π β (1rβπΉ) β
β) |
53 | 52 | sqvald 14057 |
. . . . . . . . 9
β’ (π β
((1rβπΉ)β2) = ((1rβπΉ) Β·
(1rβπΉ))) |
54 | 25 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π β (1rβπΉ) =
(1rβ(βfld βΎs πΎ))) |
55 | 54 | oveq1d 7376 |
. . . . . . . . 9
β’ (π β
((1rβπΉ)
Β· (1rβπΉ)) =
((1rβ(βfld βΎs πΎ)) Β·
(1rβπΉ))) |
56 | 25 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π β (BaseβπΉ) =
(Baseβ(βfld βΎs πΎ))) |
57 | 2, 56 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (π β πΎ = (Baseβ(βfld
βΎs πΎ))) |
58 | 51, 57 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (π β (1rβπΉ) β
(Baseβ(βfld βΎs πΎ))) |
59 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβ(βfld βΎs πΎ)) = (Baseβ(βfld
βΎs πΎ)) |
60 | 2 | fvexi 6860 |
. . . . . . . . . . . 12
β’ πΎ β V |
61 | | cnfldmul 20825 |
. . . . . . . . . . . . 13
β’ Β·
= (.rββfld) |
62 | 43, 61 | ressmulr 17196 |
. . . . . . . . . . . 12
β’ (πΎ β V β Β· =
(.rβ(βfld βΎs πΎ))) |
63 | 60, 62 | ax-mp 5 |
. . . . . . . . . . 11
β’ Β·
= (.rβ(βfld βΎs πΎ)) |
64 | | eqid 2733 |
. . . . . . . . . . 11
β’
(1rβ(βfld βΎs πΎ)) =
(1rβ(βfld βΎs πΎ)) |
65 | 59, 63, 64 | ringlidm 20000 |
. . . . . . . . . 10
β’
(((βfld βΎs πΎ) β Ring β§
(1rβπΉ)
β (Baseβ(βfld βΎs πΎ))) β
((1rβ(βfld βΎs πΎ)) Β·
(1rβπΉ)) =
(1rβπΉ)) |
66 | 26, 58, 65 | syl2anc 585 |
. . . . . . . . 9
β’ (π β
((1rβ(βfld βΎs πΎ)) Β·
(1rβπΉ)) =
(1rβπΉ)) |
67 | 53, 55, 66 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β
((1rβπΉ)β2) = (1rβπΉ)) |
68 | | sq01 14137 |
. . . . . . . . 9
β’
((1rβπΉ) β β β
(((1rβπΉ)β2) = (1rβπΉ) β
((1rβπΉ) =
0 β¨ (1rβπΉ) = 1))) |
69 | 52, 68 | syl 17 |
. . . . . . . 8
β’ (π β
(((1rβπΉ)β2) = (1rβπΉ) β
((1rβπΉ) =
0 β¨ (1rβπΉ) = 1))) |
70 | 67, 69 | mpbid 231 |
. . . . . . 7
β’ (π β
((1rβπΉ) =
0 β¨ (1rβπΉ) = 1)) |
71 | 70 | ord 863 |
. . . . . 6
β’ (π β (Β¬
(1rβπΉ) = 0
β (1rβπΉ) = 1)) |
72 | 49, 71 | mpd 15 |
. . . . 5
β’ (π β (1rβπΉ) = 1) |
73 | 72, 51 | eqeltrrd 2835 |
. . . 4
β’ (π β 1 β πΎ) |
74 | 31, 73 | jca 513 |
. . 3
β’ (π β (πΎ β β β§ 1 β πΎ)) |
75 | | cnfld1 20845 |
. . . 4
β’ 1 =
(1rββfld) |
76 | 16, 75 | issubrg 20264 |
. . 3
β’ (πΎ β
(SubRingββfld) β ((βfld β
Ring β§ (βfld βΎs πΎ) β Ring) β§ (πΎ β β β§ 1 β πΎ))) |
77 | 28, 74, 76 | sylanbrc 584 |
. 2
β’ (π β πΎ β
(SubRingββfld)) |
78 | 25, 20, 77 | 3jca 1129 |
1
β’ (π β (πΉ = (βfld
βΎs πΎ)
β§ πΎ = (π΄ β© β) β§ πΎ β
(SubRingββfld))) |