dprd2d2

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

	Ref	Expression
Hypotheses	dprd2d2.1	$⊢ (φ \land (i \in I \land j \in J)) \to S \in SubGrp (G)$
	dprd2d2.2	$⊢ (φ \land i \in I) \to G dom DProd (j \in J ⟼ S)$
	dprd2d2.3	$⊢ φ \to G dom DProd (i \in I ⟼ G DProd (j \in J ⟼ S))$
Assertion	dprd2d2	$⊢ φ \to (G dom DProd (i \in I, j \in J ⟼ S) \land G DProd (i \in I, j \in J ⟼ S) = G DProd (i \in I ⟼ G DProd (j \in J ⟼ S)))$

Proof

Step	Hyp	Ref	Expression
1		dprd2d2.1	$⊢ (φ \land (i \in I \land j \in J)) \to S \in SubGrp (G)$
2		dprd2d2.2	$⊢ (φ \land i \in I) \to G dom DProd (j \in J ⟼ S)$
3		dprd2d2.3	$⊢ φ \to G dom DProd (i \in I ⟼ G DProd (j \in J ⟼ S))$
4		relxp	$⊢ Rel (\{i\} \times J)$
5	4	rgenw	$⊢ \forall i \in I Rel (\{i\} \times J)$
6		reliun	$⊢ Rel ⋃_{i \in I} (\{i\} \times J) \leftrightarrow \forall i \in I Rel (\{i\} \times J)$
7	5 6	mpbir	$⊢ Rel ⋃_{i \in I} (\{i\} \times J)$
8	7	a1i	$⊢ φ \to Rel ⋃_{i \in I} (\{i\} \times J)$
9	1	ralrimivva	$⊢ φ \to \forall i \in I \forall j \in J S \in SubGrp (G)$
10		eqid	$⊢ (i \in I, j \in J ⟼ S) = (i \in I, j \in J ⟼ S)$
11	10	fmpox	$⊢ \forall i \in I \forall j \in J S \in SubGrp (G) \leftrightarrow (i \in I, j \in J ⟼ S) : ⋃_{i \in I} (\{i\} \times J) ⟶ SubGrp (G)$
12	9 11	sylib	$⊢ φ \to (i \in I, j \in J ⟼ S) : ⋃_{i \in I} (\{i\} \times J) ⟶ SubGrp (G)$
13		dmiun	$⊢ dom ⋃_{i \in I} (\{i\} \times J) = ⋃_{i \in I} dom (\{i\} \times J)$
14		dmxpss	$⊢ dom (\{i\} \times J) \subseteq \{i\}$
15		simpr	$⊢ (φ \land i \in I) \to i \in I$
16	15	snssd	$⊢ (φ \land i \in I) \to \{i\} \subseteq I$
17	14 16	sstrid	$⊢ (φ \land i \in I) \to dom (\{i\} \times J) \subseteq I$
18	17	ralrimiva	$⊢ φ \to \forall i \in I dom (\{i\} \times J) \subseteq I$
19		iunss	$⊢ ⋃_{i \in I} dom (\{i\} \times J) \subseteq I \leftrightarrow \forall i \in I dom (\{i\} \times J) \subseteq I$
20	18 19	sylibr	$⊢ φ \to ⋃_{i \in I} dom (\{i\} \times J) \subseteq I$
21	13 20	eqsstrid	$⊢ φ \to dom ⋃_{i \in I} (\{i\} \times J) \subseteq I$
22		simprl	$⊢ (φ \land (i \in I \land j \in J)) \to i \in I$
23		simprr	$⊢ (φ \land (i \in I \land j \in J)) \to j \in J$
24	10	ovmpt4g	$⊢ (i \in I \land j \in J \land S \in SubGrp (G)) \to i (i \in I, j \in J ⟼ S) j = S$
25	22 23 1 24	syl3anc	$⊢ (φ \land (i \in I \land j \in J)) \to i (i \in I, j \in J ⟼ S) j = S$
26	25	anassrs	$⊢ ((φ \land i \in I) \land j \in J) \to i (i \in I, j \in J ⟼ S) j = S$
27	26	mpteq2dva	$⊢ (φ \land i \in I) \to (j \in J ⟼ i (i \in I, j \in J ⟼ S) j) = (j \in J ⟼ S)$
28	2 27	breqtrrd	$⊢ (φ \land i \in I) \to G dom DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j)$
29	28	ralrimiva	$⊢ φ \to \forall i \in I G dom DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j)$
30		nfcv	$⊢ \underline{Ⅎ} i G$
31		nfcv	$⊢ \underline{Ⅎ} i dom DProd$
32		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ x / i ⦌ J$
33		nfcv	$⊢ \underline{Ⅎ} i x$
34		nfmpo1	$⊢ \underline{Ⅎ} i (i \in I, j \in J ⟼ S)$
35		nfcv	$⊢ \underline{Ⅎ} i j$
36	33 34 35	nfov	$⊢ \underline{Ⅎ} i (x (i \in I, j \in J ⟼ S) j)$
37	32 36	nfmpt	$⊢ \underline{Ⅎ} i (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j)$
38	30 31 37	nfbr	$⊢ Ⅎ i G dom DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j)$
39		csbeq1a	$⊢ i = x \to J = ⦋ x / i ⦌ J$
40		oveq1	$⊢ i = x \to i (i \in I, j \in J ⟼ S) j = x (i \in I, j \in J ⟼ S) j$
41	39 40	mpteq12dv	$⊢ i = x \to (j \in J ⟼ i (i \in I, j \in J ⟼ S) j) = (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j)$
42	41	breq2d	$⊢ i = x \to (G dom DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j) \leftrightarrow G dom DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j))$
43	38 42	rspc	$⊢ x \in I \to (\forall i \in I G dom DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j) \to G dom DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j))$
44	29 43	mpan9	$⊢ (φ \land x \in I) \to G dom DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j)$
45		nfcv	$⊢ \underline{Ⅎ} y (x (i \in I, j \in J ⟼ S) j)$
46		nfcv	$⊢ \underline{Ⅎ} j x$
47		nfmpo2	$⊢ \underline{Ⅎ} j (i \in I, j \in J ⟼ S)$
48		nfcv	$⊢ \underline{Ⅎ} j y$
49	46 47 48	nfov	$⊢ \underline{Ⅎ} j (x (i \in I, j \in J ⟼ S) y)$
50		oveq2	$⊢ j = y \to x (i \in I, j \in J ⟼ S) j = x (i \in I, j \in J ⟼ S) y$
51	45 49 50	cbvmpt	$⊢ (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j) = (y \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) y)$
52		nfv	$⊢ Ⅎ i j = z$
53	32	nfcri	$⊢ Ⅎ i j \in ⦋ x / i ⦌ J$
54	52 53	nfan	$⊢ Ⅎ i (j = z \land j \in ⦋ x / i ⦌ J)$
55	39	eleq2d	$⊢ i = x \to (j \in J \leftrightarrow j \in ⦋ x / i ⦌ J)$
56	55	anbi2d	$⊢ i = x \to ((j = z \land j \in J) \leftrightarrow (j = z \land j \in ⦋ x / i ⦌ J))$
57	54 56	equsexv	$⊢ \exists i (i = x \land (j = z \land j \in J)) \leftrightarrow (j = z \land j \in ⦋ x / i ⦌ J)$
58		simprl	$⊢ ((φ \land x \in I) \land (i = x \land j = z)) \to i = x$
59		simplr	$⊢ ((φ \land x \in I) \land (i = x \land j = z)) \to x \in I$
60	58 59	eqeltrd	$⊢ ((φ \land x \in I) \land (i = x \land j = z)) \to i \in I$
61	60	biantrurd	$⊢ ((φ \land x \in I) \land (i = x \land j = z)) \to (j \in J \leftrightarrow (i \in I \land j \in J))$
62	61	pm5.32da	$⊢ (φ \land x \in I) \to (((i = x \land j = z) \land j \in J) \leftrightarrow ((i = x \land j = z) \land (i \in I \land j \in J)))$
63		anass	$⊢ ((i = x \land j = z) \land j \in J) \leftrightarrow (i = x \land (j = z \land j \in J))$
64		eqcom	$⊢ ⟨x, z⟩ = ⟨i, j⟩ \leftrightarrow ⟨i, j⟩ = ⟨x, z⟩$
65		vex	$⊢ i \in V$
66		vex	$⊢ j \in V$
67	65 66	opth	$⊢ ⟨i, j⟩ = ⟨x, z⟩ \leftrightarrow (i = x \land j = z)$
68	64 67	bitr2i	$⊢ (i = x \land j = z) \leftrightarrow ⟨x, z⟩ = ⟨i, j⟩$
69	68	anbi1i	$⊢ ((i = x \land j = z) \land (i \in I \land j \in J)) \leftrightarrow (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J))$
70	62 63 69	3bitr3g	$⊢ (φ \land x \in I) \to ((i = x \land (j = z \land j \in J)) \leftrightarrow (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J)))$
71	70	exbidv	$⊢ (φ \land x \in I) \to (\exists i (i = x \land (j = z \land j \in J)) \leftrightarrow \exists i (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J)))$
72	57 71	bitr3id	$⊢ (φ \land x \in I) \to ((j = z \land j \in ⦋ x / i ⦌ J) \leftrightarrow \exists i (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J)))$
73	72	exbidv	$⊢ (φ \land x \in I) \to (\exists j (j = z \land j \in ⦋ x / i ⦌ J) \leftrightarrow \exists j \exists i (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J)))$
74		vex	$⊢ z \in V$
75		eleq1w	$⊢ j = z \to (j \in ⦋ x / i ⦌ J \leftrightarrow z \in ⦋ x / i ⦌ J)$
76	74 75	ceqsexv	$⊢ \exists j (j = z \land j \in ⦋ x / i ⦌ J) \leftrightarrow z \in ⦋ x / i ⦌ J$
77		excom	$⊢ \exists j \exists i (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J)) \leftrightarrow \exists i \exists j (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J))$
78	73 76 77	3bitr3g	$⊢ (φ \land x \in I) \to (z \in ⦋ x / i ⦌ J \leftrightarrow \exists i \exists j (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J)))$
79		elrelimasn	$⊢ Rel ⋃_{i \in I} (\{i\} \times J) \to (z \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] \leftrightarrow x ⋃_{i \in I} (\{i\} \times J) z)$
80	7 79	ax-mp	$⊢ z \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] \leftrightarrow x ⋃_{i \in I} (\{i\} \times J) z$
81		df-br	$⊢ x ⋃_{i \in I} (\{i\} \times J) z \leftrightarrow ⟨x, z⟩ \in ⋃_{i \in I} (\{i\} \times J)$
82		eliunxp	$⊢ ⟨x, z⟩ \in ⋃_{i \in I} (\{i\} \times J) \leftrightarrow \exists i \exists j (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J))$
83	80 81 82	3bitri	$⊢ z \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] \leftrightarrow \exists i \exists j (⟨x, z⟩ = ⟨i, j⟩ \land (i \in I \land j \in J))$
84	78 83	bitr4di	$⊢ (φ \land x \in I) \to (z \in ⦋ x / i ⦌ J \leftrightarrow z \in ⋃_{i \in I} (\{i\} \times J) [\{x\}])$
85	84	eqrdv	$⊢ (φ \land x \in I) \to ⦋ x / i ⦌ J = ⋃_{i \in I} (\{i\} \times J) [\{x\}]$
86	85	mpteq1d	$⊢ (φ \land x \in I) \to (y \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) y) = (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y)$
87	51 86	syl5eq	$⊢ (φ \land x \in I) \to (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j) = (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y)$
88	44 87	breqtrd	$⊢ (φ \land x \in I) \to G dom DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y)$
89	27	oveq2d	$⊢ (φ \land i \in I) \to G DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j) = G DProd (j \in J ⟼ S)$
90	89	mpteq2dva	$⊢ φ \to (i \in I ⟼ G DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j)) = (i \in I ⟼ G DProd (j \in J ⟼ S))$
91	3 90	breqtrrd	$⊢ φ \to G dom DProd (i \in I ⟼ G DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j))$
92		nfcv	$⊢ \underline{Ⅎ} x (G DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j))$
93		nfcv	$⊢ \underline{Ⅎ} i DProd$
94	30 93 37	nfov	$⊢ \underline{Ⅎ} i (G DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j))$
95	41	oveq2d	$⊢ i = x \to G DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j) = G DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j)$
96	92 94 95	cbvmpt	$⊢ (i \in I ⟼ G DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j)) = (x \in I ⟼ G DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j))$
97	87	oveq2d	$⊢ (φ \land x \in I) \to G DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j) = G DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y)$
98	97	mpteq2dva	$⊢ φ \to (x \in I ⟼ G DProd (j \in ⦋ x / i ⦌ J ⟼ x (i \in I, j \in J ⟼ S) j)) = (x \in I ⟼ G DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y))$
99	96 98	syl5eq	$⊢ φ \to (i \in I ⟼ G DProd (j \in J ⟼ i (i \in I, j \in J ⟼ S) j)) = (x \in I ⟼ G DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y))$
100	91 99	breqtrd	$⊢ φ \to G dom DProd (x \in I ⟼ G DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y))$
101		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
102	8 12 21 88 100 101	dprd2da	$⊢ φ \to G dom DProd (i \in I, j \in J ⟼ S)$
103	8 12 21 88 100 101	dprd2db	$⊢ φ \to G DProd (i \in I, j \in J ⟼ S) = G DProd (x \in I ⟼ G DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y))$
104	99 90	eqtr3d	$⊢ φ \to (x \in I ⟼ G DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y)) = (i \in I ⟼ G DProd (j \in J ⟼ S))$
105	104	oveq2d	$⊢ φ \to G DProd (x \in I ⟼ G DProd (y \in ⋃_{i \in I} (\{i\} \times J) [\{x\}] ⟼ x (i \in I, j \in J ⟼ S) y)) = G DProd (i \in I ⟼ G DProd (j \in J ⟼ S))$
106	103 105	eqtrd	$⊢ φ \to G DProd (i \in I, j \in J ⟼ S) = G DProd (i \in I ⟼ G DProd (j \in J ⟼ S))$
107	102 106	jca	$⊢ φ \to (G dom DProd (i \in I, j \in J ⟼ S) \land G DProd (i \in I, j \in J ⟼ S) = G DProd (i \in I ⟼ G DProd (j \in J ⟼ S)))$

Metamath Proof Explorer

Theorem dprd2d2

Proof