cntzsubr

Description: Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cntzsubr.b	$⊢ B = {Base}_{R}$
2		cntzsubr.m	$⊢ M = {mulGrp}_{R}$
3		cntzsubr.z	$⊢ Z = Cntz (M)$
4	2 1	mgpbas	$⊢ B = {Base}_{M}$
5	4 3	cntzssv	$⊢ Z (S) \subseteq B$
6	5	a1i	$⊢ (R \in Ring \land S \subseteq B) \to Z (S) \subseteq B$
7		simpll	$⊢ ((R \in Ring \land S \subseteq B) \land z \in S) \to R \in Ring$
8		ssel2	$⊢ (S \subseteq B \land z \in S) \to z \in B$
9	8	adantll	$⊢ ((R \in Ring \land S \subseteq B) \land z \in S) \to z \in B$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11		eqid	$⊢ 0_{R} = 0_{R}$
12	1 10 11	ringlz	$⊢ (R \in Ring \land z \in B) \to 0_{R} \cdot_{R} z = 0_{R}$
13	7 9 12	syl2anc	$⊢ ((R \in Ring \land S \subseteq B) \land z \in S) \to 0_{R} \cdot_{R} z = 0_{R}$
14	1 10 11	ringrz	$⊢ (R \in Ring \land z \in B) \to z \cdot_{R} 0_{R} = 0_{R}$
15	7 9 14	syl2anc	$⊢ ((R \in Ring \land S \subseteq B) \land z \in S) \to z \cdot_{R} 0_{R} = 0_{R}$
16	13 15	eqtr4d	$⊢ ((R \in Ring \land S \subseteq B) \land z \in S) \to 0_{R} \cdot_{R} z = z \cdot_{R} 0_{R}$
17	16	ralrimiva	$⊢ (R \in Ring \land S \subseteq B) \to \forall z \in S 0_{R} \cdot_{R} z = z \cdot_{R} 0_{R}$
18		simpr	$⊢ (R \in Ring \land S \subseteq B) \to S \subseteq B$
19	1 11	ring0cl	$⊢ R \in Ring \to 0_{R} \in B$
20	19	adantr	$⊢ (R \in Ring \land S \subseteq B) \to 0_{R} \in B$
21	2 10	mgpplusg	$⊢ \cdot_{R} = +_{M}$
22	4 21 3	cntzel	$⊢ (S \subseteq B \land 0_{R} \in B) \to (0_{R} \in Z (S) \leftrightarrow \forall z \in S 0_{R} \cdot_{R} z = z \cdot_{R} 0_{R})$
23	18 20 22	syl2anc	$⊢ (R \in Ring \land S \subseteq B) \to (0_{R} \in Z (S) \leftrightarrow \forall z \in S 0_{R} \cdot_{R} z = z \cdot_{R} 0_{R})$
24	17 23	mpbird	$⊢ (R \in Ring \land S \subseteq B) \to 0_{R} \in Z (S)$
25	24	ne0d	$⊢ (R \in Ring \land S \subseteq B) \to Z (S) \neq \emptyset$
26		simpl2	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to x \in Z (S)$
27		simpr	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to z \in S$
28	21 3	cntzi	$⊢ (x \in Z (S) \land z \in S) \to x \cdot_{R} z = z \cdot_{R} x$
29	26 27 28	syl2anc	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to x \cdot_{R} z = z \cdot_{R} x$
30		simpl3	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to y \in Z (S)$
31	21 3	cntzi	$⊢ (y \in Z (S) \land z \in S) \to y \cdot_{R} z = z \cdot_{R} y$
32	30 27 31	syl2anc	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to y \cdot_{R} z = z \cdot_{R} y$
33	29 32	oveq12d	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to (x \cdot_{R} z) +_{R} (y \cdot_{R} z) = (z \cdot_{R} x) +_{R} (z \cdot_{R} y)$
34		simpl1l	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to R \in Ring$
35	5 26	sselid	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to x \in B$
36	5 30	sselid	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to y \in B$
37		simp1r	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to S \subseteq B$
38	37	sselda	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to z \in B$
39		eqid	$⊢ +_{R} = +_{R}$
40	1 39 10	ringdir	$⊢ (R \in Ring \land (x \in B \land y \in B \land z \in B)) \to (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)$
41	34 35 36 38 40	syl13anc	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)$
42	1 39 10	ringdi	$⊢ (R \in Ring \land (z \in B \land x \in B \land y \in B)) \to z \cdot_{R} (x +_{R} y) = (z \cdot_{R} x) +_{R} (z \cdot_{R} y)$
43	34 38 35 36 42	syl13anc	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to z \cdot_{R} (x +_{R} y) = (z \cdot_{R} x) +_{R} (z \cdot_{R} y)$
44	33 41 43	3eqtr4d	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to (x +_{R} y) \cdot_{R} z = z \cdot_{R} (x +_{R} y)$
45	44	ralrimiva	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to \forall z \in S (x +_{R} y) \cdot_{R} z = z \cdot_{R} (x +_{R} y)$
46		simp1l	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to R \in Ring$
47		simp2	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x \in Z (S)$
48	5 47	sselid	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x \in B$
49		simp3	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to y \in Z (S)$
50	5 49	sselid	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to y \in B$
51	1 39	ringacl	$⊢ (R \in Ring \land x \in B \land y \in B) \to x +_{R} y \in B$
52	46 48 50 51	syl3anc	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x +_{R} y \in B$
53	4 21 3	cntzel	$⊢ (S \subseteq B \land x +_{R} y \in B) \to (x +_{R} y \in Z (S) \leftrightarrow \forall z \in S (x +_{R} y) \cdot_{R} z = z \cdot_{R} (x +_{R} y))$
54	37 52 53	syl2anc	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to (x +_{R} y \in Z (S) \leftrightarrow \forall z \in S (x +_{R} y) \cdot_{R} z = z \cdot_{R} (x +_{R} y))$
55	45 54	mpbird	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x +_{R} y \in Z (S)$
56	55	3expa	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land y \in Z (S)) \to x +_{R} y \in Z (S)$
57	56	ralrimiva	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to \forall y \in Z (S) x +_{R} y \in Z (S)$
58	28	adantll	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to x \cdot_{R} z = z \cdot_{R} x$
59	58	fveq2d	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to {inv}_{g} (R) (x \cdot_{R} z) = {inv}_{g} (R) (z \cdot_{R} x)$
60		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
61		simplll	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to R \in Ring$
62		simplr	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to x \in Z (S)$
63	5 62	sselid	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to x \in B$
64		simplr	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to S \subseteq B$
65	64	sselda	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to z \in B$
66	1 10 60 61 63 65	ringmneg1	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to {inv}_{g} (R) (x) \cdot_{R} z = {inv}_{g} (R) (x \cdot_{R} z)$
67	1 10 60 61 65 63	ringmneg2	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to z \cdot_{R} {inv}_{g} (R) (x) = {inv}_{g} (R) (z \cdot_{R} x)$
68	59 66 67	3eqtr4d	$⊢ (((R \in Ring \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to {inv}_{g} (R) (x) \cdot_{R} z = z \cdot_{R} {inv}_{g} (R) (x)$
69	68	ralrimiva	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to \forall z \in S {inv}_{g} (R) (x) \cdot_{R} z = z \cdot_{R} {inv}_{g} (R) (x)$
70		ringgrp	$⊢ R \in Ring \to R \in Grp$
71	70	ad2antrr	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to R \in Grp$
72		simpr	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to x \in Z (S)$
73	5 72	sselid	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to x \in B$
74	1 60	grpinvcl	$⊢ (R \in Grp \land x \in B) \to {inv}_{g} (R) (x) \in B$
75	71 73 74	syl2anc	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to {inv}_{g} (R) (x) \in B$
76	4 21 3	cntzel	$⊢ (S \subseteq B \land {inv}_{g} (R) (x) \in B) \to ({inv}_{g} (R) (x) \in Z (S) \leftrightarrow \forall z \in S {inv}_{g} (R) (x) \cdot_{R} z = z \cdot_{R} {inv}_{g} (R) (x))$
77	64 75 76	syl2anc	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to ({inv}_{g} (R) (x) \in Z (S) \leftrightarrow \forall z \in S {inv}_{g} (R) (x) \cdot_{R} z = z \cdot_{R} {inv}_{g} (R) (x))$
78	69 77	mpbird	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to {inv}_{g} (R) (x) \in Z (S)$
79	57 78	jca	$⊢ ((R \in Ring \land S \subseteq B) \land x \in Z (S)) \to (\forall y \in Z (S) x +_{R} y \in Z (S) \land {inv}_{g} (R) (x) \in Z (S))$
80	79	ralrimiva	$⊢ (R \in Ring \land S \subseteq B) \to \forall x \in Z (S) (\forall y \in Z (S) x +_{R} y \in Z (S) \land {inv}_{g} (R) (x) \in Z (S))$
81	70	adantr	$⊢ (R \in Ring \land S \subseteq B) \to R \in Grp$
82	1 39 60	issubg2	$⊢ R \in Grp \to (Z (S) \in SubGrp (R) \leftrightarrow (Z (S) \subseteq B \land Z (S) \neq \emptyset \land \forall x \in Z (S) (\forall y \in Z (S) x +_{R} y \in Z (S) \land {inv}_{g} (R) (x) \in Z (S))))$
83	81 82	syl	$⊢ (R \in Ring \land S \subseteq B) \to (Z (S) \in SubGrp (R) \leftrightarrow (Z (S) \subseteq B \land Z (S) \neq \emptyset \land \forall x \in Z (S) (\forall y \in Z (S) x +_{R} y \in Z (S) \land {inv}_{g} (R) (x) \in Z (S))))$
84	6 25 80 83	mpbir3and	$⊢ (R \in Ring \land S \subseteq B) \to Z (S) \in SubGrp (R)$
85	2	ringmgp	$⊢ R \in Ring \to M \in Mnd$
86	4 3	cntzsubm	$⊢ (M \in Mnd \land S \subseteq B) \to Z (S) \in SubMnd (M)$
87	85 86	sylan	$⊢ (R \in Ring \land S \subseteq B) \to Z (S) \in SubMnd (M)$
88	2	issubrg3	$⊢ R \in Ring \to (Z (S) \in SubRing (R) \leftrightarrow (Z (S) \in SubGrp (R) \land Z (S) \in SubMnd (M)))$
89	88	adantr	$⊢ (R \in Ring \land S \subseteq B) \to (Z (S) \in SubRing (R) \leftrightarrow (Z (S) \in SubGrp (R) \land Z (S) \in SubMnd (M)))$
90	84 87 89	mpbir2and	$⊢ (R \in Ring \land S \subseteq B) \to Z (S) \in SubRing (R)$

Metamath Proof Explorer

Theorem cntzsubr

Proof