cntzsdrg

Description: Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	cntzsdrg.b	$⊢ B = {Base}_{R}$
	cntzsdrg.m	$⊢ M = {mulGrp}_{R}$
	cntzsdrg.z	$⊢ Z = Cntz (M)$
Assertion	cntzsdrg	$⊢ (R \in DivRing \land S \subseteq B) \to Z (S) \in SubDRing (R)$

Proof

Step	Hyp	Ref	Expression
1		cntzsdrg.b	$⊢ B = {Base}_{R}$
2		cntzsdrg.m	$⊢ M = {mulGrp}_{R}$
3		cntzsdrg.z	$⊢ Z = Cntz (M)$
4		simpl	$⊢ (R \in DivRing \land S \subseteq B) \to R \in DivRing$
5		drngring	$⊢ R \in DivRing \to R \in Ring$
6	1 2 3	cntzsubr	$⊢ (R \in Ring \land S \subseteq B) \to Z (S) \in SubRing (R)$
7	5 6	sylan	$⊢ (R \in DivRing \land S \subseteq B) \to Z (S) \in SubRing (R)$
8		oveq2	$⊢ y = 0_{R} \to {inv}_{r} (R) (x) \cdot_{R} y = {inv}_{r} (R) (x) \cdot_{R} 0_{R}$
9		oveq1	$⊢ y = 0_{R} \to y \cdot_{R} {inv}_{r} (R) (x) = 0_{R} \cdot_{R} {inv}_{r} (R) (x)$
10	8 9	eqeq12d	$⊢ y = 0_{R} \to ({inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x) \leftrightarrow {inv}_{r} (R) (x) \cdot_{R} 0_{R} = 0_{R} \cdot_{R} {inv}_{r} (R) (x))$
11		eldifsn	$⊢ y \in (S ∖ \{0_{R}\}) \leftrightarrow (y \in S \land y \neq 0_{R})$
12		eqid	$⊢ Unit (R) = Unit (R)$
13	2	oveq1i	$⊢ M ↾_{𝑠} Unit (R) = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
14		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
15	12 13 14	invrfval	$⊢ {inv}_{r} (R) = {inv}_{g} (M ↾_{𝑠} Unit (R))$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	1 12 16	isdrng	$⊢ R \in DivRing \leftrightarrow (R \in Ring \land Unit (R) = B ∖ \{0_{R}\})$
18	17	simprbi	$⊢ R \in DivRing \to Unit (R) = B ∖ \{0_{R}\}$
19	18	oveq2d	$⊢ R \in DivRing \to M ↾_{𝑠} Unit (R) = M ↾_{𝑠} (B ∖ \{0_{R}\})$
20	19	fveq2d	$⊢ R \in DivRing \to {inv}_{g} (M ↾_{𝑠} Unit (R)) = {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\}))$
21	15 20	eqtrid	$⊢ R \in DivRing \to {inv}_{r} (R) = {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\}))$
22	21	ad2antrr	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to {inv}_{r} (R) = {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\}))$
23	22	fveq1d	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to {inv}_{r} (R) (x) = {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\})) (x)$
24	2	oveq1i	$⊢ M ↾_{𝑠} (B ∖ \{0_{R}\}) = {mulGrp}_{R} ↾_{𝑠} (B ∖ \{0_{R}\})$
25	1 16 24	drngmgp	$⊢ R \in DivRing \to M ↾_{𝑠} (B ∖ \{0_{R}\}) \in Grp$
26	25	ad2antrr	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to M ↾_{𝑠} (B ∖ \{0_{R}\}) \in Grp$
27		ssdif	$⊢ S \subseteq B \to S ∖ \{0_{R}\} \subseteq B ∖ \{0_{R}\}$
28	27	ad2antlr	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to S ∖ \{0_{R}\} \subseteq B ∖ \{0_{R}\}$
29		difss	$⊢ B ∖ \{0_{R}\} \subseteq B$
30		eqid	$⊢ M ↾_{𝑠} (B ∖ \{0_{R}\}) = M ↾_{𝑠} (B ∖ \{0_{R}\})$
31	2 1	mgpbas	$⊢ B = {Base}_{M}$
32	30 31	ressbas2	$⊢ B ∖ \{0_{R}\} \subseteq B \to B ∖ \{0_{R}\} = {Base}_{(M ↾_{𝑠} (B ∖ \{0_{R}\}))}$
33	29 32	ax-mp	$⊢ B ∖ \{0_{R}\} = {Base}_{(M ↾_{𝑠} (B ∖ \{0_{R}\}))}$
34		eqid	$⊢ Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) = Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\}))$
35	33 34	cntzsubg	$⊢ (M ↾_{𝑠} (B ∖ \{0_{R}\}) \in Grp \land S ∖ \{0_{R}\} \subseteq B ∖ \{0_{R}\}) \to Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\}) \in SubGrp (M ↾_{𝑠} (B ∖ \{0_{R}\}))$
36	26 28 35	syl2anc	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\}) \in SubGrp (M ↾_{𝑠} (B ∖ \{0_{R}\}))$
37		simpr	$⊢ (R \in DivRing \land S \subseteq B) \to S \subseteq B$
38		difss	$⊢ S ∖ \{0_{R}\} \subseteq S$
39	31 3	cntz2ss	$⊢ (S \subseteq B \land S ∖ \{0_{R}\} \subseteq S) \to Z (S) \subseteq Z (S ∖ \{0_{R}\})$
40	37 38 39	sylancl	$⊢ (R \in DivRing \land S \subseteq B) \to Z (S) \subseteq Z (S ∖ \{0_{R}\})$
41	40	ssdifssd	$⊢ (R \in DivRing \land S \subseteq B) \to Z (S) ∖ \{0_{R}\} \subseteq Z (S ∖ \{0_{R}\})$
42	41	sselda	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to x \in Z (S ∖ \{0_{R}\})$
43	31 3	cntzssv	$⊢ Z (S) \subseteq B$
44		ssdif	$⊢ Z (S) \subseteq B \to Z (S) ∖ \{0_{R}\} \subseteq B ∖ \{0_{R}\}$
45	43 44	mp1i	$⊢ (R \in DivRing \land S \subseteq B) \to Z (S) ∖ \{0_{R}\} \subseteq B ∖ \{0_{R}\}$
46	45	sselda	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to x \in (B ∖ \{0_{R}\})$
47	42 46	elind	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to x \in (Z (S ∖ \{0_{R}\}) \cap (B ∖ \{0_{R}\}))$
48	1	fvexi	$⊢ B \in V$
49	48	difexi	$⊢ B ∖ \{0_{R}\} \in V$
50	30 3 34	resscntz	$⊢ (B ∖ \{0_{R}\} \in V \land S ∖ \{0_{R}\} \subseteq B ∖ \{0_{R}\}) \to Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\}) = Z (S ∖ \{0_{R}\}) \cap (B ∖ \{0_{R}\})$
51	49 28 50	sylancr	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\}) = Z (S ∖ \{0_{R}\}) \cap (B ∖ \{0_{R}\})$
52	47 51	eleqtrrd	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to x \in Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\})$
53		eqid	$⊢ {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\})) = {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\}))$
54	53	subginvcl	$⊢ (Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\}) \in SubGrp (M ↾_{𝑠} (B ∖ \{0_{R}\})) \land x \in Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\})) \to {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\})) (x) \in Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\})$
55	36 52 54	syl2anc	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to {inv}_{g} (M ↾_{𝑠} (B ∖ \{0_{R}\})) (x) \in Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\})$
56	23 55	eqeltrd	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to {inv}_{r} (R) (x) \in Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\})$
57		eqid	$⊢ \cdot_{R} = \cdot_{R}$
58	2 57	mgpplusg	$⊢ \cdot_{R} = +_{M}$
59	30 58	ressplusg	$⊢ B ∖ \{0_{R}\} \in V \to \cdot_{R} = +_{(M ↾_{𝑠} (B ∖ \{0_{R}\}))}$
60	49 59	ax-mp	$⊢ \cdot_{R} = +_{(M ↾_{𝑠} (B ∖ \{0_{R}\}))}$
61	60 34	cntzi	$⊢ ({inv}_{r} (R) (x) \in Cntz (M ↾_{𝑠} (B ∖ \{0_{R}\})) (S ∖ \{0_{R}\}) \land y \in (S ∖ \{0_{R}\})) \to {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x)$
62	56 61	sylan	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in (S ∖ \{0_{R}\})) \to {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x)$
63	11 62	sylan2br	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land (y \in S \land y \neq 0_{R})) \to {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x)$
64	63	anassrs	$⊢ ((((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in S) \land y \neq 0_{R}) \to {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x)$
65	5	ad3antrrr	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in S) \to R \in Ring$
66	4	adantr	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to R \in DivRing$
67		eldifi	$⊢ x \in (Z (S) ∖ \{0_{R}\}) \to x \in Z (S)$
68	67	adantl	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to x \in Z (S)$
69	43 68	sselid	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to x \in B$
70		eldifsni	$⊢ x \in (Z (S) ∖ \{0_{R}\}) \to x \neq 0_{R}$
71	70	adantl	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to x \neq 0_{R}$
72	1 16 14	drnginvrcl	$⊢ (R \in DivRing \land x \in B \land x \neq 0_{R}) \to {inv}_{r} (R) (x) \in B$
73	66 69 71 72	syl3anc	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to {inv}_{r} (R) (x) \in B$
74	73	adantr	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in S) \to {inv}_{r} (R) (x) \in B$
75	1 57 16	ringrz	$⊢ (R \in Ring \land {inv}_{r} (R) (x) \in B) \to {inv}_{r} (R) (x) \cdot_{R} 0_{R} = 0_{R}$
76	65 74 75	syl2anc	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in S) \to {inv}_{r} (R) (x) \cdot_{R} 0_{R} = 0_{R}$
77	1 57 16	ringlz	$⊢ (R \in Ring \land {inv}_{r} (R) (x) \in B) \to 0_{R} \cdot_{R} {inv}_{r} (R) (x) = 0_{R}$
78	65 74 77	syl2anc	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in S) \to 0_{R} \cdot_{R} {inv}_{r} (R) (x) = 0_{R}$
79	76 78	eqtr4d	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in S) \to {inv}_{r} (R) (x) \cdot_{R} 0_{R} = 0_{R} \cdot_{R} {inv}_{r} (R) (x)$
80	10 64 79	pm2.61ne	$⊢ (((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \land y \in S) \to {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x)$
81	80	ralrimiva	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to \forall y \in S {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x)$
82		simplr	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to S \subseteq B$
83	31 58 3	cntzel	$⊢ (S \subseteq B \land {inv}_{r} (R) (x) \in B) \to ({inv}_{r} (R) (x) \in Z (S) \leftrightarrow \forall y \in S {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x))$
84	82 73 83	syl2anc	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to ({inv}_{r} (R) (x) \in Z (S) \leftrightarrow \forall y \in S {inv}_{r} (R) (x) \cdot_{R} y = y \cdot_{R} {inv}_{r} (R) (x))$
85	81 84	mpbird	$⊢ ((R \in DivRing \land S \subseteq B) \land x \in (Z (S) ∖ \{0_{R}\})) \to {inv}_{r} (R) (x) \in Z (S)$
86	85	ralrimiva	$⊢ (R \in DivRing \land S \subseteq B) \to \forall x \in (Z (S) ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in Z (S)$
87	14 16	issdrg2	$⊢ Z (S) \in SubDRing (R) \leftrightarrow (R \in DivRing \land Z (S) \in SubRing (R) \land \forall x \in (Z (S) ∖ \{0_{R}\}) {inv}_{r} (R) (x) \in Z (S))$
88	4 7 86 87	syl3anbrc	$⊢ (R \in DivRing \land S \subseteq B) \to Z (S) \in SubDRing (R)$

Metamath Proof Explorer

Theorem cntzsdrg

Proof