Theorem cntzun

Description: The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023)

	Ref	Expression
Hypotheses	cntzun.b	$$⊢B={\mathrm{Base}}_M$$
	cntzun.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	cntzun	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to Z\left(X\cup Y\right)=Z\left(X\right)\cap Z\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntzun.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzun.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
3		ralunb	$$⊢\forall y\in \left(X\cup Y\right)x{+}_{M}y=y{+}_{M}x\leftrightarrow \left(\forall y\in Xx{+}_{M}y=y{+}_{M}x\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)$$
4	3	a1i	$$⊢\left(\left(X\subseteq B\wedge Y\subseteq B\right)\wedge x\in B\right)\to \left(\forall y\in \left(X\cup Y\right)x{+}_{M}y=y{+}_{M}x\leftrightarrow \left(\forall y\in Xx{+}_{M}y=y{+}_{M}x\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)\right)$$
5	4	pm5.32da	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to \left(\left(x\in B\wedge \forall y\in \left(X\cup Y\right)x{+}_{M}y=y{+}_{M}x\right)\leftrightarrow \left(x\in B\wedge \left(\forall y\in Xx{+}_{M}y=y{+}_{M}x\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)\right)\right)$$
6		anandi	$$⊢\left(x\in B\wedge \left(\forall y\in Xx{+}_{M}y=y{+}_{M}x\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)\right)\leftrightarrow \left(\left(x\in B\wedge \forall y\in Xx{+}_{M}y=y{+}_{M}x\right)\wedge \left(x\in B\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)\right)$$
7	5 6	bitrdi	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to \left(\left(x\in B\wedge \forall y\in \left(X\cup Y\right)x{+}_{M}y=y{+}_{M}x\right)\leftrightarrow \left(\left(x\in B\wedge \forall y\in Xx{+}_{M}y=y{+}_{M}x\right)\wedge \left(x\in B\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)\right)\right)$$
8		unss	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\leftrightarrow X\cup Y\subseteq B$$
9		eqid	$$⊢{+}_M={+}_M$$
10	1 9 2	elcntz	$$⊢X\cup Y\subseteq B\to \left(x\in Z\left(X\cup Y\right)\leftrightarrow \left(x\in B\wedge \forall y\in \left(X\cup Y\right)x{+}_{M}y=y{+}_{M}x\right)\right)$$
11	8 10	sylbi	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to \left(x\in Z\left(X\cup Y\right)\leftrightarrow \left(x\in B\wedge \forall y\in \left(X\cup Y\right)x{+}_{M}y=y{+}_{M}x\right)\right)$$
12	1 9 2	elcntz	$$⊢X\subseteq B\to \left(x\in Z\left(X\right)\leftrightarrow \left(x\in B\wedge \forall y\in Xx{+}_{M}y=y{+}_{M}x\right)\right)$$
13	1 9 2	elcntz	$$⊢Y\subseteq B\to \left(x\in Z\left(Y\right)\leftrightarrow \left(x\in B\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)\right)$$
14	12 13	bi2anan9	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to \left(\left(x\in Z\left(X\right)\wedge x\in Z\left(Y\right)\right)\leftrightarrow \left(\left(x\in B\wedge \forall y\in Xx{+}_{M}y=y{+}_{M}x\right)\wedge \left(x\in B\wedge \forall y\in Yx{+}_{M}y=y{+}_{M}x\right)\right)\right)$$
15	7 11 14	3bitr4d	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to \left(x\in Z\left(X\cup Y\right)\leftrightarrow \left(x\in Z\left(X\right)\wedge x\in Z\left(Y\right)\right)\right)$$
16		elin	$$⊢x\in \left(Z\left(X\right)\cap Z\left(Y\right)\right)\leftrightarrow \left(x\in Z\left(X\right)\wedge x\in Z\left(Y\right)\right)$$
17	15 16	bitr4di	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to \left(x\in Z\left(X\cup Y\right)\leftrightarrow x\in \left(Z\left(X\right)\cap Z\left(Y\right)\right)\right)$$
18	17	eqrdv	$$⊢\left(X\subseteq B\wedge Y\subseteq B\right)\to Z\left(X\cup Y\right)=Z\left(X\right)\cap Z\left(Y\right)$$