prdshom

Description: Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

	Ref	Expression
Hypotheses	prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
	prdsbas.s	$⊢ φ \to S \in V$
	prdsbas.r	$⊢ φ \to R \in W$
	prdsbas.b	$⊢ B = {Base}_{P}$
	prdsbas.i	$⊢ φ \to dom R = I$
	prdshom.h	$⊢ H = Hom (P)$
Assertion	prdshom	$⊢ φ \to H = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	$⊢ P = S ⨉_{𝑠} R$
2		prdsbas.s	$⊢ φ \to S \in V$
3		prdsbas.r	$⊢ φ \to R \in W$
4		prdsbas.b	$⊢ B = {Base}_{P}$
5		prdsbas.i	$⊢ φ \to dom R = I$
6		prdshom.h	$⊢ H = Hom (P)$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8	1 2 3 4 5	prdsbas	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
9		eqid	$⊢ +_{P} = +_{P}$
10	1 2 3 4 5 9	prdsplusg	$⊢ φ \to +_{P} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
11		eqid	$⊢ \cdot_{P} = \cdot_{P}$
12	1 2 3 4 5 11	prdsmulr	$⊢ φ \to \cdot_{P} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
13		eqid	$⊢ \cdot_{P} = \cdot_{P}$
14	1 2 3 4 5 7 13	prdsvsca	$⊢ φ \to \cdot_{P} = (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
15		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))$
16		eqid	$⊢ TopSet (P) = TopSet (P)$
17	1 2 3 4 5 16	prdstset	$⊢ φ \to TopSet (P) = \prod_{𝑡} (TopOpen \circ R)$
18		eqid	$⊢ \leq_{P} = \leq_{P}$
19	1 2 3 4 5 18	prdsle	$⊢ φ \to \leq_{P} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
20		eqid	$⊢ dist (P) = dist (P)$
21	1 2 3 4 5 20	prdsds	$⊢ φ \to dist (P) = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$
22		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
23		eqidd	$⊢ φ \to (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)))) = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
24	1 7 5 8 10 12 14 15 17 19 21 22 23 2 3	prdsval	$⊢ φ \to P = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{P}⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), TopSet (P)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), dist (P)⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
25		homid	$⊢ Hom = Slot Hom (ndx)$
26		ovssunirn	$⊢ f (x) Hom (R (x)) g (x) \subseteq ⋃ ran Hom (R (x))$
27	25	strfvss	$⊢ Hom (R (x)) \subseteq ⋃ ran R (x)$
28		fvssunirn	$⊢ R (x) \subseteq ⋃ ran R$
29		rnss	$⊢ R (x) \subseteq ⋃ ran R \to ran R (x) \subseteq ran ⋃ ran R$
30		uniss	$⊢ ran R (x) \subseteq ran ⋃ ran R \to ⋃ ran R (x) \subseteq ⋃ ran ⋃ ran R$
31	28 29 30	mp2b	$⊢ ⋃ ran R (x) \subseteq ⋃ ran ⋃ ran R$
32	27 31	sstri	$⊢ Hom (R (x)) \subseteq ⋃ ran ⋃ ran R$
33		rnss	$⊢ Hom (R (x)) \subseteq ⋃ ran ⋃ ran R \to ran Hom (R (x)) \subseteq ran ⋃ ran ⋃ ran R$
34		uniss	$⊢ ran Hom (R (x)) \subseteq ran ⋃ ran ⋃ ran R \to ⋃ ran Hom (R (x)) \subseteq ⋃ ran ⋃ ran ⋃ ran R$
35	32 33 34	mp2b	$⊢ ⋃ ran Hom (R (x)) \subseteq ⋃ ran ⋃ ran ⋃ ran R$
36	26 35	sstri	$⊢ f (x) Hom (R (x)) g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran R$
37	36	rgenw	$⊢ \forall x \in I f (x) Hom (R (x)) g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran R$
38		ss2ixp	$⊢ \forall x \in I f (x) Hom (R (x)) g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran R \to \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \subseteq \underset{x \in I}{⨉} ⋃ ran ⋃ ran ⋃ ran R$
39	37 38	ax-mp	$⊢ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \subseteq \underset{x \in I}{⨉} ⋃ ran ⋃ ran ⋃ ran R$
40	3	dmexd	$⊢ φ \to dom R \in V$
41	5 40	eqeltrrd	$⊢ φ \to I \in V$
42		rnexg	$⊢ R \in W \to ran R \in V$
43		uniexg	$⊢ ran R \in V \to ⋃ ran R \in V$
44	3 42 43	3syl	$⊢ φ \to ⋃ ran R \in V$
45		rnexg	$⊢ ⋃ ran R \in V \to ran ⋃ ran R \in V$
46		uniexg	$⊢ ran ⋃ ran R \in V \to ⋃ ran ⋃ ran R \in V$
47	44 45 46	3syl	$⊢ φ \to ⋃ ran ⋃ ran R \in V$
48		rnexg	$⊢ ⋃ ran ⋃ ran R \in V \to ran ⋃ ran ⋃ ran R \in V$
49		uniexg	$⊢ ran ⋃ ran ⋃ ran R \in V \to ⋃ ran ⋃ ran ⋃ ran R \in V$
50	47 48 49	3syl	$⊢ φ \to ⋃ ran ⋃ ran ⋃ ran R \in V$
51		ixpconstg	$⊢ (I \in V \land ⋃ ran ⋃ ran ⋃ ran R \in V) \to \underset{x \in I}{⨉} ⋃ ran ⋃ ran ⋃ ran R = {⋃ ran ⋃ ran ⋃ ran R}^{I}$
52	41 50 51	syl2anc	$⊢ φ \to \underset{x \in I}{⨉} ⋃ ran ⋃ ran ⋃ ran R = {⋃ ran ⋃ ran ⋃ ran R}^{I}$
53	39 52	sseqtrid	$⊢ φ \to \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \subseteq {⋃ ran ⋃ ran ⋃ ran R}^{I}$
54		ovex	$⊢ {⋃ ran ⋃ ran ⋃ ran R}^{I} \in V$
55	54	elpw2	$⊢ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I}) \leftrightarrow \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \subseteq {⋃ ran ⋃ ran ⋃ ran R}^{I}$
56	53 55	sylibr	$⊢ φ \to \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I})$
57	56	ralrimivw	$⊢ φ \to \forall g \in B \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I})$
58	57	ralrimivw	$⊢ φ \to \forall f \in B \forall g \in B \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I})$
59		eqid	$⊢ (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
60	59	fmpo	$⊢ \forall f \in B \forall g \in B \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)) \in 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I}) \leftrightarrow (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) : B \times B ⟶ 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I})$
61	58 60	sylib	$⊢ φ \to (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) : B \times B ⟶ 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I})$
62	4	fvexi	$⊢ B \in V$
63	62 62	xpex	$⊢ B \times B \in V$
64	63	a1i	$⊢ φ \to B \times B \in V$
65	54	pwex	$⊢ 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I}) \in V$
66	65	a1i	$⊢ φ \to 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I}) \in V$
67		fex2	$⊢ ((f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) : B \times B ⟶ 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I}) \land B \times B \in V \land 𝒫 ({⋃ ran ⋃ ran ⋃ ran R}^{I}) \in V) \to (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) \in V$
68	61 64 66 67	syl3anc	$⊢ φ \to (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) \in V$
69		snsspr1	$⊢ \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩\} \subseteq \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
70		ssun2	$⊢ \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\} \subseteq \{⟨TopSet (ndx), TopSet (P)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), dist (P)⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
71	69 70	sstri	$⊢ \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩\} \subseteq \{⟨TopSet (ndx), TopSet (P)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), dist (P)⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
72		ssun2	$⊢ \{⟨TopSet (ndx), TopSet (P)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), dist (P)⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{P}⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), TopSet (P)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), dist (P)⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
73	71 72	sstri	$⊢ \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{P}⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \cdot_{P}⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), TopSet (P)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), dist (P)⟩\} \cup \{⟨Hom (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) c), e \in (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x))) (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
74	24 6 25 68 73	prdsbaslem	$⊢ φ \to H = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$

Metamath Proof Explorer

Theorem prdshom

Proof