Theorem cntzrecd

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

	Ref	Expression
Hypotheses	cntzrecd.z	|- Z = ( Cntz ` G )
	cntzrecd.t	|- ( ph -> T e. ( SubGrp ` G ) )
	cntzrecd.u	|- ( ph -> U e. ( SubGrp ` G ) )
	cntzrecd.s	|- ( ph -> T C_ ( Z ` U ) )
Assertion	cntzrecd	|- ( ph -> U C_ ( Z ` T ) )

Proof

Step	Hyp	Ref	Expression
1		cntzrecd.z	|- Z = ( Cntz ` G )
2		cntzrecd.t	|- ( ph -> T e. ( SubGrp ` G ) )
3		cntzrecd.u	|- ( ph -> U e. ( SubGrp ` G ) )
4		cntzrecd.s	|- ( ph -> T C_ ( Z ` U ) )
5		eqid	|- ( Base ` G ) = ( Base ` G )
6	5	subgss	|- ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
7	5	subgss	|- ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
8	5 1	cntzrec	|- ( ( T C_ ( Base ` G ) /\ U C_ ( Base ` G ) ) -> ( T C_ ( Z ` U ) <-> U C_ ( Z ` T ) ) )
9	6 7 8	syl2an	|- ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( T C_ ( Z ` U ) <-> U C_ ( Z ` T ) ) )
10	2 3 9	syl2anc	|- ( ph -> ( T C_ ( Z ` U ) <-> U C_ ( Z ` T ) ) )
11	4 10	mpbid	|- ( ph -> U C_ ( Z ` T ) )