lsmcntz

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

	Ref	Expression
Hypotheses	lsmcntz.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	lsmcntz.s	$⊢ φ \to S \in SubGrp (G)$
	lsmcntz.t	$⊢ φ \to T \in SubGrp (G)$
	lsmcntz.u	$⊢ φ \to U \in SubGrp (G)$
	lsmcntz.z	$⊢ Z = Cntz (G)$
Assertion	lsmcntz	$⊢ φ \to (S \underset{˙}{\oplus} T \subseteq Z (U) \leftrightarrow (S \subseteq Z (U) \land T \subseteq Z (U)))$

Step	Hyp	Ref	Expression
1		lsmcntz.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		lsmcntz.s	$⊢ φ \to S \in SubGrp (G)$
3		lsmcntz.t	$⊢ φ \to T \in SubGrp (G)$
4		lsmcntz.u	$⊢ φ \to U \in SubGrp (G)$
5		lsmcntz.z	$⊢ Z = Cntz (G)$
6		subgrcl	$⊢ U \in SubGrp (G) \to G \in Grp$
7		eqid	$⊢ {Base}_{G} = {Base}_{G}$
8	7	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
9	7 5	cntzsubg	$⊢ (G \in Grp \land U \subseteq {Base}_{G}) \to Z (U) \in SubGrp (G)$
10	6 8 9	syl2anc	$⊢ U \in SubGrp (G) \to Z (U) \in SubGrp (G)$
11	4 10	syl	$⊢ φ \to Z (U) \in SubGrp (G)$
12	1	lsmlub	$⊢ (S \in SubGrp (G) \land T \in SubGrp (G) \land Z (U) \in SubGrp (G)) \to ((S \subseteq Z (U) \land T \subseteq Z (U)) \leftrightarrow S \underset{˙}{\oplus} T \subseteq Z (U))$
13	2 3 11 12	syl3anc	$⊢ φ \to ((S \subseteq Z (U) \land T \subseteq Z (U)) \leftrightarrow S \underset{˙}{\oplus} T \subseteq Z (U))$
14	13	bicomd	$⊢ φ \to (S \underset{˙}{\oplus} T \subseteq Z (U) \leftrightarrow (S \subseteq Z (U) \land T \subseteq Z (U)))$

Metamath Proof Explorer