Theorem lsmcntz

Description: The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	lsmcntz.p	|- .(+) = ( LSSum ` G )
	lsmcntz.s	|- ( ph -> S e. ( SubGrp ` G ) )
	lsmcntz.t	|- ( ph -> T e. ( SubGrp ` G ) )
	lsmcntz.u	|- ( ph -> U e. ( SubGrp ` G ) )
	lsmcntz.z	|- Z = ( Cntz ` G )
Assertion	lsmcntz	|- ( ph -> ( ( S .(+) T ) C_ ( Z ` U ) <-> ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsmcntz.p	|- .(+) = ( LSSum ` G )
2		lsmcntz.s	|- ( ph -> S e. ( SubGrp ` G ) )
3		lsmcntz.t	|- ( ph -> T e. ( SubGrp ` G ) )
4		lsmcntz.u	|- ( ph -> U e. ( SubGrp ` G ) )
5		lsmcntz.z	|- Z = ( Cntz ` G )
6		subgrcl	|- ( U e. ( SubGrp ` G ) -> G e. Grp )
7		eqid	|- ( Base ` G ) = ( Base ` G )
8	7	subgss	|- ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
9	7 5	cntzsubg	|- ( ( G e. Grp /\ U C_ ( Base ` G ) ) -> ( Z ` U ) e. ( SubGrp ` G ) )
10	6 8 9	syl2anc	|- ( U e. ( SubGrp ` G ) -> ( Z ` U ) e. ( SubGrp ` G ) )
11	4 10	syl	|- ( ph -> ( Z ` U ) e. ( SubGrp ` G ) )
12	1	lsmlub	|- ( ( S e. ( SubGrp ` G ) /\ T e. ( SubGrp ` G ) /\ ( Z ` U ) e. ( SubGrp ` G ) ) -> ( ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) <-> ( S .(+) T ) C_ ( Z ` U ) ) )
13	2 3 11 12	syl3anc	|- ( ph -> ( ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) <-> ( S .(+) T ) C_ ( Z ` U ) ) )
14	13	bicomd	|- ( ph -> ( ( S .(+) T ) C_ ( Z ` U ) <-> ( S C_ ( Z ` U ) /\ T C_ ( Z ` U ) ) ) )