dprd2dlem2

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))$
Assertion	dprd2dlem2	$⊢ (φ \land X \in A) \to S (X) \subseteq G DProd (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) 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		df-ov	$⊢ 1^{st} (X) S 2^{nd} (X) = S (⟨1^{st} (X), 2^{nd} (X)⟩)$
8		1st2nd	$⊢ (Rel A \land X \in A) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
9	1 8	sylan	$⊢ (φ \land X \in A) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
10		simpr	$⊢ (φ \land X \in A) \to X \in A$
11	9 10	eqeltrrd	$⊢ (φ \land X \in A) \to ⟨1^{st} (X), 2^{nd} (X)⟩ \in A$
12		df-br	$⊢ 1^{st} (X) A 2^{nd} (X) \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in A$
13	11 12	sylibr	$⊢ (φ \land X \in A) \to 1^{st} (X) A 2^{nd} (X)$
14	1	adantr	$⊢ (φ \land X \in A) \to Rel A$
15		elrelimasn	$⊢ Rel A \to (2^{nd} (X) \in A [\{1^{st} (X)\}] \leftrightarrow 1^{st} (X) A 2^{nd} (X))$
16	14 15	syl	$⊢ (φ \land X \in A) \to (2^{nd} (X) \in A [\{1^{st} (X)\}] \leftrightarrow 1^{st} (X) A 2^{nd} (X))$
17	13 16	mpbird	$⊢ (φ \land X \in A) \to 2^{nd} (X) \in A [\{1^{st} (X)\}]$
18		oveq2	$⊢ j = 2^{nd} (X) \to 1^{st} (X) S j = 1^{st} (X) S 2^{nd} (X)$
19		eqid	$⊢ (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j) = (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j)$
20		ovex	$⊢ 1^{st} (X) S j \in V$
21	18 19 20	fvmpt3i	$⊢ 2^{nd} (X) \in A [\{1^{st} (X)\}] \to (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j) (2^{nd} (X)) = 1^{st} (X) S 2^{nd} (X)$
22	17 21	syl	$⊢ (φ \land X \in A) \to (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j) (2^{nd} (X)) = 1^{st} (X) S 2^{nd} (X)$
23	9	fveq2d	$⊢ (φ \land X \in A) \to S (X) = S (⟨1^{st} (X), 2^{nd} (X)⟩)$
24	7 22 23	3eqtr4a	$⊢ (φ \land X \in A) \to (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j) (2^{nd} (X)) = S (X)$
25		sneq	$⊢ i = 1^{st} (X) \to \{i\} = \{1^{st} (X)\}$
26	25	imaeq2d	$⊢ i = 1^{st} (X) \to A [\{i\}] = A [\{1^{st} (X)\}]$
27		oveq1	$⊢ i = 1^{st} (X) \to i S j = 1^{st} (X) S j$
28	26 27	mpteq12dv	$⊢ i = 1^{st} (X) \to (j \in A [\{i\}] ⟼ i S j) = (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j)$
29	28	breq2d	$⊢ i = 1^{st} (X) \to (G dom DProd (j \in A [\{i\}] ⟼ i S j) \leftrightarrow G dom DProd (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j))$
30	4	ralrimiva	$⊢ φ \to \forall i \in I G dom DProd (j \in A [\{i\}] ⟼ i S j)$
31	30	adantr	$⊢ (φ \land X \in A) \to \forall i \in I G dom DProd (j \in A [\{i\}] ⟼ i S j)$
32	3	adantr	$⊢ (φ \land X \in A) \to dom A \subseteq I$
33		1stdm	$⊢ (Rel A \land X \in A) \to 1^{st} (X) \in dom A$
34	1 33	sylan	$⊢ (φ \land X \in A) \to 1^{st} (X) \in dom A$
35	32 34	sseldd	$⊢ (φ \land X \in A) \to 1^{st} (X) \in I$
36	29 31 35	rspcdva	$⊢ (φ \land X \in A) \to G dom DProd (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j)$
37	20 19	dmmpti	$⊢ dom (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j) = A [\{1^{st} (X)\}]$
38	37	a1i	$⊢ (φ \land X \in A) \to dom (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j) = A [\{1^{st} (X)\}]$
39	36 38 17	dprdub	$⊢ (φ \land X \in A) \to (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j) (2^{nd} (X)) \subseteq G DProd (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j)$
40	24 39	eqsstrrd	$⊢ (φ \land X \in A) \to S (X) \subseteq G DProd (j \in A [\{1^{st} (X)\}] ⟼ 1^{st} (X) S j)$

Metamath Proof Explorer

Theorem dprd2dlem2

Proof