prdsco

Description: Structure product composition operation. (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)$
	prdsco.o	$⊢ \underset{˙}{∙} = comp (P)$
Assertion	prdsco	$⊢ φ \to \underset{˙}{∙} = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (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		prdsco.o	$⊢ \underset{˙}{∙} = comp (P)$
8		eqid	$⊢ {Base}_{S} = {Base}_{S}$
9	1 2 3 4 5	prdsbas	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
10		eqid	$⊢ +_{P} = +_{P}$
11	1 2 3 4 5 10	prdsplusg	$⊢ φ \to +_{P} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
12		eqid	$⊢ \cdot_{P} = \cdot_{P}$
13	1 2 3 4 5 12	prdsmulr	$⊢ φ \to \cdot_{P} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
14		eqid	$⊢ \cdot_{P} = \cdot_{P}$
15	1 2 3 4 5 8 14	prdsvsca	$⊢ φ \to \cdot_{P} = (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
16		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)))$
17		eqid	$⊢ TopSet (P) = TopSet (P)$
18	1 2 3 4 5 17	prdstset	$⊢ φ \to TopSet (P) = \prod_{𝑡} (TopOpen \circ R)$
19		eqid	$⊢ \leq_{P} = \leq_{P}$
20	1 2 3 4 5 19	prdsle	$⊢ φ \to \leq_{P} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
21		eqid	$⊢ dist (P) = dist (P)$
22	1 2 3 4 5 21	prdsds	$⊢ φ \to dist (P) = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$
23	1 2 3 4 5 6	prdshom	$⊢ φ \to H = (f \in B, g \in B ⟼ \underset{x \in I}{⨉} (f (x) Hom (R (x)) g (x)))$
24		eqidd	$⊢ φ \to (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (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) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$
25	1 8 5 9 11 13 15 16 18 20 22 23 24 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), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
26		ccoid	$⊢ comp = Slot comp (ndx)$
27	4	fvexi	$⊢ B \in V$
28	27 27	xpex	$⊢ B \times B \in V$
29	28 27	mpoex	$⊢ (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)))) \in V$
30	29	a1i	$⊢ φ \to (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x)))) \in V$
31		snsspr2	$⊢ \{⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\} \subseteq \{⟨Hom (ndx), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
32		ssun2	$⊢ \{⟨Hom (ndx), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (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), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
33	31 32	sstri	$⊢ \{⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (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), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\}$
34		ssun2	$⊢ \{⟨TopSet (ndx), TopSet (P)⟩, ⟨\leq_{ndx}, \leq_{P}⟩, ⟨dist (ndx), dist (P)⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (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), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
35	33 34	sstri	$⊢ \{⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (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), H⟩, ⟨comp (ndx), (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))⟩\})$
36	25 7 26 30 35	prdsbaslem	$⊢ φ \to \underset{˙}{∙} = (a \in (B \times B), c \in B ⟼ (d \in (2^{nd} (a) H c), e \in H (a) ⟼ (x \in I ⟼ d (x) (⟨1^{st} (a) (x), 2^{nd} (a) (x)⟩ comp (R (x)) c (x)) e (x))))$

Metamath Proof Explorer

Theorem prdsco

Proof