dprdcntz2

Description: The function S is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dprdcntz2.1	$⊢ φ \to G dom DProd S$
	dprdcntz2.2	$⊢ φ \to dom S = I$
	dprdcntz2.c	$⊢ φ \to C \subseteq I$
	dprdcntz2.d	$⊢ φ \to D \subseteq I$
	dprdcntz2.i	$⊢ φ \to C \cap D = \emptyset$
	dprdcntz2.z	$⊢ Z = Cntz (G)$
Assertion	dprdcntz2	$⊢ φ \to G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D}))$

Proof

Step	Hyp	Ref	Expression
1		dprdcntz2.1	$⊢ φ \to G dom DProd S$
2		dprdcntz2.2	$⊢ φ \to dom S = I$
3		dprdcntz2.c	$⊢ φ \to C \subseteq I$
4		dprdcntz2.d	$⊢ φ \to D \subseteq I$
5		dprdcntz2.i	$⊢ φ \to C \cap D = \emptyset$
6		dprdcntz2.z	$⊢ Z = Cntz (G)$
7	1 2 3	dprdres	$⊢ φ \to (G dom DProd ({S ↾}_{C}) \land G DProd ({S ↾}_{C}) \subseteq G DProd S)$
8	7	simpld	$⊢ φ \to G dom DProd ({S ↾}_{C})$
9		dmres	$⊢ dom ({S ↾}_{C}) = C \cap dom S$
10	3 2	sseqtrrd	$⊢ φ \to C \subseteq dom S$
11		df-ss	$⊢ C \subseteq dom S \leftrightarrow C \cap dom S = C$
12	10 11	sylib	$⊢ φ \to C \cap dom S = C$
13	9 12	syl5eq	$⊢ φ \to dom ({S ↾}_{C}) = C$
14		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
15	1 14	syl	$⊢ φ \to G \in Grp$
16		eqid	$⊢ {Base}_{G} = {Base}_{G}$
17	16	dprdssv	$⊢ G DProd ({S ↾}_{D}) \subseteq {Base}_{G}$
18	16 6	cntzsubg	$⊢ (G \in Grp \land G DProd ({S ↾}_{D}) \subseteq {Base}_{G}) \to Z (G DProd ({S ↾}_{D})) \in SubGrp (G)$
19	15 17 18	sylancl	$⊢ φ \to Z (G DProd ({S ↾}_{D})) \in SubGrp (G)$
20		fvres	$⊢ x \in C \to ({S ↾}_{C}) (x) = S (x)$
21	20	adantl	$⊢ (φ \land x \in C) \to ({S ↾}_{C}) (x) = S (x)$
22	1 2 4	dprdres	$⊢ φ \to (G dom DProd ({S ↾}_{D}) \land G DProd ({S ↾}_{D}) \subseteq G DProd S)$
23	22	simpld	$⊢ φ \to G dom DProd ({S ↾}_{D})$
24	23	adantr	$⊢ (φ \land x \in C) \to G dom DProd ({S ↾}_{D})$
25		dprdsubg	$⊢ G dom DProd ({S ↾}_{D}) \to G DProd ({S ↾}_{D}) \in SubGrp (G)$
26	24 25	syl	$⊢ (φ \land x \in C) \to G DProd ({S ↾}_{D}) \in SubGrp (G)$
27	3	sselda	$⊢ (φ \land x \in C) \to x \in I$
28	1 2	dprdf2	$⊢ φ \to S : I ⟶ SubGrp (G)$
29	28	ffvelrnda	$⊢ (φ \land x \in I) \to S (x) \in SubGrp (G)$
30	27 29	syldan	$⊢ (φ \land x \in C) \to S (x) \in SubGrp (G)$
31		dmres	$⊢ dom ({S ↾}_{D}) = D \cap dom S$
32	4 2	sseqtrrd	$⊢ φ \to D \subseteq dom S$
33		df-ss	$⊢ D \subseteq dom S \leftrightarrow D \cap dom S = D$
34	32 33	sylib	$⊢ φ \to D \cap dom S = D$
35	31 34	syl5eq	$⊢ φ \to dom ({S ↾}_{D}) = D$
36	35	adantr	$⊢ (φ \land x \in C) \to dom ({S ↾}_{D}) = D$
37	15	adantr	$⊢ (φ \land x \in C) \to G \in Grp$
38	16	subgss	$⊢ S (x) \in SubGrp (G) \to S (x) \subseteq {Base}_{G}$
39	30 38	syl	$⊢ (φ \land x \in C) \to S (x) \subseteq {Base}_{G}$
40	16 6	cntzsubg	$⊢ (G \in Grp \land S (x) \subseteq {Base}_{G}) \to Z (S (x)) \in SubGrp (G)$
41	37 39 40	syl2anc	$⊢ (φ \land x \in C) \to Z (S (x)) \in SubGrp (G)$
42		fvres	$⊢ y \in D \to ({S ↾}_{D}) (y) = S (y)$
43	42	adantl	$⊢ ((φ \land x \in C) \land y \in D) \to ({S ↾}_{D}) (y) = S (y)$
44	1	ad2antrr	$⊢ ((φ \land x \in C) \land y \in D) \to G dom DProd S$
45	2	ad2antrr	$⊢ ((φ \land x \in C) \land y \in D) \to dom S = I$
46	4	adantr	$⊢ (φ \land x \in C) \to D \subseteq I$
47	46	sselda	$⊢ ((φ \land x \in C) \land y \in D) \to y \in I$
48	27	adantr	$⊢ ((φ \land x \in C) \land y \in D) \to x \in I$
49		simpr	$⊢ ((φ \land x \in C) \land y \in D) \to y \in D$
50		noel	$⊢ \neg x \in \emptyset$
51		elin	$⊢ x \in (C \cap D) \leftrightarrow (x \in C \land x \in D)$
52	5	eleq2d	$⊢ φ \to (x \in (C \cap D) \leftrightarrow x \in \emptyset)$
53	51 52	syl5bbr	$⊢ φ \to ((x \in C \land x \in D) \leftrightarrow x \in \emptyset)$
54	50 53	mtbiri	$⊢ φ \to \neg (x \in C \land x \in D)$
55		imnan	$⊢ (x \in C \to \neg x \in D) \leftrightarrow \neg (x \in C \land x \in D)$
56	54 55	sylibr	$⊢ φ \to (x \in C \to \neg x \in D)$
57	56	imp	$⊢ (φ \land x \in C) \to \neg x \in D$
58	57	adantr	$⊢ ((φ \land x \in C) \land y \in D) \to \neg x \in D$
59		nelne2	$⊢ (y \in D \land \neg x \in D) \to y \neq x$
60	49 58 59	syl2anc	$⊢ ((φ \land x \in C) \land y \in D) \to y \neq x$
61	44 45 47 48 60 6	dprdcntz	$⊢ ((φ \land x \in C) \land y \in D) \to S (y) \subseteq Z (S (x))$
62	43 61	eqsstrd	$⊢ ((φ \land x \in C) \land y \in D) \to ({S ↾}_{D}) (y) \subseteq Z (S (x))$
63	24 36 41 62	dprdlub	$⊢ (φ \land x \in C) \to G DProd ({S ↾}_{D}) \subseteq Z (S (x))$
64	6 26 30 63	cntzrecd	$⊢ (φ \land x \in C) \to S (x) \subseteq Z (G DProd ({S ↾}_{D}))$
65	21 64	eqsstrd	$⊢ (φ \land x \in C) \to ({S ↾}_{C}) (x) \subseteq Z (G DProd ({S ↾}_{D}))$
66	8 13 19 65	dprdlub	$⊢ φ \to G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D}))$

Metamath Proof Explorer

Theorem dprdcntz2

Proof