dprdz

Description: A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

		Ref	Expression
	Hypothesis	dprd0.0	$⊢ \underset{˙}{0} = 0_{G}$
	Assertion	dprdz	$⊢ (G \in Grp \land I \in V) \to (G dom DProd (x \in I ⟼ \{\underset{˙}{0}\}) \land G DProd (x \in I ⟼ \{\underset{˙}{0}\}) = \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		dprd0.0	$⊢ \underset{˙}{0} = 0_{G}$
2		eqid	$⊢ Cntz (G) = Cntz (G)$
3		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
4		simpl	$⊢ (G \in Grp \land I \in V) \to G \in Grp$
5		simpr	$⊢ (G \in Grp \land I \in V) \to I \in V$
6	1	0subg	$⊢ G \in Grp \to \{\underset{˙}{0}\} \in SubGrp (G)$
7	6	ad2antrr	$⊢ ((G \in Grp \land I \in V) \land x \in I) \to \{\underset{˙}{0}\} \in SubGrp (G)$
8	7	fmpttd	$⊢ (G \in Grp \land I \in V) \to (x \in I ⟼ \{\underset{˙}{0}\}) : I ⟶ SubGrp (G)$
9		eqid	$⊢ {Base}_{G} = {Base}_{G}$
10	9 1	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in {Base}_{G}$
11	10	adantr	$⊢ (G \in Grp \land I \in V) \to \underset{˙}{0} \in {Base}_{G}$
12	11	snssd	$⊢ (G \in Grp \land I \in V) \to \{\underset{˙}{0}\} \subseteq {Base}_{G}$
13	9 2	cntzsubg	$⊢ (G \in Grp \land \{\underset{˙}{0}\} \subseteq {Base}_{G}) \to Cntz (G) (\{\underset{˙}{0}\}) \in SubGrp (G)$
14	12 13	syldan	$⊢ (G \in Grp \land I \in V) \to Cntz (G) (\{\underset{˙}{0}\}) \in SubGrp (G)$
15	1	subg0cl	$⊢ Cntz (G) (\{\underset{˙}{0}\}) \in SubGrp (G) \to \underset{˙}{0} \in Cntz (G) (\{\underset{˙}{0}\})$
16	14 15	syl	$⊢ (G \in Grp \land I \in V) \to \underset{˙}{0} \in Cntz (G) (\{\underset{˙}{0}\})$
17	16	snssd	$⊢ (G \in Grp \land I \in V) \to \{\underset{˙}{0}\} \subseteq Cntz (G) (\{\underset{˙}{0}\})$
18	17	adantr	$⊢ ((G \in Grp \land I \in V) \land (y \in I \land z \in I \land y \neq z)) \to \{\underset{˙}{0}\} \subseteq Cntz (G) (\{\underset{˙}{0}\})$
19		simpr1	$⊢ ((G \in Grp \land I \in V) \land (y \in I \land z \in I \land y \neq z)) \to y \in I$
20		eqidd	$⊢ x = y \to \{\underset{˙}{0}\} = \{\underset{˙}{0}\}$
21		eqid	$⊢ (x \in I ⟼ \{\underset{˙}{0}\}) = (x \in I ⟼ \{\underset{˙}{0}\})$
22		snex	$⊢ \{\underset{˙}{0}\} \in V$
23	20 21 22	fvmpt3i	$⊢ y \in I \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) = \{\underset{˙}{0}\}$
24	19 23	syl	$⊢ ((G \in Grp \land I \in V) \land (y \in I \land z \in I \land y \neq z)) \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) = \{\underset{˙}{0}\}$
25		simpr2	$⊢ ((G \in Grp \land I \in V) \land (y \in I \land z \in I \land y \neq z)) \to z \in I$
26		eqidd	$⊢ x = z \to \{\underset{˙}{0}\} = \{\underset{˙}{0}\}$
27	26 21 22	fvmpt3i	$⊢ z \in I \to (x \in I ⟼ \{\underset{˙}{0}\}) (z) = \{\underset{˙}{0}\}$
28	25 27	syl	$⊢ ((G \in Grp \land I \in V) \land (y \in I \land z \in I \land y \neq z)) \to (x \in I ⟼ \{\underset{˙}{0}\}) (z) = \{\underset{˙}{0}\}$
29	28	fveq2d	$⊢ ((G \in Grp \land I \in V) \land (y \in I \land z \in I \land y \neq z)) \to Cntz (G) ((x \in I ⟼ \{\underset{˙}{0}\}) (z)) = Cntz (G) (\{\underset{˙}{0}\})$
30	18 24 29	3sstr4d	$⊢ ((G \in Grp \land I \in V) \land (y \in I \land z \in I \land y \neq z)) \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) \subseteq Cntz (G) ((x \in I ⟼ \{\underset{˙}{0}\}) (z))$
31	23	adantl	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) = \{\underset{˙}{0}\}$
32	31	ineq1d	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) = \{\underset{˙}{0}\} \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}])$
33	9	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
34	33	ad2antrr	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to SubGrp (G) \in ACS ({Base}_{G})$
35	34	acsmred	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to SubGrp (G) \in Moore ({Base}_{G})$
36		imassrn	$⊢ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}] \subseteq ran (x \in I ⟼ \{\underset{˙}{0}\})$
37	8	adantr	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to (x \in I ⟼ \{\underset{˙}{0}\}) : I ⟶ SubGrp (G)$
38	37	frnd	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to ran (x \in I ⟼ \{\underset{˙}{0}\}) \subseteq SubGrp (G)$
39		mresspw	$⊢ SubGrp (G) \in Moore ({Base}_{G}) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
40	35 39	syl	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
41	38 40	sstrd	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to ran (x \in I ⟼ \{\underset{˙}{0}\}) \subseteq 𝒫 {Base}_{G}$
42	36 41	sstrid	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}] \subseteq 𝒫 {Base}_{G}$
43		sspwuni	$⊢ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}] \subseteq {Base}_{G}$
44	42 43	sylib	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to ⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}] \subseteq {Base}_{G}$
45	3	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}] \subseteq {Base}_{G}) \to mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) \in SubGrp (G)$
46	35 44 45	syl2anc	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) \in SubGrp (G)$
47	1	subg0cl	$⊢ mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) \in SubGrp (G) \to \underset{˙}{0} \in mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}])$
48	46 47	syl	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to \underset{˙}{0} \in mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}])$
49	48	snssd	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to \{\underset{˙}{0}\} \subseteq mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}])$
50		df-ss	$⊢ \{\underset{˙}{0}\} \subseteq mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) \leftrightarrow \{\underset{˙}{0}\} \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) = \{\underset{˙}{0}\}$
51	49 50	sylib	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to \{\underset{˙}{0}\} \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) = \{\underset{˙}{0}\}$
52	32 51	eqtrd	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) = \{\underset{˙}{0}\}$
53		eqimss	$⊢ (x \in I ⟼ \{\underset{˙}{0}\}) (y) \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) = \{\underset{˙}{0}\} \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) \subseteq \{\underset{˙}{0}\}$
54	52 53	syl	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) \cap mrCls (SubGrp (G)) (⋃ (x \in I ⟼ \{\underset{˙}{0}\}) [I ∖ \{y\}]) \subseteq \{\underset{˙}{0}\}$
55	2 1 3 4 5 8 30 54	dmdprdd	$⊢ (G \in Grp \land I \in V) \to G dom DProd (x \in I ⟼ \{\underset{˙}{0}\})$
56	21 7	dmmptd	$⊢ (G \in Grp \land I \in V) \to dom (x \in I ⟼ \{\underset{˙}{0}\}) = I$
57	6	adantr	$⊢ (G \in Grp \land I \in V) \to \{\underset{˙}{0}\} \in SubGrp (G)$
58		eqimss	$⊢ (x \in I ⟼ \{\underset{˙}{0}\}) (y) = \{\underset{˙}{0}\} \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) \subseteq \{\underset{˙}{0}\}$
59	31 58	syl	$⊢ ((G \in Grp \land I \in V) \land y \in I) \to (x \in I ⟼ \{\underset{˙}{0}\}) (y) \subseteq \{\underset{˙}{0}\}$
60	55 56 57 59	dprdlub	$⊢ (G \in Grp \land I \in V) \to G DProd (x \in I ⟼ \{\underset{˙}{0}\}) \subseteq \{\underset{˙}{0}\}$
61		dprdsubg	$⊢ G dom DProd (x \in I ⟼ \{\underset{˙}{0}\}) \to G DProd (x \in I ⟼ \{\underset{˙}{0}\}) \in SubGrp (G)$
62	1	subg0cl	$⊢ G DProd (x \in I ⟼ \{\underset{˙}{0}\}) \in SubGrp (G) \to \underset{˙}{0} \in (G DProd (x \in I ⟼ \{\underset{˙}{0}\}))$
63	55 61 62	3syl	$⊢ (G \in Grp \land I \in V) \to \underset{˙}{0} \in (G DProd (x \in I ⟼ \{\underset{˙}{0}\}))$
64	63	snssd	$⊢ (G \in Grp \land I \in V) \to \{\underset{˙}{0}\} \subseteq G DProd (x \in I ⟼ \{\underset{˙}{0}\})$
65	60 64	eqssd	$⊢ (G \in Grp \land I \in V) \to G DProd (x \in I ⟼ \{\underset{˙}{0}\}) = \{\underset{˙}{0}\}$
66	55 65	jca	$⊢ (G \in Grp \land I \in V) \to (G dom DProd (x \in I ⟼ \{\underset{˙}{0}\}) \land G DProd (x \in I ⟼ \{\underset{˙}{0}\}) = \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem dprdz

Proof