dprdres

Description: Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdres.1	$⊢ φ \to G dom DProd S$
	dprdres.2	$⊢ φ \to dom S = I$
	dprdres.3	$⊢ φ \to A \subseteq I$
Assertion	dprdres	$⊢ φ \to (G dom DProd ({S ↾}_{A}) \land G DProd ({S ↾}_{A}) \subseteq G DProd S)$

Proof

Step	Hyp	Ref	Expression
1		dprdres.1	$⊢ φ \to G dom DProd S$
2		dprdres.2	$⊢ φ \to dom S = I$
3		dprdres.3	$⊢ φ \to A \subseteq I$
4		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
5	1 4	syl	$⊢ φ \to G \in Grp$
6	1 2	dprdf2	$⊢ φ \to S : I ⟶ SubGrp (G)$
7	6 3	fssresd	$⊢ φ \to ({S ↾}_{A}) : A ⟶ SubGrp (G)$
8	1	ad2antrr	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to G dom DProd S$
9	2	ad2antrr	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to dom S = I$
10	3	ad2antrr	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to A \subseteq I$
11		simplr	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to x \in A$
12	10 11	sseldd	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to x \in I$
13		eldifi	$⊢ y \in (A ∖ \{x\}) \to y \in A$
14	13	adantl	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to y \in A$
15	10 14	sseldd	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to y \in I$
16		eldifsni	$⊢ y \in (A ∖ \{x\}) \to y \neq x$
17	16	adantl	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to y \neq x$
18	17	necomd	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to x \neq y$
19		eqid	$⊢ Cntz (G) = Cntz (G)$
20	8 9 12 15 18 19	dprdcntz	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to S (x) \subseteq Cntz (G) (S (y))$
21	11	fvresd	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to ({S ↾}_{A}) (x) = S (x)$
22	14	fvresd	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to ({S ↾}_{A}) (y) = S (y)$
23	22	fveq2d	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to Cntz (G) (({S ↾}_{A}) (y)) = Cntz (G) (S (y))$
24	20 21 23	3sstr4d	$⊢ ((φ \land x \in A) \land y \in (A ∖ \{x\})) \to ({S ↾}_{A}) (x) \subseteq Cntz (G) (({S ↾}_{A}) (y))$
25	24	ralrimiva	$⊢ (φ \land x \in A) \to \forall y \in (A ∖ \{x\}) ({S ↾}_{A}) (x) \subseteq Cntz (G) (({S ↾}_{A}) (y))$
26		fvres	$⊢ x \in A \to ({S ↾}_{A}) (x) = S (x)$
27	26	adantl	$⊢ (φ \land x \in A) \to ({S ↾}_{A}) (x) = S (x)$
28	27	ineq1d	$⊢ (φ \land x \in A) \to ({S ↾}_{A}) (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) = S (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}])$
29		eqid	$⊢ {Base}_{G} = {Base}_{G}$
30	29	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
31		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
32	5 30 31	3syl	$⊢ φ \to SubGrp (G) \in Moore ({Base}_{G})$
33	32	adantr	$⊢ (φ \land x \in A) \to SubGrp (G) \in Moore ({Base}_{G})$
34		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
35		resss	$⊢ {S ↾}_{A} \subseteq S$
36		imass1	$⊢ {S ↾}_{A} \subseteq S \to ({S ↾}_{A}) [A ∖ \{x\}] \subseteq S [A ∖ \{x\}]$
37	35 36	ax-mp	$⊢ ({S ↾}_{A}) [A ∖ \{x\}] \subseteq S [A ∖ \{x\}]$
38	3	adantr	$⊢ (φ \land x \in A) \to A \subseteq I$
39		ssdif	$⊢ A \subseteq I \to A ∖ \{x\} \subseteq I ∖ \{x\}$
40		imass2	$⊢ A ∖ \{x\} \subseteq I ∖ \{x\} \to S [A ∖ \{x\}] \subseteq S [I ∖ \{x\}]$
41	38 39 40	3syl	$⊢ (φ \land x \in A) \to S [A ∖ \{x\}] \subseteq S [I ∖ \{x\}]$
42	37 41	sstrid	$⊢ (φ \land x \in A) \to ({S ↾}_{A}) [A ∖ \{x\}] \subseteq S [I ∖ \{x\}]$
43	42	unissd	$⊢ (φ \land x \in A) \to ⋃ ({S ↾}_{A}) [A ∖ \{x\}] \subseteq ⋃ S [I ∖ \{x\}]$
44		imassrn	$⊢ S [I ∖ \{x\}] \subseteq ran S$
45	6	frnd	$⊢ φ \to ran S \subseteq SubGrp (G)$
46	29	subgss	$⊢ x \in SubGrp (G) \to x \subseteq {Base}_{G}$
47		velpw	$⊢ x \in 𝒫 {Base}_{G} \leftrightarrow x \subseteq {Base}_{G}$
48	46 47	sylibr	$⊢ x \in SubGrp (G) \to x \in 𝒫 {Base}_{G}$
49	48	ssriv	$⊢ SubGrp (G) \subseteq 𝒫 {Base}_{G}$
50	45 49	sstrdi	$⊢ φ \to ran S \subseteq 𝒫 {Base}_{G}$
51	50	adantr	$⊢ (φ \land x \in A) \to ran S \subseteq 𝒫 {Base}_{G}$
52	44 51	sstrid	$⊢ (φ \land x \in A) \to S [I ∖ \{x\}] \subseteq 𝒫 {Base}_{G}$
53		sspwuni	$⊢ S [I ∖ \{x\}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ S [I ∖ \{x\}] \subseteq {Base}_{G}$
54	52 53	sylib	$⊢ (φ \land x \in A) \to ⋃ S [I ∖ \{x\}] \subseteq {Base}_{G}$
55	33 34 43 54	mrcssd	$⊢ (φ \land x \in A) \to mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \subseteq mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}])$
56		sslin	$⊢ mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \subseteq mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}]) \to S (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \subseteq S (x) \cap mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}])$
57	55 56	syl	$⊢ (φ \land x \in A) \to S (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \subseteq S (x) \cap mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}])$
58	1	adantr	$⊢ (φ \land x \in A) \to G dom DProd S$
59	2	adantr	$⊢ (φ \land x \in A) \to dom S = I$
60	3	sselda	$⊢ (φ \land x \in A) \to x \in I$
61		eqid	$⊢ 0_{G} = 0_{G}$
62	58 59 60 61 34	dprddisj	$⊢ (φ \land x \in A) \to S (x) \cap mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}]) = \{0_{G}\}$
63	57 62	sseqtrd	$⊢ (φ \land x \in A) \to S (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \subseteq \{0_{G}\}$
64	6	ffvelcdmda	$⊢ (φ \land x \in I) \to S (x) \in SubGrp (G)$
65	60 64	syldan	$⊢ (φ \land x \in A) \to S (x) \in SubGrp (G)$
66	61	subg0cl	$⊢ S (x) \in SubGrp (G) \to 0_{G} \in S (x)$
67	65 66	syl	$⊢ (φ \land x \in A) \to 0_{G} \in S (x)$
68	43 54	sstrd	$⊢ (φ \land x \in A) \to ⋃ ({S ↾}_{A}) [A ∖ \{x\}] \subseteq {Base}_{G}$
69	34	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ ({S ↾}_{A}) [A ∖ \{x\}] \subseteq {Base}_{G}) \to mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \in SubGrp (G)$
70	33 68 69	syl2anc	$⊢ (φ \land x \in A) \to mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \in SubGrp (G)$
71	61	subg0cl	$⊢ mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) \in SubGrp (G) \to 0_{G} \in mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}])$
72	70 71	syl	$⊢ (φ \land x \in A) \to 0_{G} \in mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}])$
73	67 72	elind	$⊢ (φ \land x \in A) \to 0_{G} \in (S (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]))$
74	73	snssd	$⊢ (φ \land x \in A) \to \{0_{G}\} \subseteq S (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}])$
75	63 74	eqssd	$⊢ (φ \land x \in A) \to S (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) = \{0_{G}\}$
76	28 75	eqtrd	$⊢ (φ \land x \in A) \to ({S ↾}_{A}) (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) = \{0_{G}\}$
77	25 76	jca	$⊢ (φ \land x \in A) \to (\forall y \in (A ∖ \{x\}) ({S ↾}_{A}) (x) \subseteq Cntz (G) (({S ↾}_{A}) (y)) \land ({S ↾}_{A}) (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) = \{0_{G}\})$
78	77	ralrimiva	$⊢ φ \to \forall x \in A (\forall y \in (A ∖ \{x\}) ({S ↾}_{A}) (x) \subseteq Cntz (G) (({S ↾}_{A}) (y)) \land ({S ↾}_{A}) (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) = \{0_{G}\})$
79	1 2	dprddomcld	$⊢ φ \to I \in V$
80	79 3	ssexd	$⊢ φ \to A \in V$
81	7	fdmd	$⊢ φ \to dom ({S ↾}_{A}) = A$
82	19 61 34	dmdprd	$⊢ (A \in V \land dom ({S ↾}_{A}) = A) \to (G dom DProd ({S ↾}_{A}) \leftrightarrow (G \in Grp \land ({S ↾}_{A}) : A ⟶ SubGrp (G) \land \forall x \in A (\forall y \in (A ∖ \{x\}) ({S ↾}_{A}) (x) \subseteq Cntz (G) (({S ↾}_{A}) (y)) \land ({S ↾}_{A}) (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) = \{0_{G}\})))$
83	80 81 82	syl2anc	$⊢ φ \to (G dom DProd ({S ↾}_{A}) \leftrightarrow (G \in Grp \land ({S ↾}_{A}) : A ⟶ SubGrp (G) \land \forall x \in A (\forall y \in (A ∖ \{x\}) ({S ↾}_{A}) (x) \subseteq Cntz (G) (({S ↾}_{A}) (y)) \land ({S ↾}_{A}) (x) \cap mrCls (SubGrp (G)) (⋃ ({S ↾}_{A}) [A ∖ \{x\}]) = \{0_{G}\})))$
84	5 7 78 83	mpbir3and	$⊢ φ \to G dom DProd ({S ↾}_{A})$
85		rnss	$⊢ {S ↾}_{A} \subseteq S \to ran ({S ↾}_{A}) \subseteq ran S$
86		uniss	$⊢ ran ({S ↾}_{A}) \subseteq ran S \to ⋃ ran ({S ↾}_{A}) \subseteq ⋃ ran S$
87	35 85 86	mp2b	$⊢ ⋃ ran ({S ↾}_{A}) \subseteq ⋃ ran S$
88	87	a1i	$⊢ φ \to ⋃ ran ({S ↾}_{A}) \subseteq ⋃ ran S$
89		sspwuni	$⊢ ran S \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ ran S \subseteq {Base}_{G}$
90	50 89	sylib	$⊢ φ \to ⋃ ran S \subseteq {Base}_{G}$
91	32 34 88 90	mrcssd	$⊢ φ \to mrCls (SubGrp (G)) (⋃ ran ({S ↾}_{A})) \subseteq mrCls (SubGrp (G)) (⋃ ran S)$
92	34	dprdspan	$⊢ G dom DProd ({S ↾}_{A}) \to G DProd ({S ↾}_{A}) = mrCls (SubGrp (G)) (⋃ ran ({S ↾}_{A}))$
93	84 92	syl	$⊢ φ \to G DProd ({S ↾}_{A}) = mrCls (SubGrp (G)) (⋃ ran ({S ↾}_{A}))$
94	34	dprdspan	$⊢ G dom DProd S \to G DProd S = mrCls (SubGrp (G)) (⋃ ran S)$
95	1 94	syl	$⊢ φ \to G DProd S = mrCls (SubGrp (G)) (⋃ ran S)$
96	91 93 95	3sstr4d	$⊢ φ \to G DProd ({S ↾}_{A}) \subseteq G DProd S$
97	84 96	jca	$⊢ φ \to (G dom DProd ({S ↾}_{A}) \land G DProd ({S ↾}_{A}) \subseteq G DProd S)$

Metamath Proof Explorer

Theorem dprdres

Proof