prdstgpd

Description: The product of a family of topological groups is a topological group. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	prdstgpd.y	$⊢ Y = S ⨉_{𝑠} R$
	prdstgpd.i	$⊢ φ \to I \in W$
	prdstgpd.s	$⊢ φ \to S \in V$
	prdstgpd.r	$⊢ φ \to R : I ⟶ TopGrp$
Assertion	prdstgpd	$⊢ φ \to Y \in TopGrp$

Proof

Step	Hyp	Ref	Expression
1		prdstgpd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdstgpd.i	$⊢ φ \to I \in W$
3		prdstgpd.s	$⊢ φ \to S \in V$
4		prdstgpd.r	$⊢ φ \to R : I ⟶ TopGrp$
5		tgpgrp	$⊢ x \in TopGrp \to x \in Grp$
6	5	ssriv	$⊢ TopGrp \subseteq Grp$
7		fss	$⊢ (R : I ⟶ TopGrp \land TopGrp \subseteq Grp) \to R : I ⟶ Grp$
8	4 6 7	sylancl	$⊢ φ \to R : I ⟶ Grp$
9	1 2 3 8	prdsgrpd	$⊢ φ \to Y \in Grp$
10		tgptmd	$⊢ x \in TopGrp \to x \in TopMnd$
11	10	ssriv	$⊢ TopGrp \subseteq TopMnd$
12		fss	$⊢ (R : I ⟶ TopGrp \land TopGrp \subseteq TopMnd) \to R : I ⟶ TopMnd$
13	4 11 12	sylancl	$⊢ φ \to R : I ⟶ TopMnd$
14	1 2 3 13	prdstmdd	$⊢ φ \to Y \in TopMnd$
15		eqid	$⊢ \prod_{𝑡} (TopOpen \circ R) = \prod_{𝑡} (TopOpen \circ R)$
16		eqid	$⊢ TopOpen (Y) = TopOpen (Y)$
17		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
18	16 17	tmdtopon	$⊢ Y \in TopMnd \to TopOpen (Y) \in TopOn ({Base}_{Y})$
19	14 18	syl	$⊢ φ \to TopOpen (Y) \in TopOn ({Base}_{Y})$
20		topnfn	$⊢ TopOpen Fn V$
21	4	ffnd	$⊢ φ \to R Fn I$
22		dffn2	$⊢ R Fn I \leftrightarrow R : I ⟶ V$
23	21 22	sylib	$⊢ φ \to R : I ⟶ V$
24		fnfco	$⊢ (TopOpen Fn V \land R : I ⟶ V) \to (TopOpen \circ R) Fn I$
25	20 23 24	sylancr	$⊢ φ \to (TopOpen \circ R) Fn I$
26		fvco3	$⊢ (R : I ⟶ TopGrp \land y \in I) \to (TopOpen \circ R) (y) = TopOpen (R (y))$
27	4 26	sylan	$⊢ (φ \land y \in I) \to (TopOpen \circ R) (y) = TopOpen (R (y))$
28	4	ffvelrnda	$⊢ (φ \land y \in I) \to R (y) \in TopGrp$
29		eqid	$⊢ TopOpen (R (y)) = TopOpen (R (y))$
30		eqid	$⊢ {Base}_{R (y)} = {Base}_{R (y)}$
31	29 30	tgptopon	$⊢ R (y) \in TopGrp \to TopOpen (R (y)) \in TopOn ({Base}_{R (y)})$
32		topontop	$⊢ TopOpen (R (y)) \in TopOn ({Base}_{R (y)}) \to TopOpen (R (y)) \in Top$
33	28 31 32	3syl	$⊢ (φ \land y \in I) \to TopOpen (R (y)) \in Top$
34	27 33	eqeltrd	$⊢ (φ \land y \in I) \to (TopOpen \circ R) (y) \in Top$
35	34	ralrimiva	$⊢ φ \to \forall y \in I (TopOpen \circ R) (y) \in Top$
36		ffnfv	$⊢ (TopOpen \circ R) : I ⟶ Top \leftrightarrow ((TopOpen \circ R) Fn I \land \forall y \in I (TopOpen \circ R) (y) \in Top)$
37	25 35 36	sylanbrc	$⊢ φ \to (TopOpen \circ R) : I ⟶ Top$
38	19	adantr	$⊢ (φ \land y \in I) \to TopOpen (Y) \in TopOn ({Base}_{Y})$
39	1 3 2 21 16	prdstopn	$⊢ φ \to TopOpen (Y) = \prod_{𝑡} (TopOpen \circ R)$
40	39	adantr	$⊢ (φ \land y \in I) \to TopOpen (Y) = \prod_{𝑡} (TopOpen \circ R)$
41	40	eqcomd	$⊢ (φ \land y \in I) \to \prod_{𝑡} (TopOpen \circ R) = TopOpen (Y)$
42	41 38	eqeltrd	$⊢ (φ \land y \in I) \to \prod_{𝑡} (TopOpen \circ R) \in TopOn ({Base}_{Y})$
43		toponuni	$⊢ \prod_{𝑡} (TopOpen \circ R) \in TopOn ({Base}_{Y}) \to {Base}_{Y} = ⋃ \prod_{𝑡} (TopOpen \circ R)$
44		mpteq1	$⊢ {Base}_{Y} = ⋃ \prod_{𝑡} (TopOpen \circ R) \to (x \in {Base}_{Y} ⟼ x (y)) = (x \in ⋃ \prod_{𝑡} (TopOpen \circ R) ⟼ x (y))$
45	42 43 44	3syl	$⊢ (φ \land y \in I) \to (x \in {Base}_{Y} ⟼ x (y)) = (x \in ⋃ \prod_{𝑡} (TopOpen \circ R) ⟼ x (y))$
46	2	adantr	$⊢ (φ \land y \in I) \to I \in W$
47	37	adantr	$⊢ (φ \land y \in I) \to (TopOpen \circ R) : I ⟶ Top$
48		simpr	$⊢ (φ \land y \in I) \to y \in I$
49		eqid	$⊢ ⋃ \prod_{𝑡} (TopOpen \circ R) = ⋃ \prod_{𝑡} (TopOpen \circ R)$
50	49 15	ptpjcn	$⊢ (I \in W \land (TopOpen \circ R) : I ⟶ Top \land y \in I) \to (x \in ⋃ \prod_{𝑡} (TopOpen \circ R) ⟼ x (y)) \in (\prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (y))$
51	46 47 48 50	syl3anc	$⊢ (φ \land y \in I) \to (x \in ⋃ \prod_{𝑡} (TopOpen \circ R) ⟼ x (y)) \in (\prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (y))$
52	45 51	eqeltrd	$⊢ (φ \land y \in I) \to (x \in {Base}_{Y} ⟼ x (y)) \in (\prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (y))$
53	41 27	oveq12d	$⊢ (φ \land y \in I) \to \prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (y) = TopOpen (Y) Cn TopOpen (R (y))$
54	52 53	eleqtrd	$⊢ (φ \land y \in I) \to (x \in {Base}_{Y} ⟼ x (y)) \in (TopOpen (Y) Cn TopOpen (R (y)))$
55		eqid	$⊢ {inv}_{g} (R (y)) = {inv}_{g} (R (y))$
56	29 55	tgpinv	$⊢ R (y) \in TopGrp \to {inv}_{g} (R (y)) \in (TopOpen (R (y)) Cn TopOpen (R (y)))$
57	28 56	syl	$⊢ (φ \land y \in I) \to {inv}_{g} (R (y)) \in (TopOpen (R (y)) Cn TopOpen (R (y)))$
58	38 54 57	cnmpt11f	$⊢ (φ \land y \in I) \to (x \in {Base}_{Y} ⟼ {inv}_{g} (R (y)) (x (y))) \in (TopOpen (Y) Cn TopOpen (R (y)))$
59	27	oveq2d	$⊢ (φ \land y \in I) \to TopOpen (Y) Cn (TopOpen \circ R) (y) = TopOpen (Y) Cn TopOpen (R (y))$
60	58 59	eleqtrrd	$⊢ (φ \land y \in I) \to (x \in {Base}_{Y} ⟼ {inv}_{g} (R (y)) (x (y))) \in (TopOpen (Y) Cn (TopOpen \circ R) (y))$
61	15 19 2 37 60	ptcn	$⊢ φ \to (x \in {Base}_{Y} ⟼ (y \in I ⟼ {inv}_{g} (R (y)) (x (y)))) \in (TopOpen (Y) Cn \prod_{𝑡} (TopOpen \circ R))$
62		eqid	$⊢ {inv}_{g} (Y) = {inv}_{g} (Y)$
63	17 62	grpinvf	$⊢ Y \in Grp \to {inv}_{g} (Y) : {Base}_{Y} ⟶ {Base}_{Y}$
64	9 63	syl	$⊢ φ \to {inv}_{g} (Y) : {Base}_{Y} ⟶ {Base}_{Y}$
65	64	feqmptd	$⊢ φ \to {inv}_{g} (Y) = (x \in {Base}_{Y} ⟼ {inv}_{g} (Y) (x))$
66	2	adantr	$⊢ (φ \land x \in {Base}_{Y}) \to I \in W$
67	3	adantr	$⊢ (φ \land x \in {Base}_{Y}) \to S \in V$
68	8	adantr	$⊢ (φ \land x \in {Base}_{Y}) \to R : I ⟶ Grp$
69		simpr	$⊢ (φ \land x \in {Base}_{Y}) \to x \in {Base}_{Y}$
70	1 66 67 68 17 62 69	prdsinvgd	$⊢ (φ \land x \in {Base}_{Y}) \to {inv}_{g} (Y) (x) = (y \in I ⟼ {inv}_{g} (R (y)) (x (y)))$
71	70	mpteq2dva	$⊢ φ \to (x \in {Base}_{Y} ⟼ {inv}_{g} (Y) (x)) = (x \in {Base}_{Y} ⟼ (y \in I ⟼ {inv}_{g} (R (y)) (x (y))))$
72	65 71	eqtrd	$⊢ φ \to {inv}_{g} (Y) = (x \in {Base}_{Y} ⟼ (y \in I ⟼ {inv}_{g} (R (y)) (x (y))))$
73	39	oveq2d	$⊢ φ \to TopOpen (Y) Cn TopOpen (Y) = TopOpen (Y) Cn \prod_{𝑡} (TopOpen \circ R)$
74	61 72 73	3eltr4d	$⊢ φ \to {inv}_{g} (Y) \in (TopOpen (Y) Cn TopOpen (Y))$
75	16 62	istgp	$⊢ Y \in TopGrp \leftrightarrow (Y \in Grp \land Y \in TopMnd \land {inv}_{g} (Y) \in (TopOpen (Y) Cn TopOpen (Y)))$
76	9 14 74 75	syl3anbrc	$⊢ φ \to Y \in TopGrp$

Metamath Proof Explorer

Theorem prdstgpd

Proof