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	⊢ 𝑃 = ( 𝑆 X_s 𝑅 )
	prdsbas.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	prdsbas.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	prdsbas.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
	prdshom.h	⊢ 𝐻 = ( Hom ‘ 𝑃 )
	prdsco.o	⊢ ∙ = ( comp ‘ 𝑃 )
Assertion	prdsco	⊢ ( 𝜑 → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	⊢ 𝑃 = ( 𝑆 X_s 𝑅 )
2		prdsbas.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		prdsbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4		prdsbas.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		prdsbas.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
6		prdshom.h	⊢ 𝐻 = ( Hom ‘ 𝑃 )
7		prdsco.o	⊢ ∙ = ( comp ‘ 𝑃 )
8		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9	1 2 3 4 5	prdsbas	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
10		eqid	⊢ ( +_g ‘ 𝑃 ) = ( +_g ‘ 𝑃 )
11	1 2 3 4 5 10	prdsplusg	⊢ ( 𝜑 → ( +_g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
12		eqid	⊢ ( ._r ‘ 𝑃 ) = ( ._r ‘ 𝑃 )
13	1 2 3 4 5 12	prdsmulr	⊢ ( 𝜑 → ( ._r ‘ 𝑃 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
14		eqid	⊢ ( ·_𝑠 ‘ 𝑃 ) = ( ·_𝑠 ‘ 𝑃 )
15	1 2 3 4 5 8 14	prdsvsca	⊢ ( 𝜑 → ( ·_𝑠 ‘ 𝑃 ) = ( 𝑓 ∈ ( Base ‘ 𝑆 ) , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
16		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
17		eqid	⊢ ( TopSet ‘ 𝑃 ) = ( TopSet ‘ 𝑃 )
18	1 2 3 4 5 17	prdstset	⊢ ( 𝜑 → ( TopSet ‘ 𝑃 ) = ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) )
19		eqid	⊢ ( le ‘ 𝑃 ) = ( le ‘ 𝑃 )
20	1 2 3 4 5 19	prdsle	⊢ ( 𝜑 → ( le ‘ 𝑃 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
21		eqid	⊢ ( dist ‘ 𝑃 ) = ( dist ‘ 𝑃 )
22	1 2 3 4 5 21	prdsds	⊢ ( 𝜑 → ( dist ‘ 𝑃 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
23	1 2 3 4 5 6	prdshom	⊢ ( 𝜑 → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
24		eqidd	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
25	1 8 5 9 11 13 15 16 18 20 22 23 24 2 3	prdsval	⊢ ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , ( +_g ‘ 𝑃 ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( ._r ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( ·_𝑠 ‘ 𝑃 ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( TopSet ‘ 𝑃 ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) )
26		ccoid	⊢ comp = Slot ( comp ‘ ndx )
27	4	fvexi	⊢ 𝐵 ∈ V
28	27 27	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
29	28 27	mpoex	⊢ ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ∈ V
30	29	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ∈ V )
31		snsspr2	⊢ { ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ⊆ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ }
32		ssun2	⊢ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( TopSet ‘ ndx ) , ( TopSet ‘ 𝑃 ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } )
33	31 32	sstri	⊢ { ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( TopSet ‘ ndx ) , ( TopSet ‘ 𝑃 ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } )
34		ssun2	⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( TopSet ‘ 𝑃 ) ⟩ , ⟨ ( le ‘ ndx ) , ( le ‘ 𝑃 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( dist ‘ 𝑃 ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( 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 ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
35	33 34	sstri	⊢ { ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( 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 ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) )
36	25 7 26 30 35	prdsbaslem	⊢ ( 𝜑 → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Theorem prdsco

Proof