cntzi

Description: Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	cntzi.p	$⊢ \underset{˙}{+} = +_{M}$
	cntzi.z	$⊢ Z = Cntz (M)$
Assertion	cntzi	$⊢ (X \in Z (S) \land Y \in S) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Step	Hyp	Ref	Expression
1		cntzi.p	$⊢ \underset{˙}{+} = +_{M}$
2		cntzi.z	$⊢ Z = Cntz (M)$
3		eqid	$⊢ {Base}_{M} = {Base}_{M}$
4	3 2	cntzrcl	$⊢ X \in Z (S) \to (M \in V \land S \subseteq {Base}_{M})$
5	3 1 2	elcntz	$⊢ S \subseteq {Base}_{M} \to (X \in Z (S) \leftrightarrow (X \in {Base}_{M} \land \forall y \in S X \underset{˙}{+} y = y \underset{˙}{+} X))$
6	4 5	simpl2im	$⊢ X \in Z (S) \to (X \in Z (S) \leftrightarrow (X \in {Base}_{M} \land \forall y \in S X \underset{˙}{+} y = y \underset{˙}{+} X))$
7	6	simplbda	$⊢ (X \in Z (S) \land X \in Z (S)) \to \forall y \in S X \underset{˙}{+} y = y \underset{˙}{+} X$
8	7	anidms	$⊢ X \in Z (S) \to \forall y \in S X \underset{˙}{+} y = y \underset{˙}{+} X$
9		oveq2	$⊢ y = Y \to X \underset{˙}{+} y = X \underset{˙}{+} Y$
10		oveq1	$⊢ y = Y \to y \underset{˙}{+} X = Y \underset{˙}{+} X$
11	9 10	eqeq12d	$⊢ y = Y \to (X \underset{˙}{+} y = y \underset{˙}{+} X \leftrightarrow X \underset{˙}{+} Y = Y \underset{˙}{+} X)$
12	11	rspccva	$⊢ (\forall y \in S X \underset{˙}{+} y = y \underset{˙}{+} X \land Y \in S) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$
13	8 12	sylan	$⊢ (X \in Z (S) \land Y \in S) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Metamath Proof Explorer