prdsplusg

Description: Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015) (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$
	prdsplusg.b	$⊢ \underset{˙}{+} = +_{P}$
Assertion	prdsplusg	$⊢ φ \to \underset{˙}{+} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{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		prdsplusg.b	$⊢ \underset{˙}{+} = +_{P}$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8	1 2 3 4 5	prdsbas	$⊢ φ \to B = \underset{x \in I}{⨉} {Base}_{R (x)}$
9		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
10		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x))) = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))$
11		eqidd	$⊢ φ \to (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x))) = (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))$
12		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)))$
13		eqidd	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = \prod_{𝑡} (TopOpen \circ R)$
14		eqidd	$⊢ φ \to \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\} = \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}$
15		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <)) = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <))$
16		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)))$
17		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))))$
18	1 7 5 8 9 10 11 12 13 14 15 16 17 2 3	prdsval	$⊢ φ \to P = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \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))))⟩\})$
19		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
20		ovssunirn	$⊢ f (x) +_{R (x)} g (x) \subseteq ⋃ ran +_{R (x)}$
21	19	strfvss	$⊢ +_{R (x)} \subseteq ⋃ ran R (x)$
22		fvssunirn	$⊢ R (x) \subseteq ⋃ ran R$
23		rnss	$⊢ R (x) \subseteq ⋃ ran R \to ran R (x) \subseteq ran ⋃ ran R$
24		uniss	$⊢ ran R (x) \subseteq ran ⋃ ran R \to ⋃ ran R (x) \subseteq ⋃ ran ⋃ ran R$
25	22 23 24	mp2b	$⊢ ⋃ ran R (x) \subseteq ⋃ ran ⋃ ran R$
26	21 25	sstri	$⊢ +_{R (x)} \subseteq ⋃ ran ⋃ ran R$
27		rnss	$⊢ +_{R (x)} \subseteq ⋃ ran ⋃ ran R \to ran +_{R (x)} \subseteq ran ⋃ ran ⋃ ran R$
28		uniss	$⊢ ran +_{R (x)} \subseteq ran ⋃ ran ⋃ ran R \to ⋃ ran +_{R (x)} \subseteq ⋃ ran ⋃ ran ⋃ ran R$
29	26 27 28	mp2b	$⊢ ⋃ ran +_{R (x)} \subseteq ⋃ ran ⋃ ran ⋃ ran R$
30	20 29	sstri	$⊢ f (x) +_{R (x)} g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran R$
31		ovex	$⊢ f (x) +_{R (x)} g (x) \in V$
32	31	elpw	$⊢ f (x) +_{R (x)} g (x) \in 𝒫 ⋃ ran ⋃ ran ⋃ ran R \leftrightarrow f (x) +_{R (x)} g (x) \subseteq ⋃ ran ⋃ ran ⋃ ran R$
33	30 32	mpbir	$⊢ f (x) +_{R (x)} g (x) \in 𝒫 ⋃ ran ⋃ ran ⋃ ran R$
34	33	a1i	$⊢ (φ \land x \in I) \to f (x) +_{R (x)} g (x) \in 𝒫 ⋃ ran ⋃ ran ⋃ ran R$
35	34	fmpttd	$⊢ φ \to (x \in I ⟼ f (x) +_{R (x)} g (x)) : I ⟶ 𝒫 ⋃ ran ⋃ ran ⋃ ran R$
36		rnexg	$⊢ R \in W \to ran R \in V$
37		uniexg	$⊢ ran R \in V \to ⋃ ran R \in V$
38	3 36 37	3syl	$⊢ φ \to ⋃ ran R \in V$
39		rnexg	$⊢ ⋃ ran R \in V \to ran ⋃ ran R \in V$
40		uniexg	$⊢ ran ⋃ ran R \in V \to ⋃ ran ⋃ ran R \in V$
41	38 39 40	3syl	$⊢ φ \to ⋃ ran ⋃ ran R \in V$
42		rnexg	$⊢ ⋃ ran ⋃ ran R \in V \to ran ⋃ ran ⋃ ran R \in V$
43		uniexg	$⊢ ran ⋃ ran ⋃ ran R \in V \to ⋃ ran ⋃ ran ⋃ ran R \in V$
44		pwexg	$⊢ ⋃ ran ⋃ ran ⋃ ran R \in V \to 𝒫 ⋃ ran ⋃ ran ⋃ ran R \in V$
45	41 42 43 44	4syl	$⊢ φ \to 𝒫 ⋃ ran ⋃ ran ⋃ ran R \in V$
46	3	dmexd	$⊢ φ \to dom R \in V$
47	5 46	eqeltrrd	$⊢ φ \to I \in V$
48	45 47	elmapd	$⊢ φ \to ((x \in I ⟼ f (x) +_{R (x)} g (x)) \in ({𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I}) \leftrightarrow (x \in I ⟼ f (x) +_{R (x)} g (x)) : I ⟶ 𝒫 ⋃ ran ⋃ ran ⋃ ran R)$
49	35 48	mpbird	$⊢ φ \to (x \in I ⟼ f (x) +_{R (x)} g (x)) \in ({𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I})$
50	49	ralrimivw	$⊢ φ \to \forall g \in B (x \in I ⟼ f (x) +_{R (x)} g (x)) \in ({𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I})$
51	50	ralrimivw	$⊢ φ \to \forall f \in B \forall g \in B (x \in I ⟼ f (x) +_{R (x)} g (x)) \in ({𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I})$
52		eqid	$⊢ (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$
53	52	fmpo	$⊢ \forall f \in B \forall g \in B (x \in I ⟼ f (x) +_{R (x)} g (x)) \in ({𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I}) \leftrightarrow (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) : B \times B ⟶ {𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I}$
54	51 53	sylib	$⊢ φ \to (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) : B \times B ⟶ {𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I}$
55	4	fvexi	$⊢ B \in V$
56	55 55	xpex	$⊢ B \times B \in V$
57		ovex	$⊢ {𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I} \in V$
58		fex2	$⊢ ((f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{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 ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) \in V$
59	56 57 58	mp3an23	$⊢ (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) : B \times B ⟶ {𝒫 ⋃ ran ⋃ ran ⋃ ran R}^{I} \to (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) \in V$
60	54 59	syl	$⊢ φ \to (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x))) \in V$
61		snsstp2	$⊢ \{⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\}$
62		ssun1	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}$
63	61 62	sstri	$⊢ \{⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}$
64		ssun1	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \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))))⟩\})$
65	63 64	sstri	$⊢ \{⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))⟩, ⟨\cdot_{ndx}, (f \in B, g \in B ⟼ (x \in I ⟼ f (x) \cdot_{R (x)} g (x)))⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (f \in {Base}_{S}, g \in B ⟼ (x \in I ⟼ f \cdot_{R (x)} g (x)))⟩, ⟨\cdot_{𝑖} (ndx), (f \in B, g \in B ⟼ \underset{x \in I}{\sum_{S}} (f (x) \cdot_{𝑖} (R (x)) g (x)))⟩\}) \cup (\{⟨TopSet (ndx), \prod_{𝑡} (TopOpen \circ R)⟩, ⟨\leq_{ndx}, \{⟨f, g⟩ \| (\{f, g\} \subseteq B \land \forall x \in I f (x) \leq_{R (x)} g (x))\}⟩, ⟨dist (ndx), (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))⟩\} \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))))⟩\})$
66	18 6 19 60 65	prdsbaslem	$⊢ φ \to \underset{˙}{+} = (f \in B, g \in B ⟼ (x \in I ⟼ f (x) +_{R (x)} g (x)))$

Metamath Proof Explorer

Theorem prdsplusg

Proof