dprdss

Description: Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdss.1	$⊢ φ \to G dom DProd T$
	dprdss.2	$⊢ φ \to dom T = I$
	dprdss.3	$⊢ φ \to S : I ⟶ SubGrp (G)$
	dprdss.4	$⊢ (φ \land k \in I) \to S (k) \subseteq T (k)$
Assertion	dprdss	$⊢ φ \to (G dom DProd S \land G DProd S \subseteq G DProd T)$

Proof

Step	Hyp	Ref	Expression
1		dprdss.1	$⊢ φ \to G dom DProd T$
2		dprdss.2	$⊢ φ \to dom T = I$
3		dprdss.3	$⊢ φ \to S : I ⟶ SubGrp (G)$
4		dprdss.4	$⊢ (φ \land k \in I) \to S (k) \subseteq T (k)$
5		eqid	$⊢ Cntz (G) = Cntz (G)$
6		eqid	$⊢ 0_{G} = 0_{G}$
7		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
8		dprdgrp	$⊢ G dom DProd T \to G \in Grp$
9	1 8	syl	$⊢ φ \to G \in Grp$
10	1 2	dprddomcld	$⊢ φ \to I \in V$
11	4	ralrimiva	$⊢ φ \to \forall k \in I S (k) \subseteq T (k)$
12		fveq2	$⊢ k = x \to S (k) = S (x)$
13		fveq2	$⊢ k = x \to T (k) = T (x)$
14	12 13	sseq12d	$⊢ k = x \to (S (k) \subseteq T (k) \leftrightarrow S (x) \subseteq T (x))$
15	14	rspcv	$⊢ x \in I \to (\forall k \in I S (k) \subseteq T (k) \to S (x) \subseteq T (x))$
16	11 15	mpan9	$⊢ (φ \land x \in I) \to S (x) \subseteq T (x)$
17	16	3ad2antr1	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to S (x) \subseteq T (x)$
18	1	adantr	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to G dom DProd T$
19	2	adantr	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to dom T = I$
20		simpr1	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to x \in I$
21		simpr2	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to y \in I$
22		simpr3	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to x \neq y$
23	18 19 20 21 22 5	dprdcntz	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to T (x) \subseteq Cntz (G) (T (y))$
24	1 2	dprdf2	$⊢ φ \to T : I ⟶ SubGrp (G)$
25	24	adantr	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to T : I ⟶ SubGrp (G)$
26	25 21	ffvelcdmd	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to T (y) \in SubGrp (G)$
27		eqid	$⊢ {Base}_{G} = {Base}_{G}$
28	27	subgss	$⊢ T (y) \in SubGrp (G) \to T (y) \subseteq {Base}_{G}$
29	26 28	syl	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to T (y) \subseteq {Base}_{G}$
30		fveq2	$⊢ k = y \to S (k) = S (y)$
31		fveq2	$⊢ k = y \to T (k) = T (y)$
32	30 31	sseq12d	$⊢ k = y \to (S (k) \subseteq T (k) \leftrightarrow S (y) \subseteq T (y))$
33	11	adantr	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to \forall k \in I S (k) \subseteq T (k)$
34	32 33 21	rspcdva	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to S (y) \subseteq T (y)$
35	27 5	cntz2ss	$⊢ (T (y) \subseteq {Base}_{G} \land S (y) \subseteq T (y)) \to Cntz (G) (T (y)) \subseteq Cntz (G) (S (y))$
36	29 34 35	syl2anc	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to Cntz (G) (T (y)) \subseteq Cntz (G) (S (y))$
37	23 36	sstrd	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to T (x) \subseteq Cntz (G) (S (y))$
38	17 37	sstrd	$⊢ (φ \land (x \in I \land y \in I \land x \neq y)) \to S (x) \subseteq Cntz (G) (S (y))$
39	9	adantr	$⊢ (φ \land x \in I) \to G \in Grp$
40	27	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
41		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
42	39 40 41	3syl	$⊢ (φ \land x \in I) \to SubGrp (G) \in Moore ({Base}_{G})$
43		difss	$⊢ I ∖ \{x\} \subseteq I$
44	11	adantr	$⊢ (φ \land x \in I) \to \forall k \in I S (k) \subseteq T (k)$
45		ssralv	$⊢ I ∖ \{x\} \subseteq I \to (\forall k \in I S (k) \subseteq T (k) \to \forall k \in (I ∖ \{x\}) S (k) \subseteq T (k))$
46	43 44 45	mpsyl	$⊢ (φ \land x \in I) \to \forall k \in (I ∖ \{x\}) S (k) \subseteq T (k)$
47		ss2iun	$⊢ \forall k \in (I ∖ \{x\}) S (k) \subseteq T (k) \to ⋃_{k \in I ∖ \{x\}} S (k) \subseteq ⋃_{k \in I ∖ \{x\}} T (k)$
48	46 47	syl	$⊢ (φ \land x \in I) \to ⋃_{k \in I ∖ \{x\}} S (k) \subseteq ⋃_{k \in I ∖ \{x\}} T (k)$
49	3	adantr	$⊢ (φ \land x \in I) \to S : I ⟶ SubGrp (G)$
50		ffun	$⊢ S : I ⟶ SubGrp (G) \to Fun S$
51		funiunfv	$⊢ Fun S \to ⋃_{k \in I ∖ \{x\}} S (k) = ⋃ S [I ∖ \{x\}]$
52	49 50 51	3syl	$⊢ (φ \land x \in I) \to ⋃_{k \in I ∖ \{x\}} S (k) = ⋃ S [I ∖ \{x\}]$
53	24	adantr	$⊢ (φ \land x \in I) \to T : I ⟶ SubGrp (G)$
54		ffun	$⊢ T : I ⟶ SubGrp (G) \to Fun T$
55		funiunfv	$⊢ Fun T \to ⋃_{k \in I ∖ \{x\}} T (k) = ⋃ T [I ∖ \{x\}]$
56	53 54 55	3syl	$⊢ (φ \land x \in I) \to ⋃_{k \in I ∖ \{x\}} T (k) = ⋃ T [I ∖ \{x\}]$
57	48 52 56	3sstr3d	$⊢ (φ \land x \in I) \to ⋃ S [I ∖ \{x\}] \subseteq ⋃ T [I ∖ \{x\}]$
58		imassrn	$⊢ T [I ∖ \{x\}] \subseteq ran T$
59	53	frnd	$⊢ (φ \land x \in I) \to ran T \subseteq SubGrp (G)$
60		mresspw	$⊢ SubGrp (G) \in Moore ({Base}_{G}) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
61	42 60	syl	$⊢ (φ \land x \in I) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
62	59 61	sstrd	$⊢ (φ \land x \in I) \to ran T \subseteq 𝒫 {Base}_{G}$
63	58 62	sstrid	$⊢ (φ \land x \in I) \to T [I ∖ \{x\}] \subseteq 𝒫 {Base}_{G}$
64		sspwuni	$⊢ T [I ∖ \{x\}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ T [I ∖ \{x\}] \subseteq {Base}_{G}$
65	63 64	sylib	$⊢ (φ \land x \in I) \to ⋃ T [I ∖ \{x\}] \subseteq {Base}_{G}$
66	42 7 57 65	mrcssd	$⊢ (φ \land x \in I) \to mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}]) \subseteq mrCls (SubGrp (G)) (⋃ T [I ∖ \{x\}])$
67		ss2in	$⊢ (S (x) \subseteq T (x) \land mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}]) \subseteq mrCls (SubGrp (G)) (⋃ T [I ∖ \{x\}])) \to S (x) \cap mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}]) \subseteq T (x) \cap mrCls (SubGrp (G)) (⋃ T [I ∖ \{x\}])$
68	16 66 67	syl2anc	$⊢ (φ \land x \in I) \to S (x) \cap mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}]) \subseteq T (x) \cap mrCls (SubGrp (G)) (⋃ T [I ∖ \{x\}])$
69	1	adantr	$⊢ (φ \land x \in I) \to G dom DProd T$
70	2	adantr	$⊢ (φ \land x \in I) \to dom T = I$
71		simpr	$⊢ (φ \land x \in I) \to x \in I$
72	69 70 71 6 7	dprddisj	$⊢ (φ \land x \in I) \to T (x) \cap mrCls (SubGrp (G)) (⋃ T [I ∖ \{x\}]) = \{0_{G}\}$
73	68 72	sseqtrd	$⊢ (φ \land x \in I) \to S (x) \cap mrCls (SubGrp (G)) (⋃ S [I ∖ \{x\}]) \subseteq \{0_{G}\}$
74	5 6 7 9 10 3 38 73	dmdprdd	$⊢ φ \to G dom DProd S$
75	1	a1d	$⊢ φ \to (G dom DProd S \to G dom DProd T)$
76		ss2ixp	$⊢ \forall k \in I S (k) \subseteq T (k) \to \underset{k \in I}{⨉} S (k) \subseteq \underset{k \in I}{⨉} T (k)$
77	11 76	syl	$⊢ φ \to \underset{k \in I}{⨉} S (k) \subseteq \underset{k \in I}{⨉} T (k)$
78		rabss2	$⊢ \underset{k \in I}{⨉} S (k) \subseteq \underset{k \in I}{⨉} T (k) \to \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} \subseteq \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\}$
79		ssrexv	$⊢ \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} \subseteq \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\} \to (\exists f \in \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f \to \exists f \in \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f)$
80	77 78 79	3syl	$⊢ φ \to (\exists f \in \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f \to \exists f \in \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f)$
81	75 80	anim12d	$⊢ φ \to ((G dom DProd S \land \exists f \in \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f) \to (G dom DProd T \land \exists f \in \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f))$
82		fdm	$⊢ S : I ⟶ SubGrp (G) \to dom S = I$
83		eqid	$⊢ \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} = \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\}$
84	6 83	eldprd	$⊢ dom S = I \to (a \in (G DProd S) \leftrightarrow (G dom DProd S \land \exists f \in \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f))$
85	3 82 84	3syl	$⊢ φ \to (a \in (G DProd S) \leftrightarrow (G dom DProd S \land \exists f \in \{h \in \underset{k \in I}{⨉} S (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f))$
86		eqid	$⊢ \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\} = \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\}$
87	6 86	eldprd	$⊢ dom T = I \to (a \in (G DProd T) \leftrightarrow (G dom DProd T \land \exists f \in \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f))$
88	2 87	syl	$⊢ φ \to (a \in (G DProd T) \leftrightarrow (G dom DProd T \land \exists f \in \{h \in \underset{k \in I}{⨉} T (k) \| {finSupp}_{0_{G}} (h)\} a = \sum_{G} f))$
89	81 85 88	3imtr4d	$⊢ φ \to (a \in (G DProd S) \to a \in (G DProd T))$
90	89	ssrdv	$⊢ φ \to G DProd S \subseteq G DProd T$
91	74 90	jca	$⊢ φ \to (G dom DProd S \land G DProd S \subseteq G DProd T)$

Metamath Proof Explorer

Theorem dprdss

Proof