Theorem cntzrecd

Description: Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	cntzrecd.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
	cntzrecd.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
	cntzrecd.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
	cntzrecd.s	$$⊢\phi \to T\subseteq Z\left(U\right)$$
Assertion	cntzrecd	$$⊢\phi \to U\subseteq Z\left(T\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntzrecd.z	$$⊢Z=\mathrm{Cntz}\left(G\right)$$
2		cntzrecd.t	$$⊢\phi \to T\in \mathrm{SubGrp}\left(G\right)$$
3		cntzrecd.u	$$⊢\phi \to U\in \mathrm{SubGrp}\left(G\right)$$
4		cntzrecd.s	$$⊢\phi \to T\subseteq Z\left(U\right)$$
5		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
6	5	subgss	$$⊢T\in \mathrm{SubGrp}\left(G\right)\to T\subseteq {\mathrm{Base}}_G$$
7	5	subgss	$$⊢U\in \mathrm{SubGrp}\left(G\right)\to U\subseteq {\mathrm{Base}}_G$$
8	5 1	cntzrec	$$⊢\left(T\subseteq {\mathrm{Base}}_G\wedge U\subseteq {\mathrm{Base}}_G\right)\to \left(T\subseteq Z\left(U\right)\leftrightarrow U\subseteq Z\left(T\right)\right)$$
9	6 7 8	syl2an	$$⊢\left(T\in \mathrm{SubGrp}\left(G\right)\wedge U\in \mathrm{SubGrp}\left(G\right)\right)\to \left(T\subseteq Z\left(U\right)\leftrightarrow U\subseteq Z\left(T\right)\right)$$
10	2 3 9	syl2anc	$$⊢\phi \to \left(T\subseteq Z\left(U\right)\leftrightarrow U\subseteq Z\left(T\right)\right)$$
11	4 10	mpbid	$$⊢\phi \to U\subseteq Z\left(T\right)$$