cntzsubg

Description: Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	cntzrec.b	$⊢ B = {Base}_{M}$
	cntzrec.z	$⊢ Z = Cntz (M)$
Assertion	cntzsubg	$⊢ (M \in Grp \land S \subseteq B) \to Z (S) \in SubGrp (M)$

Proof

Step	Hyp	Ref	Expression
1		cntzrec.b	$⊢ B = {Base}_{M}$
2		cntzrec.z	$⊢ Z = Cntz (M)$
3		grpmnd	$⊢ M \in Grp \to M \in Mnd$
4	1 2	cntzsubm	$⊢ (M \in Mnd \land S \subseteq B) \to Z (S) \in SubMnd (M)$
5	3 4	sylan	$⊢ (M \in Grp \land S \subseteq B) \to Z (S) \in SubMnd (M)$
6		simpll	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to M \in Grp$
7	1 2	cntzssv	$⊢ Z (S) \subseteq B$
8		simprl	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to x \in Z (S)$
9	7 8	sselid	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to x \in B$
10		eqid	$⊢ {inv}_{g} (M) = {inv}_{g} (M)$
11	1 10	grpinvcl	$⊢ (M \in Grp \land x \in B) \to {inv}_{g} (M) (x) \in B$
12	6 9 11	syl2anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to {inv}_{g} (M) (x) \in B$
13		ssel2	$⊢ (S \subseteq B \land y \in S) \to y \in B$
14	13	ad2ant2l	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to y \in B$
15		eqid	$⊢ +_{M} = +_{M}$
16	1 15	grpcl	$⊢ (M \in Grp \land x \in B \land {inv}_{g} (M) (x) \in B) \to x +_{M} {inv}_{g} (M) (x) \in B$
17	6 9 12 16	syl3anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to x +_{M} {inv}_{g} (M) (x) \in B$
18	1 15	grpass	$⊢ (M \in Grp \land ({inv}_{g} (M) (x) \in B \land y \in B \land x +_{M} {inv}_{g} (M) (x) \in B)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} (x +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} (y +_{M} (x +_{M} {inv}_{g} (M) (x)))$
19	6 12 14 17 18	syl13anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} (x +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} (y +_{M} (x +_{M} {inv}_{g} (M) (x)))$
20	1 15	grpass	$⊢ (M \in Grp \land (y \in B \land x \in B \land {inv}_{g} (M) (x) \in B)) \to (y +_{M} x) +_{M} {inv}_{g} (M) (x) = y +_{M} (x +_{M} {inv}_{g} (M) (x))$
21	6 14 9 12 20	syl13anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to (y +_{M} x) +_{M} {inv}_{g} (M) (x) = y +_{M} (x +_{M} {inv}_{g} (M) (x))$
22	21	oveq2d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to {inv}_{g} (M) (x) +_{M} ((y +_{M} x) +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} (y +_{M} (x +_{M} {inv}_{g} (M) (x)))$
23	19 22	eqtr4d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} (x +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} ((y +_{M} x) +_{M} {inv}_{g} (M) (x))$
24	15 2	cntzi	$⊢ (x \in Z (S) \land y \in S) \to x +_{M} y = y +_{M} x$
25	24	adantl	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to x +_{M} y = y +_{M} x$
26	25	oveq1d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to (x +_{M} y) +_{M} {inv}_{g} (M) (x) = (y +_{M} x) +_{M} {inv}_{g} (M) (x)$
27	26	oveq2d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to {inv}_{g} (M) (x) +_{M} ((x +_{M} y) +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} ((y +_{M} x) +_{M} {inv}_{g} (M) (x))$
28	23 27	eqtr4d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} (x +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} ((x +_{M} y) +_{M} {inv}_{g} (M) (x))$
29	1 15	grpcl	$⊢ (M \in Grp \land y \in B \land {inv}_{g} (M) (x) \in B) \to y +_{M} {inv}_{g} (M) (x) \in B$
30	6 14 12 29	syl3anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to y +_{M} {inv}_{g} (M) (x) \in B$
31	1 15	grpass	$⊢ (M \in Grp \land ({inv}_{g} (M) (x) \in B \land x \in B \land y +_{M} {inv}_{g} (M) (x) \in B)) \to ({inv}_{g} (M) (x) +_{M} x) +_{M} (y +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} (x +_{M} (y +_{M} {inv}_{g} (M) (x)))$
32	6 12 9 30 31	syl13anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} x) +_{M} (y +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} (x +_{M} (y +_{M} {inv}_{g} (M) (x)))$
33	1 15	grpass	$⊢ (M \in Grp \land (x \in B \land y \in B \land {inv}_{g} (M) (x) \in B)) \to (x +_{M} y) +_{M} {inv}_{g} (M) (x) = x +_{M} (y +_{M} {inv}_{g} (M) (x))$
34	6 9 14 12 33	syl13anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to (x +_{M} y) +_{M} {inv}_{g} (M) (x) = x +_{M} (y +_{M} {inv}_{g} (M) (x))$
35	34	oveq2d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to {inv}_{g} (M) (x) +_{M} ((x +_{M} y) +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} (x +_{M} (y +_{M} {inv}_{g} (M) (x)))$
36	32 35	eqtr4d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} x) +_{M} (y +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} ((x +_{M} y) +_{M} {inv}_{g} (M) (x))$
37	28 36	eqtr4d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} (x +_{M} {inv}_{g} (M) (x)) = ({inv}_{g} (M) (x) +_{M} x) +_{M} (y +_{M} {inv}_{g} (M) (x))$
38		eqid	$⊢ 0_{M} = 0_{M}$
39	1 15 38 10	grprinv	$⊢ (M \in Grp \land x \in B) \to x +_{M} {inv}_{g} (M) (x) = 0_{M}$
40	6 9 39	syl2anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to x +_{M} {inv}_{g} (M) (x) = 0_{M}$
41	40	oveq2d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} (x +_{M} {inv}_{g} (M) (x)) = ({inv}_{g} (M) (x) +_{M} y) +_{M} 0_{M}$
42	1 15	grpcl	$⊢ (M \in Grp \land {inv}_{g} (M) (x) \in B \land y \in B) \to {inv}_{g} (M) (x) +_{M} y \in B$
43	6 12 14 42	syl3anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to {inv}_{g} (M) (x) +_{M} y \in B$
44	1 15 38	grprid	$⊢ (M \in Grp \land {inv}_{g} (M) (x) +_{M} y \in B) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} 0_{M} = {inv}_{g} (M) (x) +_{M} y$
45	6 43 44	syl2anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} 0_{M} = {inv}_{g} (M) (x) +_{M} y$
46	41 45	eqtrd	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} y) +_{M} (x +_{M} {inv}_{g} (M) (x)) = {inv}_{g} (M) (x) +_{M} y$
47	1 15 38 10	grplinv	$⊢ (M \in Grp \land x \in B) \to {inv}_{g} (M) (x) +_{M} x = 0_{M}$
48	6 9 47	syl2anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to {inv}_{g} (M) (x) +_{M} x = 0_{M}$
49	48	oveq1d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} x) +_{M} (y +_{M} {inv}_{g} (M) (x)) = 0_{M} +_{M} (y +_{M} {inv}_{g} (M) (x))$
50	1 15 38	grplid	$⊢ (M \in Grp \land y +_{M} {inv}_{g} (M) (x) \in B) \to 0_{M} +_{M} (y +_{M} {inv}_{g} (M) (x)) = y +_{M} {inv}_{g} (M) (x)$
51	6 30 50	syl2anc	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to 0_{M} +_{M} (y +_{M} {inv}_{g} (M) (x)) = y +_{M} {inv}_{g} (M) (x)$
52	49 51	eqtrd	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to ({inv}_{g} (M) (x) +_{M} x) +_{M} (y +_{M} {inv}_{g} (M) (x)) = y +_{M} {inv}_{g} (M) (x)$
53	37 46 52	3eqtr3d	$⊢ ((M \in Grp \land S \subseteq B) \land (x \in Z (S) \land y \in S)) \to {inv}_{g} (M) (x) +_{M} y = y +_{M} {inv}_{g} (M) (x)$
54	53	anassrs	$⊢ (((M \in Grp \land S \subseteq B) \land x \in Z (S)) \land y \in S) \to {inv}_{g} (M) (x) +_{M} y = y +_{M} {inv}_{g} (M) (x)$
55	54	ralrimiva	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to \forall y \in S {inv}_{g} (M) (x) +_{M} y = y +_{M} {inv}_{g} (M) (x)$
56		simplr	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to S \subseteq B$
57		simpll	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to M \in Grp$
58		simpr	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to x \in Z (S)$
59	7 58	sselid	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to x \in B$
60	57 59 11	syl2anc	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to {inv}_{g} (M) (x) \in B$
61	1 15 2	cntzel	$⊢ (S \subseteq B \land {inv}_{g} (M) (x) \in B) \to ({inv}_{g} (M) (x) \in Z (S) \leftrightarrow \forall y \in S {inv}_{g} (M) (x) +_{M} y = y +_{M} {inv}_{g} (M) (x))$
62	56 60 61	syl2anc	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to ({inv}_{g} (M) (x) \in Z (S) \leftrightarrow \forall y \in S {inv}_{g} (M) (x) +_{M} y = y +_{M} {inv}_{g} (M) (x))$
63	55 62	mpbird	$⊢ ((M \in Grp \land S \subseteq B) \land x \in Z (S)) \to {inv}_{g} (M) (x) \in Z (S)$
64	63	ralrimiva	$⊢ (M \in Grp \land S \subseteq B) \to \forall x \in Z (S) {inv}_{g} (M) (x) \in Z (S)$
65	10	issubg3	$⊢ M \in Grp \to (Z (S) \in SubGrp (M) \leftrightarrow (Z (S) \in SubMnd (M) \land \forall x \in Z (S) {inv}_{g} (M) (x) \in Z (S)))$
66	65	adantr	$⊢ (M \in Grp \land S \subseteq B) \to (Z (S) \in SubGrp (M) \leftrightarrow (Z (S) \in SubMnd (M) \land \forall x \in Z (S) {inv}_{g} (M) (x) \in Z (S)))$
67	5 64 66	mpbir2and	$⊢ (M \in Grp \land S \subseteq B) \to Z (S) \in SubGrp (M)$

Metamath Proof Explorer

Theorem cntzsubg

Proof