cntzsubrng

Description: Centralizers in a non-unital ring are subrings. (Contributed by AV, 17-Feb-2025)

	Ref	Expression
Hypotheses	cntzsubrng.b	$⊢ B = {Base}_{R}$
	cntzsubrng.m	$⊢ M = {mulGrp}_{R}$
	cntzsubrng.z	$⊢ Z = Cntz (M)$
Assertion	cntzsubrng	Could not format assertion : No typesetting found for \|- ( ( R e. Rng /\ S C_ B ) -> ( Z ` S ) e. ( SubRng ` R ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		cntzsubrng.b	$⊢ B = {Base}_{R}$
2		cntzsubrng.m	$⊢ M = {mulGrp}_{R}$
3		cntzsubrng.z	$⊢ Z = Cntz (M)$
4	2 1	mgpbas	$⊢ B = {Base}_{M}$
5	4 3	cntzssv	$⊢ Z (S) \subseteq B$
6	5	a1i	$⊢ (R \in Rng \land S \subseteq B) \to Z (S) \subseteq B$
7		simpll	$⊢ ((R \in Rng \land S \subseteq B) \land z \in S) \to R \in Rng$
8		ssel2	$⊢ (S \subseteq B \land z \in S) \to z \in B$
9	8	adantll	$⊢ ((R \in Rng \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	rnglz	$⊢ (R \in Rng \land z \in B) \to 0_{R} \cdot_{R} z = 0_{R}$
13	7 9 12	syl2anc	$⊢ ((R \in Rng \land S \subseteq B) \land z \in S) \to 0_{R} \cdot_{R} z = 0_{R}$
14	1 10 11	rngrz	$⊢ (R \in Rng \land z \in B) \to z \cdot_{R} 0_{R} = 0_{R}$
15	7 9 14	syl2anc	$⊢ ((R \in Rng \land S \subseteq B) \land z \in S) \to z \cdot_{R} 0_{R} = 0_{R}$
16	13 15	eqtr4d	$⊢ ((R \in Rng \land S \subseteq B) \land z \in S) \to 0_{R} \cdot_{R} z = z \cdot_{R} 0_{R}$
17	16	ralrimiva	$⊢ (R \in Rng \land S \subseteq B) \to \forall z \in S 0_{R} \cdot_{R} z = z \cdot_{R} 0_{R}$
18		simpr	$⊢ (R \in Rng \land S \subseteq B) \to S \subseteq B$
19	1 11	rng0cl	$⊢ R \in Rng \to 0_{R} \in B$
20	19	adantr	$⊢ (R \in Rng \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 Rng \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 Rng \land S \subseteq B) \to 0_{R} \in Z (S)$
25	24	ne0d	$⊢ (R \in Rng \land S \subseteq B) \to Z (S) \neq \emptyset$
26		simpl2	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to x \in Z (S)$
27	21 3	cntzi	$⊢ (x \in Z (S) \land z \in S) \to x \cdot_{R} z = z \cdot_{R} x$
28	26 27	sylancom	$⊢ (((R \in Rng \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$
29		simpl3	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to y \in Z (S)$
30	21 3	cntzi	$⊢ (y \in Z (S) \land z \in S) \to y \cdot_{R} z = z \cdot_{R} y$
31	29 30	sylancom	$⊢ (((R \in Rng \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$
32	28 31	oveq12d	$⊢ (((R \in Rng \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)$
33		simpl1l	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to R \in Rng$
34	5 26	sselid	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to x \in B$
35	5 29	sselid	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to y \in B$
36		simp1r	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to S \subseteq B$
37	36	sselda	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \land z \in S) \to z \in B$
38		eqid	$⊢ +_{R} = +_{R}$
39	1 38 10	rngdir	$⊢ (R \in Rng \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)$
40	33 34 35 37 39	syl13anc	$⊢ (((R \in Rng \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)$
41	1 38 10	rngdi	$⊢ (R \in Rng \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)$
42	33 37 34 35 41	syl13anc	$⊢ (((R \in Rng \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)$
43	32 40 42	3eqtr4d	$⊢ (((R \in Rng \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)$
44	43	ralrimiva	$⊢ ((R \in Rng \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)$
45		simp1l	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to R \in Rng$
46		simp2	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x \in Z (S)$
47	5 46	sselid	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x \in B$
48		simp3	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to y \in Z (S)$
49	5 48	sselid	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to y \in B$
50	1 38	rngacl	$⊢ (R \in Rng \land x \in B \land y \in B) \to x +_{R} y \in B$
51	45 47 49 50	syl3anc	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x +_{R} y \in B$
52	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))$
53	36 51 52	syl2anc	$⊢ ((R \in Rng \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))$
54	44 53	mpbird	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S) \land y \in Z (S)) \to x +_{R} y \in Z (S)$
55	54	3expa	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S)) \land y \in Z (S)) \to x +_{R} y \in Z (S)$
56	55	ralrimiva	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S)) \to \forall y \in Z (S) x +_{R} y \in Z (S)$
57	27	adantll	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to x \cdot_{R} z = z \cdot_{R} x$
58	57	fveq2d	$⊢ (((R \in Rng \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)$
59		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
60		simplll	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to R \in Rng$
61		simplr	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to x \in Z (S)$
62	5 61	sselid	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to x \in B$
63		simplr	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S)) \to S \subseteq B$
64	63	sselda	$⊢ (((R \in Rng \land S \subseteq B) \land x \in Z (S)) \land z \in S) \to z \in B$
65	1 10 59 60 62 64	rngmneg1	$⊢ (((R \in Rng \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)$
66	1 10 59 60 64 62	rngmneg2	$⊢ (((R \in Rng \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)$
67	58 65 66	3eqtr4d	$⊢ (((R \in Rng \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)$
68	67	ralrimiva	$⊢ ((R \in Rng \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)$
69		rnggrp	$⊢ R \in Rng \to R \in Grp$
70	69	ad2antrr	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S)) \to R \in Grp$
71		simpr	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S)) \to x \in Z (S)$
72	5 71	sselid	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S)) \to x \in B$
73	1 59 70 72	grpinvcld	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S)) \to {inv}_{g} (R) (x) \in B$
74	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))$
75	63 73 74	syl2anc	$⊢ ((R \in Rng \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))$
76	68 75	mpbird	$⊢ ((R \in Rng \land S \subseteq B) \land x \in Z (S)) \to {inv}_{g} (R) (x) \in Z (S)$
77	56 76	jca	$⊢ ((R \in Rng \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))$
78	77	ralrimiva	$⊢ (R \in Rng \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))$
79	69	adantr	$⊢ (R \in Rng \land S \subseteq B) \to R \in Grp$
80	1 38 59	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))))$
81	79 80	syl	$⊢ (R \in Rng \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))))$
82	6 25 78 81	mpbir3and	$⊢ (R \in Rng \land S \subseteq B) \to Z (S) \in SubGrp (R)$
83		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
84	83	rngmgp	Could not format ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) : No typesetting found for \|- ( R e. Rng -> ( mulGrp ` R ) e. Smgrp ) with typecode \|-
85	83 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
86	85	sseq2i	$⊢ S \subseteq B \leftrightarrow S \subseteq {Base}_{{mulGrp}_{R}}$
87	86	biimpi	$⊢ S \subseteq B \to S \subseteq {Base}_{{mulGrp}_{R}}$
88		eqid	$⊢ {Base}_{{mulGrp}_{R}} = {Base}_{{mulGrp}_{R}}$
89	2	fveq2i	$⊢ Cntz (M) = Cntz ({mulGrp}_{R})$
90	3 89	eqtri	$⊢ Z = Cntz ({mulGrp}_{R})$
91		eqid	$⊢ Z (S) = Z (S)$
92	88 90 91	cntzsgrpcl	Could not format ( ( ( mulGrp ` R ) e. Smgrp /\ S C_ ( Base ` ( mulGrp ` R ) ) ) -> A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( +g ` ( mulGrp ` R ) ) y ) e. ( Z ` S ) ) : No typesetting found for \|- ( ( ( mulGrp ` R ) e. Smgrp /\ S C_ ( Base ` ( mulGrp ` R ) ) ) -> A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( +g ` ( mulGrp ` R ) ) y ) e. ( Z ` S ) ) with typecode \|-
93	84 87 92	syl2an	$⊢ (R \in Rng \land S \subseteq B) \to \forall x \in Z (S) \forall y \in Z (S) x +_{{mulGrp}_{R}} y \in Z (S)$
94	83 10	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
95	94	oveqi	$⊢ x \cdot_{R} y = x +_{{mulGrp}_{R}} y$
96	95	eleq1i	$⊢ x \cdot_{R} y \in Z (S) \leftrightarrow x +_{{mulGrp}_{R}} y \in Z (S)$
97	96	2ralbii	$⊢ \forall x \in Z (S) \forall y \in Z (S) x \cdot_{R} y \in Z (S) \leftrightarrow \forall x \in Z (S) \forall y \in Z (S) x +_{{mulGrp}_{R}} y \in Z (S)$
98	93 97	sylibr	$⊢ (R \in Rng \land S \subseteq B) \to \forall x \in Z (S) \forall y \in Z (S) x \cdot_{R} y \in Z (S)$
99	1 10	issubrng2	Could not format ( R e. Rng -> ( ( Z ` S ) e. ( SubRng ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) ) ) ) : No typesetting found for \|- ( R e. Rng -> ( ( Z ` S ) e. ( SubRng ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) ) ) ) with typecode \|-
100	99	adantr	Could not format ( ( R e. Rng /\ S C_ B ) -> ( ( Z ` S ) e. ( SubRng ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) ) ) ) : No typesetting found for \|- ( ( R e. Rng /\ S C_ B ) -> ( ( Z ` S ) e. ( SubRng ` R ) <-> ( ( Z ` S ) e. ( SubGrp ` R ) /\ A. x e. ( Z ` S ) A. y e. ( Z ` S ) ( x ( .r ` R ) y ) e. ( Z ` S ) ) ) ) with typecode \|-
101	82 98 100	mpbir2and	Could not format ( ( R e. Rng /\ S C_ B ) -> ( Z ` S ) e. ( SubRng ` R ) ) : No typesetting found for \|- ( ( R e. Rng /\ S C_ B ) -> ( Z ` S ) e. ( SubRng ` R ) ) with typecode \|-

Metamath Proof Explorer

Theorem cntzsubrng

Proof