prdstmdd

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

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

Proof

Step	Hyp	Ref	Expression
1		prdstmdd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdstmdd.i	$⊢ φ \to I \in W$
3		prdstmdd.s	$⊢ φ \to S \in V$
4		prdstmdd.r	$⊢ φ \to R : I ⟶ TopMnd$
5		tmdmnd	$⊢ x \in TopMnd \to x \in Mnd$
6	5	ssriv	$⊢ TopMnd \subseteq Mnd$
7		fss	$⊢ (R : I ⟶ TopMnd \land TopMnd \subseteq Mnd) \to R : I ⟶ Mnd$
8	4 6 7	sylancl	$⊢ φ \to R : I ⟶ Mnd$
9	1 2 3 8	prdsmndd	$⊢ φ \to Y \in Mnd$
10		tmdtps	$⊢ x \in TopMnd \to x \in TopSp$
11	10	ssriv	$⊢ TopMnd \subseteq TopSp$
12		fss	$⊢ (R : I ⟶ TopMnd \land TopMnd \subseteq TopSp) \to R : I ⟶ TopSp$
13	4 11 12	sylancl	$⊢ φ \to R : I ⟶ TopSp$
14	1 3 2 13	prdstps	$⊢ φ \to Y \in TopSp$
15		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
16	3	3ad2ant1	$⊢ (φ \land f \in {Base}_{Y} \land g \in {Base}_{Y}) \to S \in V$
17	2	3ad2ant1	$⊢ (φ \land f \in {Base}_{Y} \land g \in {Base}_{Y}) \to I \in W$
18	4	ffnd	$⊢ φ \to R Fn I$
19	18	3ad2ant1	$⊢ (φ \land f \in {Base}_{Y} \land g \in {Base}_{Y}) \to R Fn I$
20		simp2	$⊢ (φ \land f \in {Base}_{Y} \land g \in {Base}_{Y}) \to f \in {Base}_{Y}$
21		simp3	$⊢ (φ \land f \in {Base}_{Y} \land g \in {Base}_{Y}) \to g \in {Base}_{Y}$
22		eqid	$⊢ +_{Y} = +_{Y}$
23	1 15 16 17 19 20 21 22	prdsplusgval	$⊢ (φ \land f \in {Base}_{Y} \land g \in {Base}_{Y}) \to f +_{Y} g = (k \in I ⟼ f (k) +_{R (k)} g (k))$
24	23	mpoeq3dva	$⊢ φ \to (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ f +_{Y} g) = (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ (k \in I ⟼ f (k) +_{R (k)} g (k)))$
25		eqid	$⊢ +_{𝑓} (Y) = +_{𝑓} (Y)$
26	15 22 25	plusffval	$⊢ +_{𝑓} (Y) = (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ f +_{Y} g)$
27		vex	$⊢ f \in V$
28		vex	$⊢ g \in V$
29	27 28	op1std	$⊢ z = ⟨f, g⟩ \to 1^{st} (z) = f$
30	29	fveq1d	$⊢ z = ⟨f, g⟩ \to 1^{st} (z) (k) = f (k)$
31	27 28	op2ndd	$⊢ z = ⟨f, g⟩ \to 2^{nd} (z) = g$
32	31	fveq1d	$⊢ z = ⟨f, g⟩ \to 2^{nd} (z) (k) = g (k)$
33	30 32	oveq12d	$⊢ z = ⟨f, g⟩ \to 1^{st} (z) (k) +_{R (k)} 2^{nd} (z) (k) = f (k) +_{R (k)} g (k)$
34	33	mpteq2dv	$⊢ z = ⟨f, g⟩ \to (k \in I ⟼ 1^{st} (z) (k) +_{R (k)} 2^{nd} (z) (k)) = (k \in I ⟼ f (k) +_{R (k)} g (k))$
35	34	mpompt	$⊢ (z \in ({Base}_{Y} \times {Base}_{Y}) ⟼ (k \in I ⟼ 1^{st} (z) (k) +_{R (k)} 2^{nd} (z) (k))) = (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ (k \in I ⟼ f (k) +_{R (k)} g (k)))$
36	24 26 35	3eqtr4g	$⊢ φ \to +_{𝑓} (Y) = (z \in ({Base}_{Y} \times {Base}_{Y}) ⟼ (k \in I ⟼ 1^{st} (z) (k) +_{R (k)} 2^{nd} (z) (k)))$
37		eqid	$⊢ \prod_{𝑡} (TopOpen \circ R) = \prod_{𝑡} (TopOpen \circ R)$
38		eqid	$⊢ TopOpen (Y) = TopOpen (Y)$
39	15 38	istps	$⊢ Y \in TopSp \leftrightarrow TopOpen (Y) \in TopOn ({Base}_{Y})$
40	14 39	sylib	$⊢ φ \to TopOpen (Y) \in TopOn ({Base}_{Y})$
41		txtopon	$⊢ (TopOpen (Y) \in TopOn ({Base}_{Y}) \land TopOpen (Y) \in TopOn ({Base}_{Y})) \to TopOpen (Y) \times_{t} TopOpen (Y) \in TopOn ({Base}_{Y} \times {Base}_{Y})$
42	40 40 41	syl2anc	$⊢ φ \to TopOpen (Y) \times_{t} TopOpen (Y) \in TopOn ({Base}_{Y} \times {Base}_{Y})$
43		topnfn	$⊢ TopOpen Fn V$
44		ssv	$⊢ TopSp \subseteq V$
45		fnssres	$⊢ (TopOpen Fn V \land TopSp \subseteq V) \to ({TopOpen ↾}_{TopSp}) Fn TopSp$
46	43 44 45	mp2an	$⊢ ({TopOpen ↾}_{TopSp}) Fn TopSp$
47		fvres	$⊢ x \in TopSp \to ({TopOpen ↾}_{TopSp}) (x) = TopOpen (x)$
48		eqid	$⊢ TopOpen (x) = TopOpen (x)$
49	48	tpstop	$⊢ x \in TopSp \to TopOpen (x) \in Top$
50	47 49	eqeltrd	$⊢ x \in TopSp \to ({TopOpen ↾}_{TopSp}) (x) \in Top$
51	50	rgen	$⊢ \forall x \in TopSp ({TopOpen ↾}_{TopSp}) (x) \in Top$
52		ffnfv	$⊢ ({TopOpen ↾}_{TopSp}) : TopSp ⟶ Top \leftrightarrow (({TopOpen ↾}_{TopSp}) Fn TopSp \land \forall x \in TopSp ({TopOpen ↾}_{TopSp}) (x) \in Top)$
53	46 51 52	mpbir2an	$⊢ ({TopOpen ↾}_{TopSp}) : TopSp ⟶ Top$
54		fco2	$⊢ (({TopOpen ↾}_{TopSp}) : TopSp ⟶ Top \land R : I ⟶ TopSp) \to (TopOpen \circ R) : I ⟶ Top$
55	53 13 54	sylancr	$⊢ φ \to (TopOpen \circ R) : I ⟶ Top$
56	33	mpompt	$⊢ (z \in ({Base}_{Y} \times {Base}_{Y}) ⟼ 1^{st} (z) (k) +_{R (k)} 2^{nd} (z) (k)) = (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ f (k) +_{R (k)} g (k))$
57		eqid	$⊢ TopOpen (R (k)) = TopOpen (R (k))$
58		eqid	$⊢ +_{R (k)} = +_{R (k)}$
59	4	ffvelrnda	$⊢ (φ \land k \in I) \to R (k) \in TopMnd$
60	40	adantr	$⊢ (φ \land k \in I) \to TopOpen (Y) \in TopOn ({Base}_{Y})$
61	60 60	cnmpt1st	$⊢ (φ \land k \in I) \to (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ f) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (Y))$
62	1 3 2 18 38	prdstopn	$⊢ φ \to TopOpen (Y) = \prod_{𝑡} (TopOpen \circ R)$
63	62	adantr	$⊢ (φ \land k \in I) \to TopOpen (Y) = \prod_{𝑡} (TopOpen \circ R)$
64	63 60	eqeltrrd	$⊢ (φ \land k \in I) \to \prod_{𝑡} (TopOpen \circ R) \in TopOn ({Base}_{Y})$
65		toponuni	$⊢ \prod_{𝑡} (TopOpen \circ R) \in TopOn ({Base}_{Y}) \to {Base}_{Y} = ⋃ \prod_{𝑡} (TopOpen \circ R)$
66	64 65	syl	$⊢ (φ \land k \in I) \to {Base}_{Y} = ⋃ \prod_{𝑡} (TopOpen \circ R)$
67	66	mpteq1d	$⊢ (φ \land k \in I) \to (x \in {Base}_{Y} ⟼ x (k)) = (x \in ⋃ \prod_{𝑡} (TopOpen \circ R) ⟼ x (k))$
68	2	adantr	$⊢ (φ \land k \in I) \to I \in W$
69	55	adantr	$⊢ (φ \land k \in I) \to (TopOpen \circ R) : I ⟶ Top$
70		simpr	$⊢ (φ \land k \in I) \to k \in I$
71		eqid	$⊢ ⋃ \prod_{𝑡} (TopOpen \circ R) = ⋃ \prod_{𝑡} (TopOpen \circ R)$
72	71 37	ptpjcn	$⊢ (I \in W \land (TopOpen \circ R) : I ⟶ Top \land k \in I) \to (x \in ⋃ \prod_{𝑡} (TopOpen \circ R) ⟼ x (k)) \in (\prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (k))$
73	68 69 70 72	syl3anc	$⊢ (φ \land k \in I) \to (x \in ⋃ \prod_{𝑡} (TopOpen \circ R) ⟼ x (k)) \in (\prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (k))$
74	67 73	eqeltrd	$⊢ (φ \land k \in I) \to (x \in {Base}_{Y} ⟼ x (k)) \in (\prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (k))$
75	63	eqcomd	$⊢ (φ \land k \in I) \to \prod_{𝑡} (TopOpen \circ R) = TopOpen (Y)$
76		fvco3	$⊢ (R : I ⟶ TopMnd \land k \in I) \to (TopOpen \circ R) (k) = TopOpen (R (k))$
77	4 76	sylan	$⊢ (φ \land k \in I) \to (TopOpen \circ R) (k) = TopOpen (R (k))$
78	75 77	oveq12d	$⊢ (φ \land k \in I) \to \prod_{𝑡} (TopOpen \circ R) Cn (TopOpen \circ R) (k) = TopOpen (Y) Cn TopOpen (R (k))$
79	74 78	eleqtrd	$⊢ (φ \land k \in I) \to (x \in {Base}_{Y} ⟼ x (k)) \in (TopOpen (Y) Cn TopOpen (R (k)))$
80		fveq1	$⊢ x = f \to x (k) = f (k)$
81	60 60 61 60 79 80	cnmpt21	$⊢ (φ \land k \in I) \to (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ f (k)) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (R (k)))$
82	60 60	cnmpt2nd	$⊢ (φ \land k \in I) \to (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ g) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (Y))$
83		fveq1	$⊢ x = g \to x (k) = g (k)$
84	60 60 82 60 79 83	cnmpt21	$⊢ (φ \land k \in I) \to (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ g (k)) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (R (k)))$
85	57 58 59 60 60 81 84	cnmpt2plusg	$⊢ (φ \land k \in I) \to (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ f (k) +_{R (k)} g (k)) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (R (k)))$
86	77	oveq2d	$⊢ (φ \land k \in I) \to (TopOpen (Y) \times_{t} TopOpen (Y)) Cn (TopOpen \circ R) (k) = (TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (R (k))$
87	85 86	eleqtrrd	$⊢ (φ \land k \in I) \to (f \in {Base}_{Y}, g \in {Base}_{Y} ⟼ f (k) +_{R (k)} g (k)) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn (TopOpen \circ R) (k))$
88	56 87	eqeltrid	$⊢ (φ \land k \in I) \to (z \in ({Base}_{Y} \times {Base}_{Y}) ⟼ 1^{st} (z) (k) +_{R (k)} 2^{nd} (z) (k)) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn (TopOpen \circ R) (k))$
89	37 42 2 55 88	ptcn	$⊢ φ \to (z \in ({Base}_{Y} \times {Base}_{Y}) ⟼ (k \in I ⟼ 1^{st} (z) (k) +_{R (k)} 2^{nd} (z) (k))) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn \prod_{𝑡} (TopOpen \circ R))$
90	36 89	eqeltrd	$⊢ φ \to +_{𝑓} (Y) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn \prod_{𝑡} (TopOpen \circ R))$
91	62	oveq2d	$⊢ φ \to (TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (Y) = (TopOpen (Y) \times_{t} TopOpen (Y)) Cn \prod_{𝑡} (TopOpen \circ R)$
92	90 91	eleqtrrd	$⊢ φ \to +_{𝑓} (Y) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (Y))$
93	25 38	istmd	$⊢ Y \in TopMnd \leftrightarrow (Y \in Mnd \land Y \in TopSp \land +_{𝑓} (Y) \in ((TopOpen (Y) \times_{t} TopOpen (Y)) Cn TopOpen (Y)))$
94	9 14 92 93	syl3anbrc	$⊢ φ \to Y \in TopMnd$

Metamath Proof Explorer

Theorem prdstmdd

Proof