dprd2dlem1

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dprd2d.1	$⊢ φ \to Rel A$
	dprd2d.2	$⊢ φ \to S : A ⟶ SubGrp (G)$
	dprd2d.3	$⊢ φ \to dom A \subseteq I$
	dprd2d.4	$⊢ (φ \land i \in I) \to G dom DProd (j \in A [\{i\}] ⟼ i S j)$
	dprd2d.5	$⊢ φ \to G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
	dprd2d.k	$⊢ K = mrCls (SubGrp (G))$
	dprd2d.6	$⊢ φ \to C \subseteq I$
Assertion	dprd2dlem1	$⊢ φ \to K (⋃ S [{A ↾}_{C}]) = G DProd (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$

Proof

Step	Hyp	Ref	Expression
1		dprd2d.1	$⊢ φ \to Rel A$
2		dprd2d.2	$⊢ φ \to S : A ⟶ SubGrp (G)$
3		dprd2d.3	$⊢ φ \to dom A \subseteq I$
4		dprd2d.4	$⊢ (φ \land i \in I) \to G dom DProd (j \in A [\{i\}] ⟼ i S j)$
5		dprd2d.5	$⊢ φ \to G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
6		dprd2d.k	$⊢ K = mrCls (SubGrp (G))$
7		dprd2d.6	$⊢ φ \to C \subseteq I$
8		dprdgrp	$⊢ G dom DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \to G \in Grp$
9	5 8	syl	$⊢ φ \to G \in Grp$
10		eqid	$⊢ {Base}_{G} = {Base}_{G}$
11	10	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
12		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
13	9 11 12	3syl	$⊢ φ \to SubGrp (G) \in Moore ({Base}_{G})$
14		ffun	$⊢ S : A ⟶ SubGrp (G) \to Fun S$
15		funiunfv	$⊢ Fun S \to ⋃_{x \in {A ↾}_{C}} S (x) = ⋃ S [{A ↾}_{C}]$
16	2 14 15	3syl	$⊢ φ \to ⋃_{x \in {A ↾}_{C}} S (x) = ⋃ S [{A ↾}_{C}]$
17		resss	$⊢ {A ↾}_{C} \subseteq A$
18	17	sseli	$⊢ x \in ({A ↾}_{C}) \to x \in A$
19	1 2 3 4 5 6	dprd2dlem2	$⊢ (φ \land x \in A) \to S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
20	18 19	sylan2	$⊢ (φ \land x \in ({A ↾}_{C})) \to S (x) \subseteq G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
21		1st2nd	$⊢ (Rel A \land x \in A) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
22	1 18 21	syl2an	$⊢ (φ \land x \in ({A ↾}_{C})) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
23		simpr	$⊢ (φ \land x \in ({A ↾}_{C})) \to x \in ({A ↾}_{C})$
24	22 23	eqeltrrd	$⊢ (φ \land x \in ({A ↾}_{C})) \to ⟨1^{st} (x), 2^{nd} (x)⟩ \in ({A ↾}_{C})$
25		fvex	$⊢ 2^{nd} (x) \in V$
26	25	opelresi	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in ({A ↾}_{C}) \leftrightarrow (1^{st} (x) \in C \land ⟨1^{st} (x), 2^{nd} (x)⟩ \in A)$
27	26	simplbi	$⊢ ⟨1^{st} (x), 2^{nd} (x)⟩ \in ({A ↾}_{C}) \to 1^{st} (x) \in C$
28	24 27	syl	$⊢ (φ \land x \in ({A ↾}_{C})) \to 1^{st} (x) \in C$
29		ovex	$⊢ G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in V$
30		eqid	$⊢ (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
31		sneq	$⊢ i = 1^{st} (x) \to \{i\} = \{1^{st} (x)\}$
32	31	imaeq2d	$⊢ i = 1^{st} (x) \to A [\{i\}] = A [\{1^{st} (x)\}]$
33		oveq1	$⊢ i = 1^{st} (x) \to i S j = 1^{st} (x) S j$
34	32 33	mpteq12dv	$⊢ i = 1^{st} (x) \to (j \in A [\{i\}] ⟼ i S j) = (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
35	34	oveq2d	$⊢ i = 1^{st} (x) \to G DProd (j \in A [\{i\}] ⟼ i S j) = G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j)$
36	30 35	elrnmpt1s	$⊢ (1^{st} (x) \in C \land G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in V) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
37	28 29 36	sylancl	$⊢ (φ \land x \in ({A ↾}_{C})) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
38		elssuni	$⊢ G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \in ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
39	37 38	syl	$⊢ (φ \land x \in ({A ↾}_{C})) \to G DProd (j \in A [\{1^{st} (x)\}] ⟼ 1^{st} (x) S j) \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
40	20 39	sstrd	$⊢ (φ \land x \in ({A ↾}_{C})) \to S (x) \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
41	40	ralrimiva	$⊢ φ \to \forall x \in ({A ↾}_{C}) S (x) \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
42		iunss	$⊢ ⋃_{x \in {A ↾}_{C}} S (x) \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \leftrightarrow \forall x \in ({A ↾}_{C}) S (x) \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
43	41 42	sylibr	$⊢ φ \to ⋃_{x \in {A ↾}_{C}} S (x) \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
44	16 43	eqsstrrd	$⊢ φ \to ⋃ S [{A ↾}_{C}] \subseteq ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
45	7	sselda	$⊢ (φ \land i \in C) \to i \in I$
46	45 4	syldan	$⊢ (φ \land i \in C) \to G dom DProd (j \in A [\{i\}] ⟼ i S j)$
47		ovex	$⊢ i S j \in V$
48		eqid	$⊢ (j \in A [\{i\}] ⟼ i S j) = (j \in A [\{i\}] ⟼ i S j)$
49	47 48	dmmpti	$⊢ dom (j \in A [\{i\}] ⟼ i S j) = A [\{i\}]$
50	49	a1i	$⊢ (φ \land i \in C) \to dom (j \in A [\{i\}] ⟼ i S j) = A [\{i\}]$
51		imassrn	$⊢ S [{A ↾}_{C}] \subseteq ran S$
52	2	frnd	$⊢ φ \to ran S \subseteq SubGrp (G)$
53		mresspw	$⊢ SubGrp (G) \in Moore ({Base}_{G}) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
54	13 53	syl	$⊢ φ \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
55	52 54	sstrd	$⊢ φ \to ran S \subseteq 𝒫 {Base}_{G}$
56	51 55	sstrid	$⊢ φ \to S [{A ↾}_{C}] \subseteq 𝒫 {Base}_{G}$
57		sspwuni	$⊢ S [{A ↾}_{C}] \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ S [{A ↾}_{C}] \subseteq {Base}_{G}$
58	56 57	sylib	$⊢ φ \to ⋃ S [{A ↾}_{C}] \subseteq {Base}_{G}$
59	6	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ S [{A ↾}_{C}] \subseteq {Base}_{G}) \to K (⋃ S [{A ↾}_{C}]) \in SubGrp (G)$
60	13 58 59	syl2anc	$⊢ φ \to K (⋃ S [{A ↾}_{C}]) \in SubGrp (G)$
61	60	adantr	$⊢ (φ \land i \in C) \to K (⋃ S [{A ↾}_{C}]) \in SubGrp (G)$
62		oveq2	$⊢ j = k \to i S j = i S k$
63	62 48 47	fvmpt3i	$⊢ k \in A [\{i\}] \to (j \in A [\{i\}] ⟼ i S j) (k) = i S k$
64	63	adantl	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to (j \in A [\{i\}] ⟼ i S j) (k) = i S k$
65		df-ov	$⊢ i S k = S (⟨i, k⟩)$
66	2	ffnd	$⊢ φ \to S Fn A$
67	66	ad2antrr	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to S Fn A$
68	17	a1i	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to {A ↾}_{C} \subseteq A$
69		simplr	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to i \in C$
70		elrelimasn	$⊢ Rel A \to (k \in A [\{i\}] \leftrightarrow i A k)$
71	1 70	syl	$⊢ φ \to (k \in A [\{i\}] \leftrightarrow i A k)$
72	71	adantr	$⊢ (φ \land i \in C) \to (k \in A [\{i\}] \leftrightarrow i A k)$
73	72	biimpa	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to i A k$
74		df-br	$⊢ i A k \leftrightarrow ⟨i, k⟩ \in A$
75	73 74	sylib	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to ⟨i, k⟩ \in A$
76		vex	$⊢ k \in V$
77	76	opelresi	$⊢ ⟨i, k⟩ \in ({A ↾}_{C}) \leftrightarrow (i \in C \land ⟨i, k⟩ \in A)$
78	69 75 77	sylanbrc	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to ⟨i, k⟩ \in ({A ↾}_{C})$
79		fnfvima	$⊢ (S Fn A \land {A ↾}_{C} \subseteq A \land ⟨i, k⟩ \in ({A ↾}_{C})) \to S (⟨i, k⟩) \in S [{A ↾}_{C}]$
80	67 68 78 79	syl3anc	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to S (⟨i, k⟩) \in S [{A ↾}_{C}]$
81	65 80	eqeltrid	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to i S k \in S [{A ↾}_{C}]$
82		elssuni	$⊢ i S k \in S [{A ↾}_{C}] \to i S k \subseteq ⋃ S [{A ↾}_{C}]$
83	81 82	syl	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to i S k \subseteq ⋃ S [{A ↾}_{C}]$
84	13 6 58	mrcssidd	$⊢ φ \to ⋃ S [{A ↾}_{C}] \subseteq K (⋃ S [{A ↾}_{C}])$
85	84	ad2antrr	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to ⋃ S [{A ↾}_{C}] \subseteq K (⋃ S [{A ↾}_{C}])$
86	83 85	sstrd	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to i S k \subseteq K (⋃ S [{A ↾}_{C}])$
87	64 86	eqsstrd	$⊢ ((φ \land i \in C) \land k \in A [\{i\}]) \to (j \in A [\{i\}] ⟼ i S j) (k) \subseteq K (⋃ S [{A ↾}_{C}])$
88	46 50 61 87	dprdlub	$⊢ (φ \land i \in C) \to G DProd (j \in A [\{i\}] ⟼ i S j) \subseteq K (⋃ S [{A ↾}_{C}])$
89		ovex	$⊢ G DProd (j \in A [\{i\}] ⟼ i S j) \in V$
90	89	elpw	$⊢ G DProd (j \in A [\{i\}] ⟼ i S j) \in 𝒫 K (⋃ S [{A ↾}_{C}]) \leftrightarrow G DProd (j \in A [\{i\}] ⟼ i S j) \subseteq K (⋃ S [{A ↾}_{C}])$
91	88 90	sylibr	$⊢ (φ \land i \in C) \to G DProd (j \in A [\{i\}] ⟼ i S j) \in 𝒫 K (⋃ S [{A ↾}_{C}])$
92	91	fmpttd	$⊢ φ \to (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) : C ⟶ 𝒫 K (⋃ S [{A ↾}_{C}])$
93	92	frnd	$⊢ φ \to ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \subseteq 𝒫 K (⋃ S [{A ↾}_{C}])$
94		sspwuni	$⊢ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \subseteq 𝒫 K (⋃ S [{A ↾}_{C}]) \leftrightarrow ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \subseteq K (⋃ S [{A ↾}_{C}])$
95	93 94	sylib	$⊢ φ \to ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \subseteq K (⋃ S [{A ↾}_{C}])$
96	13 6	mrcssvd	$⊢ φ \to K (⋃ S [{A ↾}_{C}]) \subseteq {Base}_{G}$
97	95 96	sstrd	$⊢ φ \to ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \subseteq {Base}_{G}$
98	13 6 44 97	mrcssd	$⊢ φ \to K (⋃ S [{A ↾}_{C}]) \subseteq K (⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)))$
99	6	mrcsscl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \subseteq K (⋃ S [{A ↾}_{C}]) \land K (⋃ S [{A ↾}_{C}]) \in SubGrp (G)) \to K (⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))) \subseteq K (⋃ S [{A ↾}_{C}])$
100	13 95 60 99	syl3anc	$⊢ φ \to K (⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))) \subseteq K (⋃ S [{A ↾}_{C}])$
101	98 100	eqssd	$⊢ φ \to K (⋃ S [{A ↾}_{C}]) = K (⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)))$
102		eqid	$⊢ (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
103	89 102	dmmpti	$⊢ dom (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = I$
104	103	a1i	$⊢ φ \to dom (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = I$
105	5 104 7	dprdres	$⊢ φ \to (G dom DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{C}) \land G DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{C}) \subseteq G DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)))$
106	105	simpld	$⊢ φ \to G dom DProd ({(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{C})$
107	7	resmptd	$⊢ φ \to {(i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) ↾}_{C} = (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
108	106 107	breqtrd	$⊢ φ \to G dom DProd (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
109	6	dprdspan	$⊢ G dom DProd (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) \to G DProd (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = K (⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)))$
110	108 109	syl	$⊢ φ \to G DProd (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)) = K (⋃ ran (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j)))$
111	101 110	eqtr4d	$⊢ φ \to K (⋃ S [{A ↾}_{C}]) = G DProd (i \in C ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$

Metamath Proof Explorer

Theorem dprd2dlem1

Proof