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	$⊢ P = R ↾_{𝑠} ⋂ SubDRing (R)$
	Assertion	primefld	$⊢ R \in DivRing \to P \in Field$

Proof

Step	Hyp	Ref	Expression
1		primefld.1	$⊢ P = R ↾_{𝑠} ⋂ SubDRing (R)$
2		id	$⊢ R \in DivRing \to R \in DivRing$
3		issdrg	$⊢ s \in SubDRing (R) \leftrightarrow (R \in DivRing \land s \in SubRing (R) \land R ↾_{𝑠} s \in DivRing)$
4	3	simp2bi	$⊢ s \in SubDRing (R) \to s \in SubRing (R)$
5	4	ssriv	$⊢ SubDRing (R) \subseteq SubRing (R)$
6	5	a1i	$⊢ R \in DivRing \to SubDRing (R) \subseteq SubRing (R)$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	7	sdrgid	$⊢ R \in DivRing \to {Base}_{R} \in SubDRing (R)$
9	8	ne0d	$⊢ R \in DivRing \to SubDRing (R) \neq \emptyset$
10	3	simp3bi	$⊢ s \in SubDRing (R) \to R ↾_{𝑠} s \in DivRing$
11	10	adantl	$⊢ (R \in DivRing \land s \in SubDRing (R)) \to R ↾_{𝑠} s \in DivRing$
12	1 2 6 9 11	subdrgint	$⊢ R \in DivRing \to P \in DivRing$
13		drngring	$⊢ P \in DivRing \to P \in Ring$
14	12 13	syl	$⊢ R \in DivRing \to P \in Ring$
15		ssidd	$⊢ R \in DivRing \to {Base}_{R} \subseteq {Base}_{R}$
16		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
17		eqid	$⊢ Cntz ({mulGrp}_{R}) = Cntz ({mulGrp}_{R})$
18	7 16 17	cntzsdrg	$⊢ (R \in DivRing \land {Base}_{R} \subseteq {Base}_{R}) \to Cntz ({mulGrp}_{R}) ({Base}_{R}) \in SubDRing (R)$
19	2 15 18	syl2anc	$⊢ R \in DivRing \to Cntz ({mulGrp}_{R}) ({Base}_{R}) \in SubDRing (R)$
20		intss1	$⊢ Cntz ({mulGrp}_{R}) ({Base}_{R}) \in SubDRing (R) \to ⋂ SubDRing (R) \subseteq Cntz ({mulGrp}_{R}) ({Base}_{R})$
21	19 20	syl	$⊢ R \in DivRing \to ⋂ SubDRing (R) \subseteq Cntz ({mulGrp}_{R}) ({Base}_{R})$
22	16 7	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
23	22 17	cntrval	$⊢ Cntz ({mulGrp}_{R}) ({Base}_{R}) = Cntr ({mulGrp}_{R})$
24	21 23	sseqtrdi	$⊢ R \in DivRing \to ⋂ SubDRing (R) \subseteq Cntr ({mulGrp}_{R})$
25	22	cntrss	$⊢ Cntr ({mulGrp}_{R}) \subseteq {Base}_{R}$
26	24 25	sstrdi	$⊢ R \in DivRing \to ⋂ SubDRing (R) \subseteq {Base}_{R}$
27	1 7	ressbas2	$⊢ ⋂ SubDRing (R) \subseteq {Base}_{R} \to ⋂ SubDRing (R) = {Base}_{P}$
28	26 27	syl	$⊢ R \in DivRing \to ⋂ SubDRing (R) = {Base}_{P}$
29	28 24	eqsstrrd	$⊢ R \in DivRing \to {Base}_{P} \subseteq Cntr ({mulGrp}_{R})$
30	29	adantr	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to {Base}_{P} \subseteq Cntr ({mulGrp}_{R})$
31		simprl	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x \in {Base}_{P}$
32	30 31	sseldd	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x \in Cntr ({mulGrp}_{R})$
33	28 26	eqsstrrd	$⊢ R \in DivRing \to {Base}_{P} \subseteq {Base}_{R}$
34	33	adantr	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to {Base}_{P} \subseteq {Base}_{R}$
35		simprr	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to y \in {Base}_{P}$
36	34 35	sseldd	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to y \in {Base}_{R}$
37		eqid	$⊢ \cdot_{R} = \cdot_{R}$
38	16 37	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
39		eqid	$⊢ Cntr ({mulGrp}_{R}) = Cntr ({mulGrp}_{R})$
40	22 38 39	cntri	$⊢ (x \in Cntr ({mulGrp}_{R}) \land y \in {Base}_{R}) \to x \cdot_{R} y = y \cdot_{R} x$
41	32 36 40	syl2anc	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x \cdot_{R} y = y \cdot_{R} x$
42	8 26	ssexd	$⊢ R \in DivRing \to ⋂ SubDRing (R) \in V$
43	1 37	ressmulr	$⊢ ⋂ SubDRing (R) \in V \to \cdot_{R} = \cdot_{P}$
44	42 43	syl	$⊢ R \in DivRing \to \cdot_{R} = \cdot_{P}$
45	44	oveqdr	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x \cdot_{R} y = x \cdot_{P} y$
46	44	oveqdr	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to y \cdot_{R} x = y \cdot_{P} x$
47	41 45 46	3eqtr3d	$⊢ (R \in DivRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x \cdot_{P} y = y \cdot_{P} x$
48	47	ralrimivva	$⊢ R \in DivRing \to \forall x \in {Base}_{P} \forall y \in {Base}_{P} x \cdot_{P} y = y \cdot_{P} x$
49		eqid	$⊢ {Base}_{P} = {Base}_{P}$
50		eqid	$⊢ \cdot_{P} = \cdot_{P}$
51	49 50	iscrng2	$⊢ P \in CRing \leftrightarrow (P \in Ring \land \forall x \in {Base}_{P} \forall y \in {Base}_{P} x \cdot_{P} y = y \cdot_{P} x)$
52	14 48 51	sylanbrc	$⊢ R \in DivRing \to P \in CRing$
53		isfld	$⊢ P \in Field \leftrightarrow (P \in DivRing \land P \in CRing)$
54	12 52 53	sylanbrc	$⊢ R \in DivRing \to P \in Field$

Metamath Proof Explorer

Theorem primefld

Proof