Metamath Proof Explorer

Theorem primefld

Description: The smallest sub division ring of a division ring, here named P , is a field, called thePrime Field of R . (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Hypothesis primefld.1 ⊢ 𝑃 = ( 𝑅 ↾s ∩ ( SubDRing ‘ 𝑅 ) )
Assertion primefld ( 𝑅 ∈ DivRing → 𝑃 ∈ Field )

Proof

Step Hyp Ref Expression
1 primefld.1 ⊢ 𝑃 = ( 𝑅 ↾s ∩ ( SubDRing ‘ 𝑅 ) )
2 id ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ DivRing )
3 issdrg ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑠 ) ∈ DivRing ) )
4 3 simp2bi ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → 𝑠 ∈ ( SubRing ‘ 𝑅 ) )
5 4 ssriv ⊢ ( SubDRing ‘ 𝑅 ) ⊆ ( SubRing ‘ 𝑅 )
6 5 a1i ⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) ⊆ ( SubRing ‘ 𝑅 ) )
7 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8 7 sdrgid ⊢ ( 𝑅 ∈ DivRing → ( Base ‘ 𝑅 ) ∈ ( SubDRing ‘ 𝑅 ) )
9 8 ne0d ⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) ≠ ∅ )
10 3 simp3bi ⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑠 ) ∈ DivRing )
11 10 adantl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑠 ) ∈ DivRing )
12 1 2 6 9 11 subdrgint ⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ DivRing )
13 drngring ⊢ ( 𝑃 ∈ DivRing → 𝑃 ∈ Ring )
14 12 13 syl ⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ Ring )
15 ssidd ⊢ ( 𝑅 ∈ DivRing → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
16 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
17 eqid ⊢ ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) = ( Cntz ‘ ( mulGrp ‘ 𝑅 ) )
18 7 16 17 cntzsdrg ⊢ ( ( 𝑅 ∈ DivRing ∧ ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) ) → ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) ∈ ( SubDRing ‘ 𝑅 ) )
19 2 15 18 syl2anc ⊢ ( 𝑅 ∈ DivRing → ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) ∈ ( SubDRing ‘ 𝑅 ) )
20 intss1 ⊢ ( ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) ∈ ( SubDRing ‘ 𝑅 ) → ∩ ( SubDRing ‘ 𝑅 ) ⊆ ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) )
21 19 20 syl ⊢ ( 𝑅 ∈ DivRing → ∩ ( SubDRing ‘ 𝑅 ) ⊆ ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) )
22 16 7 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
23 22 17 cntrval ⊢ ( ( Cntz ‘ ( mulGrp ‘ 𝑅 ) ) ‘ ( Base ‘ 𝑅 ) ) = ( Cntr ‘ ( mulGrp ‘ 𝑅 ) )
24 21 23 sseqtrdi ⊢ ( 𝑅 ∈ DivRing → ∩ ( SubDRing ‘ 𝑅 ) ⊆ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) )
25 22 cntrss ⊢ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ⊆ ( Base ‘ 𝑅 )
26 24 25 sstrdi ⊢ ( 𝑅 ∈ DivRing → ∩ ( SubDRing ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
27 1 7 ressbas2 ⊢ ( ∩ ( SubDRing ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) → ∩ ( SubDRing ‘ 𝑅 ) = ( Base ‘ 𝑃 ) )
28 26 27 syl ⊢ ( 𝑅 ∈ DivRing → ∩ ( SubDRing ‘ 𝑅 ) = ( Base ‘ 𝑃 ) )
29 28 24 eqsstrrd ⊢ ( 𝑅 ∈ DivRing → ( Base ‘ 𝑃 ) ⊆ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) )
30 29 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( Base ‘ 𝑃 ) ⊆ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) )
31 simprl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
32 30 31 sseldd ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑥 ∈ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) )
33 28 26 eqsstrrd ⊢ ( 𝑅 ∈ DivRing → ( Base ‘ 𝑃 ) ⊆ ( Base ‘ 𝑅 ) )
34 33 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( Base ‘ 𝑃 ) ⊆ ( Base ‘ 𝑅 ) )
35 simprr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑃 ) )
36 34 35 sseldd ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
37 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
38 16 37 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
39 eqid ⊢ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) = ( Cntr ‘ ( mulGrp ‘ 𝑅 ) )
40 22 38 39 cntri ⊢ ( ( 𝑥 ∈ ( Cntr ‘ ( mulGrp ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
41 32 36 40 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
42 8 26 ssexd ⊢ ( 𝑅 ∈ DivRing → ∩ ( SubDRing ‘ 𝑅 ) ∈ V )
43 1 37 ressmulr ⊢ ( ∩ ( SubDRing ‘ 𝑅 ) ∈ V → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑃 ) )
44 42 43 syl ⊢ ( 𝑅 ∈ DivRing → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑃 ) )
45 44 oveqdr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) )
46 44 oveqdr ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑦 ( .r ‘ 𝑃 ) 𝑥 ) )
47 41 45 46 3eqtr3d ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑃 ) 𝑥 ) )
48 47 ralrimivva ⊢ ( 𝑅 ∈ DivRing → ∀ 𝑥 ∈ ( Base ‘ 𝑃 ) ∀ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑃 ) 𝑥 ) )
49 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
50 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
51 49 50 iscrng2 ⊢ ( 𝑃 ∈ CRing ↔ ( 𝑃 ∈ Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑃 ) ∀ 𝑦 ∈ ( Base ‘ 𝑃 ) ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑃 ) 𝑥 ) ) )
52 14 48 51 sylanbrc ⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ CRing )
53 isfld ⊢ ( 𝑃 ∈ Field ↔ ( 𝑃 ∈ DivRing ∧ 𝑃 ∈ CRing ) )
54 12 52 53 sylanbrc ⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ Field )