Step | Hyp | Ref
| Expression |
1 | | primefld.1 |
. . 3
⊢ 𝑃 = (𝑅 ↾s ∩ (SubDRing‘𝑅)) |
2 | | id 22 |
. . 3
⊢ (𝑅 ∈ DivRing → 𝑅 ∈
DivRing) |
3 | | issdrg 19686 |
. . . . . 6
⊢ (𝑠 ∈ (SubDRing‘𝑅) ↔ (𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubRing‘𝑅) ∧ (𝑅 ↾s 𝑠) ∈ DivRing)) |
4 | 3 | simp2bi 1147 |
. . . . 5
⊢ (𝑠 ∈ (SubDRing‘𝑅) → 𝑠 ∈ (SubRing‘𝑅)) |
5 | 4 | ssriv 3879 |
. . . 4
⊢
(SubDRing‘𝑅)
⊆ (SubRing‘𝑅) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) ⊆
(SubRing‘𝑅)) |
7 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑅) =
(Base‘𝑅) |
8 | 7 | sdrgid 19687 |
. . . 4
⊢ (𝑅 ∈ DivRing →
(Base‘𝑅) ∈
(SubDRing‘𝑅)) |
9 | 8 | ne0d 4222 |
. . 3
⊢ (𝑅 ∈ DivRing →
(SubDRing‘𝑅) ≠
∅) |
10 | 3 | simp3bi 1148 |
. . . 4
⊢ (𝑠 ∈ (SubDRing‘𝑅) → (𝑅 ↾s 𝑠) ∈ DivRing) |
11 | 10 | adantl 485 |
. . 3
⊢ ((𝑅 ∈ DivRing ∧ 𝑠 ∈ (SubDRing‘𝑅)) → (𝑅 ↾s 𝑠) ∈ DivRing) |
12 | 1, 2, 6, 9, 11 | subdrgint 19694 |
. 2
⊢ (𝑅 ∈ DivRing → 𝑃 ∈
DivRing) |
13 | | drngring 19621 |
. . . 4
⊢ (𝑃 ∈ DivRing → 𝑃 ∈ Ring) |
14 | 12, 13 | syl 17 |
. . 3
⊢ (𝑅 ∈ DivRing → 𝑃 ∈ Ring) |
15 | | ssidd 3898 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ DivRing →
(Base‘𝑅) ⊆
(Base‘𝑅)) |
16 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
17 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(Cntz‘(mulGrp‘𝑅)) = (Cntz‘(mulGrp‘𝑅)) |
18 | 7, 16, 17 | cntzsdrg 19693 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ DivRing ∧
(Base‘𝑅) ⊆
(Base‘𝑅)) →
((Cntz‘(mulGrp‘𝑅))‘(Base‘𝑅)) ∈ (SubDRing‘𝑅)) |
19 | 2, 15, 18 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ DivRing →
((Cntz‘(mulGrp‘𝑅))‘(Base‘𝑅)) ∈ (SubDRing‘𝑅)) |
20 | | intss1 4848 |
. . . . . . . . . . . . 13
⊢
(((Cntz‘(mulGrp‘𝑅))‘(Base‘𝑅)) ∈ (SubDRing‘𝑅) → ∩
(SubDRing‘𝑅) ⊆
((Cntz‘(mulGrp‘𝑅))‘(Base‘𝑅))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ DivRing → ∩ (SubDRing‘𝑅) ⊆ ((Cntz‘(mulGrp‘𝑅))‘(Base‘𝑅))) |
22 | 16, 7 | mgpbas 19357 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
23 | 22, 17 | cntrval 18560 |
. . . . . . . . . . . 12
⊢
((Cntz‘(mulGrp‘𝑅))‘(Base‘𝑅)) = (Cntr‘(mulGrp‘𝑅)) |
24 | 21, 23 | sseqtrdi 3925 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ DivRing → ∩ (SubDRing‘𝑅) ⊆ (Cntr‘(mulGrp‘𝑅))) |
25 | 22 | cntrss 18571 |
. . . . . . . . . . 11
⊢
(Cntr‘(mulGrp‘𝑅)) ⊆ (Base‘𝑅) |
26 | 24, 25 | sstrdi 3887 |
. . . . . . . . . 10
⊢ (𝑅 ∈ DivRing → ∩ (SubDRing‘𝑅) ⊆ (Base‘𝑅)) |
27 | 1, 7 | ressbas2 16651 |
. . . . . . . . . 10
⊢ (∩ (SubDRing‘𝑅) ⊆ (Base‘𝑅) → ∩
(SubDRing‘𝑅) =
(Base‘𝑃)) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ DivRing → ∩ (SubDRing‘𝑅) = (Base‘𝑃)) |
29 | 28, 24 | eqsstrrd 3914 |
. . . . . . . 8
⊢ (𝑅 ∈ DivRing →
(Base‘𝑃) ⊆
(Cntr‘(mulGrp‘𝑅))) |
30 | 29 | adantr 484 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (Base‘𝑃) ⊆ (Cntr‘(mulGrp‘𝑅))) |
31 | | simprl 771 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → 𝑥 ∈ (Base‘𝑃)) |
32 | 30, 31 | sseldd 3876 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → 𝑥 ∈ (Cntr‘(mulGrp‘𝑅))) |
33 | 28, 26 | eqsstrrd 3914 |
. . . . . . . 8
⊢ (𝑅 ∈ DivRing →
(Base‘𝑃) ⊆
(Base‘𝑅)) |
34 | 33 | adantr 484 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (Base‘𝑃) ⊆ (Base‘𝑅)) |
35 | | simprr 773 |
. . . . . . 7
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → 𝑦 ∈ (Base‘𝑃)) |
36 | 34, 35 | sseldd 3876 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → 𝑦 ∈ (Base‘𝑅)) |
37 | | eqid 2738 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
38 | 16, 37 | mgpplusg 19355 |
. . . . . . 7
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
39 | | eqid 2738 |
. . . . . . 7
⊢
(Cntr‘(mulGrp‘𝑅)) = (Cntr‘(mulGrp‘𝑅)) |
40 | 22, 38, 39 | cntri 18572 |
. . . . . 6
⊢ ((𝑥 ∈
(Cntr‘(mulGrp‘𝑅)) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑥)) |
41 | 32, 36, 40 | syl2anc 587 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (𝑥(.r‘𝑅)𝑦) = (𝑦(.r‘𝑅)𝑥)) |
42 | 8, 26 | ssexd 5189 |
. . . . . . 7
⊢ (𝑅 ∈ DivRing → ∩ (SubDRing‘𝑅) ∈ V) |
43 | 1, 37 | ressmulr 16721 |
. . . . . . 7
⊢ (∩ (SubDRing‘𝑅) ∈ V → (.r‘𝑅) = (.r‘𝑃)) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ DivRing →
(.r‘𝑅) =
(.r‘𝑃)) |
45 | 44 | oveqdr 7192 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (𝑥(.r‘𝑅)𝑦) = (𝑥(.r‘𝑃)𝑦)) |
46 | 44 | oveqdr 7192 |
. . . . 5
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (𝑦(.r‘𝑅)𝑥) = (𝑦(.r‘𝑃)𝑥)) |
47 | 41, 45, 46 | 3eqtr3d 2781 |
. . . 4
⊢ ((𝑅 ∈ DivRing ∧ (𝑥 ∈ (Base‘𝑃) ∧ 𝑦 ∈ (Base‘𝑃))) → (𝑥(.r‘𝑃)𝑦) = (𝑦(.r‘𝑃)𝑥)) |
48 | 47 | ralrimivva 3103 |
. . 3
⊢ (𝑅 ∈ DivRing →
∀𝑥 ∈
(Base‘𝑃)∀𝑦 ∈ (Base‘𝑃)(𝑥(.r‘𝑃)𝑦) = (𝑦(.r‘𝑃)𝑥)) |
49 | | eqid 2738 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
50 | | eqid 2738 |
. . . 4
⊢
(.r‘𝑃) = (.r‘𝑃) |
51 | 49, 50 | iscrng2 19428 |
. . 3
⊢ (𝑃 ∈ CRing ↔ (𝑃 ∈ Ring ∧ ∀𝑥 ∈ (Base‘𝑃)∀𝑦 ∈ (Base‘𝑃)(𝑥(.r‘𝑃)𝑦) = (𝑦(.r‘𝑃)𝑥))) |
52 | 14, 48, 51 | sylanbrc 586 |
. 2
⊢ (𝑅 ∈ DivRing → 𝑃 ∈ CRing) |
53 | | isfld 19623 |
. 2
⊢ (𝑃 ∈ Field ↔ (𝑃 ∈ DivRing ∧ 𝑃 ∈ CRing)) |
54 | 12, 52, 53 | sylanbrc 586 |
1
⊢ (𝑅 ∈ DivRing → 𝑃 ∈ Field) |