prdsds - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prdsds		Structured version Visualization version GIF version

Theorem prdsds 16040

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)

**Hypotheses**
Ref	Expression
prdsbas.p	⊢ 𝑃 = (𝑆X_s𝑅)
prdsbas.s	⊢ (𝜑 → 𝑆 ∈ 𝑉)
prdsbas.r	⊢ (𝜑 → 𝑅 ∈ 𝑊)
prdsbas.b	⊢ 𝐵 = (Base‘𝑃)
prdsbas.i	⊢ (𝜑 → dom 𝑅 = 𝐼)
prdsds.l	⊢ 𝐷 = (dist‘𝑃)

**Assertion**
Ref	Expression
prdsds	⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )))

Distinct variable groups: 𝑓,𝑔,𝑥,𝐵 𝜑,𝑓,𝑔,𝑥 𝑓,𝐼,𝑔,𝑥 𝑃,𝑓,𝑔,𝑥 𝑅,𝑓,𝑔,𝑥 𝑆,𝑓,𝑔,𝑥 Allowed substitution hints: 𝐷(𝑥,𝑓,𝑔) 𝑉(𝑥,𝑓,𝑔) 𝑊(𝑥,𝑓,𝑔)

Proof of Theorem prdsds Dummy variables 𝑎 𝑐 𝑑 𝑒 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prdsbas.p	. . 3 ⊢ 𝑃 = (𝑆X_s𝑅)
2		eqid 2626	. . 3 ⊢ (Base‘𝑆) = (Base‘𝑆)
3		prdsbas.i	. . 3 ⊢ (𝜑 → dom 𝑅 = 𝐼)
4		prdsbas.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ 𝑉)
5		prdsbas.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ 𝑊)
6		prdsbas.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
7	1, 4, 5, 6, 3	prdsbas 16033	. . 3 ⊢ (𝜑 → 𝐵 = X𝑥 ∈ 𝐼 (Base‘(𝑅‘𝑥)))
8		eqid 2626	. . . 4 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
9	1, 4, 5, 6, 3, 8	prdsplusg 16034	. . 3 ⊢ (𝜑 → (+_g‘𝑃) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(+_g‘(𝑅‘𝑥))(𝑔‘𝑥)))))
10		eqid 2626	. . . 4 ⊢ (._r‘𝑃) = (._r‘𝑃)
11	1, 4, 5, 6, 3, 10	prdsmulr 16035	. . 3 ⊢ (𝜑 → (._r‘𝑃) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(._r‘(𝑅‘𝑥))(𝑔‘𝑥)))))
12		eqid 2626	. . . 4 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
13	1, 4, 5, 6, 3, 2, 12	prdsvsca 16036	. . 3 ⊢ (𝜑 → ( ·_𝑠 ‘𝑃) = (𝑓 ∈ (Base‘𝑆), 𝑔 ∈ 𝐵 ↦ (𝑥 ∈ 𝐼 ↦ (𝑓( ·_𝑠 ‘(𝑅‘𝑥))(𝑔‘𝑥)))))
14		eqidd 2627	. . 3 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥))))))
15		eqidd 2627	. . 3 ⊢ (𝜑 → (∏_t‘(TopOpen ∘ 𝑅)) = (∏_t‘(TopOpen ∘ 𝑅)))
16		eqid 2626	. . . 4 ⊢ (le‘𝑃) = (le‘𝑃)
17	1, 4, 5, 6, 3, 16	prdsle 16038	. . 3 ⊢ (𝜑 → (le‘𝑃) = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐼 (𝑓‘𝑥)(le‘(𝑅‘𝑥))(𝑔‘𝑥))})
18		eqidd 2627	. . 3 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )))
19		eqidd 2627	. . 3 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥))))
20		eqidd 2627	. . 3 ⊢ (𝜑 → (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥))))))
21	1, 2, 3, 7, 9, 11, 13, 14, 15, 17, 18, 19, 20, 4, 5	prdsval 16031	. 2 ⊢ (𝜑 → 𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), (+_g‘𝑃)⟩, ⟨(._r‘ndx), (._r‘𝑃)⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), ( ·_𝑠 ‘𝑃)⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < ))⟩} ∪ {⟨(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
22		prdsds.l	. 2 ⊢ 𝐷 = (dist‘𝑃)
23		dsid 15979	. 2 ⊢ dist = Slot (dist‘ndx)
24		df-sup 8293	. . . . . . 7 ⊢ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ) = ∪ {𝑦 ∈ ℝ^ ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))}
25		ssrab2 3671	. . . . . . . . 9 ⊢ {𝑦 ∈ ℝ^* ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ⊆ ℝ^*
26	25	unissi 4432	. . . . . . . 8 ⊢ ∪ {𝑦 ∈ ℝ^* ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ⊆ ∪ ℝ^*
27		xrex 11773	. . . . . . . . . 10 ⊢ ℝ^* ∈ V
28	27	uniex 6907	. . . . . . . . 9 ⊢ ∪ ℝ^* ∈ V
29	28	elpw2 4793	. . . . . . . 8 ⊢ (∪ {𝑦 ∈ ℝ^* ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ∈ 𝒫 ∪ ℝ^* ↔ ∪ {𝑦 ∈ ℝ^* ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ⊆ ∪ ℝ^*)
30	26, 29	mpbir 221	. . . . . . 7 ⊢ ∪ {𝑦 ∈ ℝ^* ∣ (∀𝑧 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}) ¬ 𝑦 < 𝑧 ∧ ∀𝑧 ∈ ℝ^* (𝑧 < 𝑦 → ∃𝑤 ∈ (ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0})𝑧 < 𝑤))} ∈ 𝒫 ∪ ℝ^*
31	24, 30	eqeltri 2700	. . . . . 6 ⊢ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ) ∈ 𝒫 ∪ ℝ^
32	31	rgen2w 2925	. . . . 5 ⊢ ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ) ∈ 𝒫 ∪ ℝ^
33		eqid 2626	. . . . . 6 ⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))
34	33	fmpt2 7183	. . . . 5 ⊢ (∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ) ∈ 𝒫 ∪ ℝ^ ↔ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )):(𝐵 × 𝐵)⟶𝒫 ∪ ℝ^)
35	32, 34	mpbi 220	. . . 4 ⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )):(𝐵 × 𝐵)⟶𝒫 ∪ ℝ^
36		fvex 6160	. . . . . 6 ⊢ (Base‘𝑃) ∈ V
37	6, 36	eqeltri 2700	. . . . 5 ⊢ 𝐵 ∈ V
38	37, 37	xpex 6916	. . . 4 ⊢ (𝐵 × 𝐵) ∈ V
39	28	pwex 4813	. . . 4 ⊢ 𝒫 ∪ ℝ^* ∈ V
40		fex2 7071	. . . 4 ⊢ (((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < )):(𝐵 × 𝐵)⟶𝒫 ∪ ℝ^ ∧ (𝐵 × 𝐵) ∈ V ∧ 𝒫 ∪ ℝ^* ∈ V) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )) ∈ V)
41	35, 38, 39, 40	mp3an 1421	. . 3 ⊢ (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )) ∈ V
42	41	a1i 11	. 2 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )) ∈ V)
43		snsstp3 4322	. . . 4 ⊢ {⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ⊆ {⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩}
44		ssun1 3759	. . . 4 ⊢ {⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ⊆ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ∪ {⟨(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})
45	43, 44	sstri 3597	. . 3 ⊢ {⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ⊆ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ∪ {⟨(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})
46		ssun2 3760	. . 3 ⊢ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ∪ {⟨(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}) ⊆ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), (+_g‘𝑃)⟩, ⟨(._r‘ndx), (._r‘𝑃)⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), ( ·_𝑠 ‘𝑃)⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ∪ {⟨(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}))
47	45, 46	sstri 3597	. 2 ⊢ {⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ⊆ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), (+_g‘𝑃)⟩, ⟨(._r‘ndx), (._r‘𝑃)⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·_𝑠 ‘ndx), ( ·_𝑠 ‘𝑃)⟩, ⟨(·_𝑖‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑆 Σ_g (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(·_𝑖‘(𝑅‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏_t‘(TopOpen ∘ 𝑅))⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^, < ))⟩} ∪ {⟨(Hom ‘ndx), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐 ∈ 𝐵 ↦ (𝑑 ∈ (𝑐(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))(2^nd ‘𝑎)), 𝑒 ∈ ((𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ X𝑥 ∈ 𝐼 ((𝑓‘𝑥)(Hom ‘(𝑅‘𝑥))(𝑔‘𝑥)))‘𝑎) ↦ (𝑥 ∈ 𝐼 ↦ ((𝑑‘𝑥)(⟨((1^st ‘𝑎)‘𝑥), ((2^nd ‘𝑎)‘𝑥)⟩(comp‘(𝑅‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩}))
48	21, 22, 23, 42, 47	prdsvallem 16030	1 ⊢ (𝜑 → 𝐷 = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ sup((ran (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)(dist‘(𝑅‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ^*, < )))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 = wceq 1480 ∈ wcel 1992 ∀wral 2912 ∃wrex 2913 {crab 2916 Vcvv 3191 ∪ cun 3558 ⊆ wss 3560 𝒫 cpw 4135 {csn 4153 {cpr 4155 {ctp 4157 ⟨cop 4159 ∪ cuni 4407 class class class wbr 4618 ↦ cmpt 4678 × cxp 5077 dom cdm 5079 ran crn 5080 ∘ ccom 5083 ⟶wf 5846 ‘cfv 5850 (class class class)co 6605 ↦ cmpt2 6607 1^st c1st 7114 2^nd c2nd 7115 Xcixp 7853 supcsup 8291 0cc0 9881 ℝ^*cxr 10018 < clt 10019 ndxcnx 15773 Basecbs 15776 +_gcplusg 15857 ._rcmulr 15858 Scalarcsca 15860 ·_𝑠 cvsca 15861 ·_𝑖cip 15862 TopSetcts 15863 lecple 15864 distcds 15866 Hom chom 15868 compcco 15869 TopOpenctopn 15998 ∏_tcpt 16015 Σ_g cgsu 16017 X_scprds 16022

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1841 ax-6 1890 ax-7 1937 ax-8 1994 ax-9 2001 ax-10 2021 ax-11 2036 ax-12 2049 ax-13 2250 ax-ext 2606 ax-sep 4746 ax-nul 4754 ax-pow 4808 ax-pr 4872 ax-un 6903 ax-cnex 9937 ax-resscn 9938 ax-1cn 9939 ax-icn 9940 ax-addcl 9941 ax-addrcl 9942 ax-mulcl 9943 ax-mulrcl 9944 ax-mulcom 9945 ax-addass 9946 ax-mulass 9947 ax-distr 9948 ax-i2m1 9949 ax-1ne0 9950 ax-1rid 9951 ax-rnegex 9952 ax-rrecex 9953 ax-cnre 9954 ax-pre-lttri 9955 ax-pre-lttrn 9956 ax-pre-ltadd 9957 ax-pre-mulgt0 9958

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1883 df-eu 2478 df-mo 2479 df-clab 2613 df-cleq 2619 df-clel 2622 df-nfc 2756 df-ne 2797 df-nel 2900 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3193 df-sbc 3423 df-csb 3520 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-pss 3576 df-nul 3897 df-if 4064 df-pw 4137 df-sn 4154 df-pr 4156 df-tp 4158 df-op 4160 df-uni 4408 df-int 4446 df-iun 4492 df-br 4619 df-opab 4679 df-mpt 4680 df-tr 4718 df-eprel 4990 df-id 4994 df-po 5000 df-so 5001 df-fr 5038 df-we 5040 df-xp 5085 df-rel 5086 df-cnv 5087 df-co 5088 df-dm 5089 df-rn 5090 df-res 5091 df-ima 5092 df-pred 5642 df-ord 5688 df-on 5689 df-lim 5690 df-suc 5691 df-iota 5813 df-fun 5852 df-fn 5853 df-f 5854 df-f1 5855 df-fo 5856 df-f1o 5857 df-fv 5858 df-riota 6566 df-ov 6608 df-oprab 6609 df-mpt2 6610 df-om 7014 df-1st 7116 df-2nd 7117 df-wrecs 7353 df-recs 7414 df-rdg 7452 df-1o 7506 df-oadd 7510 df-er 7688 df-map 7805 df-ixp 7854 df-en 7901 df-dom 7902 df-sdom 7903 df-fin 7904 df-sup 8293 df-pnf 10021 df-mnf 10022 df-xr 10023 df-ltxr 10024 df-le 10025 df-sub 10213 df-neg 10214 df-nn 10966 df-2 11024 df-3 11025 df-4 11026 df-5 11027 df-6 11028 df-7 11029 df-8 11030 df-9 11031 df-n0 11238 df-z 11323 df-dec 11438 df-uz 11632 df-fz 12266 df-struct 15778 df-ndx 15779 df-slot 15780 df-base 15781 df-plusg 15870 df-mulr 15871 df-sca 15873 df-vsca 15874 df-ip 15875 df-tset 15876 df-ple 15877 df-ds 15880 df-hom 15882 df-cco 15883 df-prds 16024

This theorem is referenced by: prdsdsfn 16041 prdstset 16042 prdshom 16043 prdsco 16044 prdsdsval 16054 prdsdsf 22077

W3C validator