resscntz

Description: Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	resscntz.p	$⊢ H = G ↾_{𝑠} A$
	resscntz.z	$⊢ Z = Cntz (G)$
	resscntz.y	$⊢ Y = Cntz (H)$
Assertion	resscntz	$⊢ (A \in V \land S \subseteq A) \to Y (S) = Z (S) \cap A$

Proof

Step	Hyp	Ref	Expression
1		resscntz.p	$⊢ H = G ↾_{𝑠} A$
2		resscntz.z	$⊢ Z = Cntz (G)$
3		resscntz.y	$⊢ Y = Cntz (H)$
4		eqid	$⊢ {Base}_{H} = {Base}_{H}$
5	4 3	cntzrcl	$⊢ x \in Y (S) \to (H \in V \land S \subseteq {Base}_{H})$
6	5	simprd	$⊢ x \in Y (S) \to S \subseteq {Base}_{H}$
7		eqid	$⊢ {Base}_{G} = {Base}_{G}$
8	1 7	ressbasss	$⊢ {Base}_{H} \subseteq {Base}_{G}$
9	6 8	sstrdi	$⊢ x \in Y (S) \to S \subseteq {Base}_{G}$
10	9	a1i	$⊢ (A \in V \land S \subseteq A) \to (x \in Y (S) \to S \subseteq {Base}_{G})$
11		elinel1	$⊢ x \in (Z (S) \cap A) \to x \in Z (S)$
12	7 2	cntzrcl	$⊢ x \in Z (S) \to (G \in V \land S \subseteq {Base}_{G})$
13	12	simprd	$⊢ x \in Z (S) \to S \subseteq {Base}_{G}$
14	11 13	syl	$⊢ x \in (Z (S) \cap A) \to S \subseteq {Base}_{G}$
15	14	a1i	$⊢ (A \in V \land S \subseteq A) \to (x \in (Z (S) \cap A) \to S \subseteq {Base}_{G})$
16		elin	$⊢ x \in (A \cap {Base}_{G}) \leftrightarrow (x \in A \land x \in {Base}_{G})$
17	1 7	ressbas	$⊢ A \in V \to A \cap {Base}_{G} = {Base}_{H}$
18	17	eleq2d	$⊢ A \in V \to (x \in (A \cap {Base}_{G}) \leftrightarrow x \in {Base}_{H})$
19	16 18	bitr3id	$⊢ A \in V \to ((x \in A \land x \in {Base}_{G}) \leftrightarrow x \in {Base}_{H})$
20		eqid	$⊢ +_{G} = +_{G}$
21	1 20	ressplusg	$⊢ A \in V \to +_{G} = +_{H}$
22	21	oveqd	$⊢ A \in V \to x +_{G} y = x +_{H} y$
23	21	oveqd	$⊢ A \in V \to y +_{G} x = y +_{H} x$
24	22 23	eqeq12d	$⊢ A \in V \to (x +_{G} y = y +_{G} x \leftrightarrow x +_{H} y = y +_{H} x)$
25	24	ralbidv	$⊢ A \in V \to (\forall y \in S x +_{G} y = y +_{G} x \leftrightarrow \forall y \in S x +_{H} y = y +_{H} x)$
26	19 25	anbi12d	$⊢ A \in V \to (((x \in A \land x \in {Base}_{G}) \land \forall y \in S x +_{G} y = y +_{G} x) \leftrightarrow (x \in {Base}_{H} \land \forall y \in S x +_{H} y = y +_{H} x))$
27	26	ad2antrr	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to (((x \in A \land x \in {Base}_{G}) \land \forall y \in S x +_{G} y = y +_{G} x) \leftrightarrow (x \in {Base}_{H} \land \forall y \in S x +_{H} y = y +_{H} x))$
28		anass	$⊢ ((x \in A \land x \in {Base}_{G}) \land \forall y \in S x +_{G} y = y +_{G} x) \leftrightarrow (x \in A \land (x \in {Base}_{G} \land \forall y \in S x +_{G} y = y +_{G} x))$
29	27 28	bitr3di	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to ((x \in {Base}_{H} \land \forall y \in S x +_{H} y = y +_{H} x) \leftrightarrow (x \in A \land (x \in {Base}_{G} \land \forall y \in S x +_{G} y = y +_{G} x)))$
30		ssin	$⊢ (S \subseteq A \land S \subseteq {Base}_{G}) \leftrightarrow S \subseteq A \cap {Base}_{G}$
31	17	sseq2d	$⊢ A \in V \to (S \subseteq A \cap {Base}_{G} \leftrightarrow S \subseteq {Base}_{H})$
32	30 31	bitrid	$⊢ A \in V \to ((S \subseteq A \land S \subseteq {Base}_{G}) \leftrightarrow S \subseteq {Base}_{H})$
33	32	biimpd	$⊢ A \in V \to ((S \subseteq A \land S \subseteq {Base}_{G}) \to S \subseteq {Base}_{H})$
34	33	impl	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to S \subseteq {Base}_{H}$
35		eqid	$⊢ +_{H} = +_{H}$
36	4 35 3	elcntz	$⊢ S \subseteq {Base}_{H} \to (x \in Y (S) \leftrightarrow (x \in {Base}_{H} \land \forall y \in S x +_{H} y = y +_{H} x))$
37	34 36	syl	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to (x \in Y (S) \leftrightarrow (x \in {Base}_{H} \land \forall y \in S x +_{H} y = y +_{H} x))$
38		elin	$⊢ x \in (Z (S) \cap A) \leftrightarrow (x \in Z (S) \land x \in A)$
39	38	biancomi	$⊢ x \in (Z (S) \cap A) \leftrightarrow (x \in A \land x \in Z (S))$
40	7 20 2	elcntz	$⊢ S \subseteq {Base}_{G} \to (x \in Z (S) \leftrightarrow (x \in {Base}_{G} \land \forall y \in S x +_{G} y = y +_{G} x))$
41	40	adantl	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to (x \in Z (S) \leftrightarrow (x \in {Base}_{G} \land \forall y \in S x +_{G} y = y +_{G} x))$
42	41	anbi2d	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to ((x \in A \land x \in Z (S)) \leftrightarrow (x \in A \land (x \in {Base}_{G} \land \forall y \in S x +_{G} y = y +_{G} x)))$
43	39 42	bitrid	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to (x \in (Z (S) \cap A) \leftrightarrow (x \in A \land (x \in {Base}_{G} \land \forall y \in S x +_{G} y = y +_{G} x)))$
44	29 37 43	3bitr4d	$⊢ ((A \in V \land S \subseteq A) \land S \subseteq {Base}_{G}) \to (x \in Y (S) \leftrightarrow x \in (Z (S) \cap A))$
45	44	ex	$⊢ (A \in V \land S \subseteq A) \to (S \subseteq {Base}_{G} \to (x \in Y (S) \leftrightarrow x \in (Z (S) \cap A)))$
46	10 15 45	pm5.21ndd	$⊢ (A \in V \land S \subseteq A) \to (x \in Y (S) \leftrightarrow x \in (Z (S) \cap A))$
47	46	eqrdv	$⊢ (A \in V \land S \subseteq A) \to Y (S) = Z (S) \cap A$

Metamath Proof Explorer

Theorem resscntz

Proof