lsmcntzr

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	lsmcntzr	$⊢ φ \to (S \subseteq Z (T \underset{˙}{\oplus} U) \leftrightarrow (S \subseteq Z (T) \land S \subseteq Z (U)))$

Proof

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	1 3 4 2 5	lsmcntz	$⊢ φ \to (T \underset{˙}{\oplus} U \subseteq Z (S) \leftrightarrow (T \subseteq Z (S) \land U \subseteq Z (S)))$
7		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
8		grpmnd	$⊢ G \in Grp \to G \in Mnd$
9	2 7 8	3syl	$⊢ φ \to G \in Mnd$
10		eqid	$⊢ {Base}_{G} = {Base}_{G}$
11	10	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
12	3 11	syl	$⊢ φ \to T \subseteq {Base}_{G}$
13	10	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
14	4 13	syl	$⊢ φ \to U \subseteq {Base}_{G}$
15	10 1	lsmssv	$⊢ (G \in Mnd \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to T \underset{˙}{\oplus} U \subseteq {Base}_{G}$
16	9 12 14 15	syl3anc	$⊢ φ \to T \underset{˙}{\oplus} U \subseteq {Base}_{G}$
17	10	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
18	2 17	syl	$⊢ φ \to S \subseteq {Base}_{G}$
19	10 5	cntzrec	$⊢ (T \underset{˙}{\oplus} U \subseteq {Base}_{G} \land S \subseteq {Base}_{G}) \to (T \underset{˙}{\oplus} U \subseteq Z (S) \leftrightarrow S \subseteq Z (T \underset{˙}{\oplus} U))$
20	16 18 19	syl2anc	$⊢ φ \to (T \underset{˙}{\oplus} U \subseteq Z (S) \leftrightarrow S \subseteq Z (T \underset{˙}{\oplus} U))$
21	10 5	cntzrec	$⊢ (T \subseteq {Base}_{G} \land S \subseteq {Base}_{G}) \to (T \subseteq Z (S) \leftrightarrow S \subseteq Z (T))$
22	12 18 21	syl2anc	$⊢ φ \to (T \subseteq Z (S) \leftrightarrow S \subseteq Z (T))$
23	10 5	cntzrec	$⊢ (U \subseteq {Base}_{G} \land S \subseteq {Base}_{G}) \to (U \subseteq Z (S) \leftrightarrow S \subseteq Z (U))$
24	14 18 23	syl2anc	$⊢ φ \to (U \subseteq Z (S) \leftrightarrow S \subseteq Z (U))$
25	22 24	anbi12d	$⊢ φ \to ((T \subseteq Z (S) \land U \subseteq Z (S)) \leftrightarrow (S \subseteq Z (T) \land S \subseteq Z (U)))$
26	6 20 25	3bitr3d	$⊢ φ \to (S \subseteq Z (T \underset{˙}{\oplus} U) \leftrightarrow (S \subseteq Z (T) \land S \subseteq Z (U)))$

Metamath Proof Explorer

Theorem lsmcntzr

Proof