dprd2db

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 25-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))$
Assertion	dprd2db	$⊢ φ \to G DProd S = G DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$

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	1 2 3 4 5 6	dprd2da	$⊢ φ \to G dom DProd S$
8	6	dprdspan	$⊢ G dom DProd S \to G DProd S = K (⋃ ran S)$
9	7 8	syl	$⊢ φ \to G DProd S = K (⋃ ran S)$
10		relssres	$⊢ (Rel A \land dom A \subseteq I) \to {A ↾}_{I} = A$
11	1 3 10	syl2anc	$⊢ φ \to {A ↾}_{I} = A$
12	11	imaeq2d	$⊢ φ \to S [{A ↾}_{I}] = S [A]$
13		ffn	$⊢ S : A ⟶ SubGrp (G) \to S Fn A$
14		fnima	$⊢ S Fn A \to S [A] = ran S$
15	2 13 14	3syl	$⊢ φ \to S [A] = ran S$
16	12 15	eqtr2d	$⊢ φ \to ran S = S [{A ↾}_{I}]$
17	16	unieqd	$⊢ φ \to ⋃ ran S = ⋃ S [{A ↾}_{I}]$
18	17	fveq2d	$⊢ φ \to K (⋃ ran S) = K (⋃ S [{A ↾}_{I}])$
19		ssidd	$⊢ φ \to I \subseteq I$
20	1 2 3 4 5 6 19	dprd2dlem1	$⊢ φ \to K (⋃ S [{A ↾}_{I}]) = G DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$
21	9 18 20	3eqtrd	$⊢ φ \to G DProd S = G DProd (i \in I ⟼ G DProd (j \in A [\{i\}] ⟼ i S j))$

Metamath Proof Explorer