cntzrecd

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

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

Metamath Proof Explorer