dmdprdd

Description: Show that a given family is a direct product decomposition. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

	Ref	Expression
Hypotheses	dmdprd.z	$⊢ Z = Cntz (G)$
	dmdprd.0	$⊢ \underset{˙}{0} = 0_{G}$
	dmdprd.k	$⊢ K = mrCls (SubGrp (G))$
	dmdprdd.1	$⊢ φ \to G \in Grp$
	dmdprdd.2	$⊢ φ \to I \in V$
	dmdprdd.3	$⊢ φ \to S : I ⟶ SubGrp (G)$
	dmdprdd.4	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to S (x) \subseteq Z (S (y))$
	dmdprdd.5	$⊢ (φ \land x \in I) \to S (x) \cap K (⋃ S [I ∖ \{x\}]) \subseteq \{\underset{˙}{0}\}$
Assertion	dmdprdd	$⊢ φ \to G dom DProd S$

Proof

Step	Hyp	Ref	Expression
1		dmdprd.z	$⊢ Z = Cntz (G)$
2		dmdprd.0	$⊢ \underset{˙}{0} = 0_{G}$
3		dmdprd.k	$⊢ K = mrCls (SubGrp (G))$
4		dmdprdd.1	$⊢ φ \to G \in Grp$
5		dmdprdd.2	$⊢ φ \to I \in V$
6		dmdprdd.3	$⊢ φ \to S : I ⟶ SubGrp (G)$
7		dmdprdd.4	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to S (x) \subseteq Z (S (y))$
8		dmdprdd.5	$⊢ (φ \land x \in I) \to S (x) \cap K (⋃ S [I ∖ \{x\}]) \subseteq \{\underset{˙}{0}\}$
9		eldifsn	$⊢ y \in (I ∖ \{x\}) \leftrightarrow (y \in I \land y \neq x)$
10		necom	$⊢ y \neq x \leftrightarrow x \neq y$
11	10	anbi2i	$⊢ (y \in I \land y \neq x) \leftrightarrow (y \in I \land x \neq y)$
12	9 11	bitri	$⊢ y \in (I ∖ \{x\}) \leftrightarrow (y \in I \land x \neq y)$
13	7	3exp2	$⊢ φ \to (x \in I \to (y \in I \to (x \neq y \to S (x) \subseteq Z (S (y)))))$
14	13	imp4b	$⊢ (φ \land x \in I) \to ((y \in I \land x \neq y) \to S (x) \subseteq Z (S (y)))$
15	12 14	syl5bi	$⊢ (φ \land x \in I) \to (y \in (I ∖ \{x\}) \to S (x) \subseteq Z (S (y)))$
16	15	ralrimiv	$⊢ (φ \land x \in I) \to \forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y))$
17	6	ffvelrnda	$⊢ (φ \land x \in I) \to S (x) \in SubGrp (G)$
18	2	subg0cl	$⊢ S (x) \in SubGrp (G) \to \underset{˙}{0} \in S (x)$
19	17 18	syl	$⊢ (φ \land x \in I) \to \underset{˙}{0} \in S (x)$
20	4	adantr	$⊢ (φ \land x \in I) \to G \in Grp$
21		eqid	$⊢ {Base}_{G} = {Base}_{G}$
22	21	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
23		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
24	20 22 23	3syl	$⊢ (φ \land x \in I) \to SubGrp (G) \in Moore ({Base}_{G})$
25		imassrn	$⊢ S [I ∖ \{x\}] \subseteq ran S$
26	6	frnd	$⊢ φ \to ran S \subseteq SubGrp (G)$
27	26	adantr	$⊢ (φ \land x \in I) \to ran S \subseteq SubGrp (G)$
28	25 27	sstrid	$⊢ (φ \land x \in I) \to S [I ∖ \{x\}] \subseteq SubGrp (G)$
29		mresspw	$⊢ SubGrp (G) \in Moore ({Base}_{G}) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
30	24 29	syl	$⊢ (φ \land x \in I) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
31	28 30	sstrd	$⊢ (φ \land x \in I) \to S [I ∖ \{x\}] \subseteq 𝒫 {Base}_{G}$
32		sspwuni	$⊢ S [I ∖ \{x\}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ S [I ∖ \{x\}] \subseteq {Base}_{G}$
33	31 32	sylib	$⊢ (φ \land x \in I) \to ⋃ S [I ∖ \{x\}] \subseteq {Base}_{G}$
34	3	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ S [I ∖ \{x\}] \subseteq {Base}_{G}) \to K (⋃ S [I ∖ \{x\}]) \in SubGrp (G)$
35	24 33 34	syl2anc	$⊢ (φ \land x \in I) \to K (⋃ S [I ∖ \{x\}]) \in SubGrp (G)$
36	2	subg0cl	$⊢ K (⋃ S [I ∖ \{x\}]) \in SubGrp (G) \to \underset{˙}{0} \in K (⋃ S [I ∖ \{x\}])$
37	35 36	syl	$⊢ (φ \land x \in I) \to \underset{˙}{0} \in K (⋃ S [I ∖ \{x\}])$
38	19 37	elind	$⊢ (φ \land x \in I) \to \underset{˙}{0} \in (S (x) \cap K (⋃ S [I ∖ \{x\}]))$
39	38	snssd	$⊢ (φ \land x \in I) \to \{\underset{˙}{0}\} \subseteq S (x) \cap K (⋃ S [I ∖ \{x\}])$
40	8 39	eqssd	$⊢ (φ \land x \in I) \to S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\}$
41	16 40	jca	$⊢ (φ \land x \in I) \to (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})$
42	41	ralrimiva	$⊢ φ \to \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})$
43	6	fdmd	$⊢ φ \to dom S = I$
44	1 2 3	dmdprd	$⊢ (I \in V \land dom S = I) \to (G dom DProd S \leftrightarrow (G \in Grp \land S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
45	5 43 44	syl2anc	$⊢ φ \to (G dom DProd S \leftrightarrow (G \in Grp \land S : I ⟶ SubGrp (G) \land \forall x \in I (\forall y \in (I ∖ \{x\}) S (x) \subseteq Z (S (y)) \land S (x) \cap K (⋃ S [I ∖ \{x\}]) = \{\underset{˙}{0}\})))$
46	4 6 42 45	mpbir3and	$⊢ φ \to G dom DProd S$

Metamath Proof Explorer

Theorem dmdprdd

Proof