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

Theorem prdshom 16569
Description: Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.)
Hypotheses
Ref Expression
prdsbas.p 𝑃 = (𝑆Xs𝑅)
prdsbas.s (𝜑𝑆𝑉)
prdsbas.r (𝜑𝑅𝑊)
prdsbas.b 𝐵 = (Base‘𝑃)
prdsbas.i (𝜑 → dom 𝑅 = 𝐼)
prdshom.h 𝐻 = (Hom ‘𝑃)
Assertion
Ref Expression
prdshom (𝜑𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
Distinct variable groups:   𝑓,𝑔,𝑥,𝐵   𝜑,𝑓,𝑔,𝑥   𝑓,𝐼,𝑔,𝑥   𝑃,𝑓,𝑔,𝑥   𝑅,𝑓,𝑔,𝑥   𝑆,𝑓,𝑔,𝑥
Allowed substitution hints:   𝐻(𝑥,𝑓,𝑔)   𝑉(𝑥,𝑓,𝑔)   𝑊(𝑥,𝑓,𝑔)

Proof of Theorem prdshom
Dummy variables 𝑎 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prdsbas.p . . 3 𝑃 = (𝑆Xs𝑅)
2 eqid 2794 . . 3 (Base‘𝑆) = (Base‘𝑆)
3 prdsbas.i . . 3 (𝜑 → dom 𝑅 = 𝐼)
4 prdsbas.s . . . 4 (𝜑𝑆𝑉)
5 prdsbas.r . . . 4 (𝜑𝑅𝑊)
6 prdsbas.b . . . 4 𝐵 = (Base‘𝑃)
71, 4, 5, 6, 3prdsbas 16559 . . 3 (𝜑𝐵 = X𝑥𝐼 (Base‘(𝑅𝑥)))
8 eqid 2794 . . . 4 (+g𝑃) = (+g𝑃)
91, 4, 5, 6, 3, 8prdsplusg 16560 . . 3 (𝜑 → (+g𝑃) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(+g‘(𝑅𝑥))(𝑔𝑥)))))
10 eqid 2794 . . . 4 (.r𝑃) = (.r𝑃)
111, 4, 5, 6, 3, 10prdsmulr 16561 . . 3 (𝜑 → (.r𝑃) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑥𝐼 ↦ ((𝑓𝑥)(.r‘(𝑅𝑥))(𝑔𝑥)))))
12 eqid 2794 . . . 4 ( ·𝑠𝑃) = ( ·𝑠𝑃)
131, 4, 5, 6, 3, 2, 12prdsvsca 16562 . . 3 (𝜑 → ( ·𝑠𝑃) = (𝑓 ∈ (Base‘𝑆), 𝑔𝐵 ↦ (𝑥𝐼 ↦ (𝑓( ·𝑠 ‘(𝑅𝑥))(𝑔𝑥)))))
14 eqidd 2795 . . 3 (𝜑 → (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))) = (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥))))))
15 eqid 2794 . . . 4 (TopSet‘𝑃) = (TopSet‘𝑃)
161, 4, 5, 6, 3, 15prdstset 16568 . . 3 (𝜑 → (TopSet‘𝑃) = (∏t‘(TopOpen ∘ 𝑅)))
17 eqid 2794 . . . 4 (le‘𝑃) = (le‘𝑃)
181, 4, 5, 6, 3, 17prdsle 16564 . . 3 (𝜑 → (le‘𝑃) = {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝐵 ∧ ∀𝑥𝐼 (𝑓𝑥)(le‘(𝑅𝑥))(𝑔𝑥))})
19 eqid 2794 . . . 4 (dist‘𝑃) = (dist‘𝑃)
201, 4, 5, 6, 3, 19prdsds 16566 . . 3 (𝜑 → (dist‘𝑃) = (𝑓𝐵, 𝑔𝐵 ↦ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)(dist‘(𝑅𝑥))(𝑔𝑥))) ∪ {0}), ℝ*, < )))
21 eqidd 2795 . . 3 (𝜑 → (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))) = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
22 eqidd 2795 . . 3 (𝜑 → (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))) = (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥))))))
231, 2, 3, 7, 9, 11, 13, 14, 16, 18, 20, 21, 22, 4, 5prdsval 16557 . 2 (𝜑𝑃 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), (+g𝑃)⟩, ⟨(.r‘ndx), (.r𝑃)⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), ( ·𝑠𝑃)⟩, ⟨(·𝑖‘ndx), (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (TopSet‘𝑃)⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (dist‘𝑃)⟩} ∪ {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})))
24 prdshom.h . 2 𝐻 = (Hom ‘𝑃)
25 homid 16517 . 2 Hom = Slot (Hom ‘ndx)
26 ovssunirn 7054 . . . . . . . . . . 11 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ ran (Hom ‘(𝑅𝑥))
2725strfvss 16335 . . . . . . . . . . . . 13 (Hom ‘(𝑅𝑥)) ⊆ ran (𝑅𝑥)
28 fvssunirn 6570 . . . . . . . . . . . . . 14 (𝑅𝑥) ⊆ ran 𝑅
29 rnss 5694 . . . . . . . . . . . . . 14 ((𝑅𝑥) ⊆ ran 𝑅 → ran (𝑅𝑥) ⊆ ran ran 𝑅)
30 uniss 4768 . . . . . . . . . . . . . 14 (ran (𝑅𝑥) ⊆ ran ran 𝑅 ran (𝑅𝑥) ⊆ ran ran 𝑅)
3128, 29, 30mp2b 10 . . . . . . . . . . . . 13 ran (𝑅𝑥) ⊆ ran ran 𝑅
3227, 31sstri 3900 . . . . . . . . . . . 12 (Hom ‘(𝑅𝑥)) ⊆ ran ran 𝑅
33 rnss 5694 . . . . . . . . . . . 12 ((Hom ‘(𝑅𝑥)) ⊆ ran ran 𝑅 → ran (Hom ‘(𝑅𝑥)) ⊆ ran ran ran 𝑅)
34 uniss 4768 . . . . . . . . . . . 12 (ran (Hom ‘(𝑅𝑥)) ⊆ ran ran ran 𝑅 ran (Hom ‘(𝑅𝑥)) ⊆ ran ran ran 𝑅)
3532, 33, 34mp2b 10 . . . . . . . . . . 11 ran (Hom ‘(𝑅𝑥)) ⊆ ran ran ran 𝑅
3626, 35sstri 3900 . . . . . . . . . 10 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑅
3736rgenw 3116 . . . . . . . . 9 𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑅
38 ss2ixp 8326 . . . . . . . . 9 (∀𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ ran ran ran 𝑅X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ X𝑥𝐼 ran ran ran 𝑅)
3937, 38ax-mp 5 . . . . . . . 8 X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ X𝑥𝐼 ran ran ran 𝑅
405dmexd 7474 . . . . . . . . . 10 (𝜑 → dom 𝑅 ∈ V)
413, 40eqeltrrd 2883 . . . . . . . . 9 (𝜑𝐼 ∈ V)
42 rnexg 7473 . . . . . . . . . . . 12 (𝑅𝑊 → ran 𝑅 ∈ V)
43 uniexg 7328 . . . . . . . . . . . 12 (ran 𝑅 ∈ V → ran 𝑅 ∈ V)
445, 42, 433syl 18 . . . . . . . . . . 11 (𝜑 ran 𝑅 ∈ V)
45 rnexg 7473 . . . . . . . . . . 11 ( ran 𝑅 ∈ V → ran ran 𝑅 ∈ V)
46 uniexg 7328 . . . . . . . . . . 11 (ran ran 𝑅 ∈ V → ran ran 𝑅 ∈ V)
4744, 45, 463syl 18 . . . . . . . . . 10 (𝜑 ran ran 𝑅 ∈ V)
48 rnexg 7473 . . . . . . . . . 10 ( ran ran 𝑅 ∈ V → ran ran ran 𝑅 ∈ V)
49 uniexg 7328 . . . . . . . . . 10 (ran ran ran 𝑅 ∈ V → ran ran ran 𝑅 ∈ V)
5047, 48, 493syl 18 . . . . . . . . 9 (𝜑 ran ran ran 𝑅 ∈ V)
51 ixpconstg 8322 . . . . . . . . 9 ((𝐼 ∈ V ∧ ran ran ran 𝑅 ∈ V) → X𝑥𝐼 ran ran ran 𝑅 = ( ran ran ran 𝑅𝑚 𝐼))
5241, 50, 51syl2anc 584 . . . . . . . 8 (𝜑X𝑥𝐼 ran ran ran 𝑅 = ( ran ran ran 𝑅𝑚 𝐼))
5339, 52sseqtrid 3942 . . . . . . 7 (𝜑X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ ( ran ran ran 𝑅𝑚 𝐼))
54 ovex 7051 . . . . . . . 8 ( ran ran ran 𝑅𝑚 𝐼) ∈ V
5554elpw2 5142 . . . . . . 7 (X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑅𝑚 𝐼) ↔ X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ⊆ ( ran ran ran 𝑅𝑚 𝐼))
5653, 55sylibr 235 . . . . . 6 (𝜑X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑅𝑚 𝐼))
5756ralrimivw 3149 . . . . 5 (𝜑 → ∀𝑔𝐵 X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑅𝑚 𝐼))
5857ralrimivw 3149 . . . 4 (𝜑 → ∀𝑓𝐵𝑔𝐵 X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑅𝑚 𝐼))
59 eqid 2794 . . . . 5 (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))) = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))
6059fmpo 7625 . . . 4 (∀𝑓𝐵𝑔𝐵 X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)) ∈ 𝒫 ( ran ran ran 𝑅𝑚 𝐼) ↔ (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))):(𝐵 × 𝐵)⟶𝒫 ( ran ran ran 𝑅𝑚 𝐼))
6158, 60sylib 219 . . 3 (𝜑 → (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))):(𝐵 × 𝐵)⟶𝒫 ( ran ran ran 𝑅𝑚 𝐼))
626fvexi 6555 . . . . 5 𝐵 ∈ V
6362, 62xpex 7336 . . . 4 (𝐵 × 𝐵) ∈ V
6463a1i 11 . . 3 (𝜑 → (𝐵 × 𝐵) ∈ V)
6554pwex 5175 . . . 4 𝒫 ( ran ran ran 𝑅𝑚 𝐼) ∈ V
6665a1i 11 . . 3 (𝜑 → 𝒫 ( ran ran ran 𝑅𝑚 𝐼) ∈ V)
67 fex2 7497 . . 3 (((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))):(𝐵 × 𝐵)⟶𝒫 ( ran ran ran 𝑅𝑚 𝐼) ∧ (𝐵 × 𝐵) ∈ V ∧ 𝒫 ( ran ran ran 𝑅𝑚 𝐼) ∈ V) → (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))) ∈ V)
6861, 64, 66, 67syl3anc 1364 . 2 (𝜑 → (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))) ∈ V)
69 snsspr1 4656 . . . 4 {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩} ⊆ {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}
70 ssun2 4072 . . . 4 {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩} ⊆ ({⟨(TopSet‘ndx), (TopSet‘𝑃)⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (dist‘𝑃)⟩} ∪ {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})
7169, 70sstri 3900 . . 3 {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩} ⊆ ({⟨(TopSet‘ndx), (TopSet‘𝑃)⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (dist‘𝑃)⟩} ∪ {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩})
72 ssun2 4072 . . 3 ({⟨(TopSet‘ndx), (TopSet‘𝑃)⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (dist‘𝑃)⟩} ∪ {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}) ⊆ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), (+g𝑃)⟩, ⟨(.r‘ndx), (.r𝑃)⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), ( ·𝑠𝑃)⟩, ⟨(·𝑖‘ndx), (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (TopSet‘𝑃)⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (dist‘𝑃)⟩} ∪ {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}))
7371, 72sstri 3900 . 2 {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩} ⊆ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), (+g𝑃)⟩, ⟨(.r‘ndx), (.r𝑃)⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), ( ·𝑠𝑃)⟩, ⟨(·𝑖‘ndx), (𝑓𝐵, 𝑔𝐵 ↦ (𝑆 Σg (𝑥𝐼 ↦ ((𝑓𝑥)(·𝑖‘(𝑅𝑥))(𝑔𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (TopSet‘𝑃)⟩, ⟨(le‘ndx), (le‘𝑃)⟩, ⟨(dist‘ndx), (dist‘𝑃)⟩} ∪ {⟨(Hom ‘ndx), (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝐵 × 𝐵), 𝑐𝐵 ↦ (𝑑 ∈ (𝑐(𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))(2nd𝑎)), 𝑒 ∈ ((𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥)))‘𝑎) ↦ (𝑥𝐼 ↦ ((𝑑𝑥)(⟨((1st𝑎)‘𝑥), ((2nd𝑎)‘𝑥)⟩(comp‘(𝑅𝑥))(𝑐𝑥))(𝑒𝑥)))))⟩}))
7423, 24, 25, 68, 73prdsvallem 16556 1 (𝜑𝐻 = (𝑓𝐵, 𝑔𝐵X𝑥𝐼 ((𝑓𝑥)(Hom ‘(𝑅𝑥))(𝑔𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1522  wcel 2080  wral 3104  Vcvv 3436  cun 3859  wss 3861  𝒫 cpw 4455  {csn 4474  {cpr 4476  {ctp 4478  cop 4480   cuni 4747  cmpt 5043   × cxp 5444  dom cdm 5446  ran crn 5447  wf 6224  cfv 6228  (class class class)co 7019  cmpo 7021  1st c1st 7546  2nd c2nd 7547  𝑚 cmap 8259  Xcixp 8313  ndxcnx 16309  Basecbs 16312  +gcplusg 16394  .rcmulr 16395  Scalarcsca 16397   ·𝑠 cvsca 16398  ·𝑖cip 16399  TopSetcts 16400  lecple 16401  distcds 16403  Hom chom 16405  compcco 16406   Σg cgsu 16543  Xscprds 16548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-cnex 10442  ax-resscn 10443  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-addrcl 10447  ax-mulcl 10448  ax-mulrcl 10449  ax-mulcom 10450  ax-addass 10451  ax-mulass 10452  ax-distr 10453  ax-i2m1 10454  ax-1ne0 10455  ax-1rid 10456  ax-rnegex 10457  ax-rrecex 10458  ax-cnre 10459  ax-pre-lttri 10460  ax-pre-lttrn 10461  ax-pre-ltadd 10462  ax-pre-mulgt0 10463
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-nel 3090  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-int 4785  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-riota 6980  df-ov 7022  df-oprab 7023  df-mpo 7024  df-om 7440  df-1st 7548  df-2nd 7549  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-oadd 7960  df-er 8142  df-map 8261  df-ixp 8314  df-en 8361  df-dom 8362  df-sdom 8363  df-fin 8364  df-sup 8755  df-pnf 10526  df-mnf 10527  df-xr 10528  df-ltxr 10529  df-le 10530  df-sub 10721  df-neg 10722  df-nn 11489  df-2 11550  df-3 11551  df-4 11552  df-5 11553  df-6 11554  df-7 11555  df-8 11556  df-9 11557  df-n0 11748  df-z 11832  df-dec 11949  df-uz 12094  df-fz 12743  df-struct 16314  df-ndx 16315  df-slot 16316  df-base 16318  df-plusg 16407  df-mulr 16408  df-sca 16410  df-vsca 16411  df-ip 16412  df-tset 16413  df-ple 16414  df-ds 16416  df-hom 16418  df-cco 16419  df-prds 16550
This theorem is referenced by:  prdsco  16570
  Copyright terms: Public domain W3C validator