prdsval

Description: Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

	Ref	Expression
Hypotheses	prdsval.p	⊢ 𝑃 = ( 𝑆 X_s 𝑅 )
	prdsval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	prdsval.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
	prdsval.b	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
	prdsval.a	⊢ ( 𝜑 → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
	prdsval.t	⊢ ( 𝜑 → × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
	prdsval.m	⊢ ( 𝜑 → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
	prdsval.j	⊢ ( 𝜑 → , = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
	prdsval.o	⊢ ( 𝜑 → 𝑂 = ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) )
	prdsval.l	⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
	prdsval.d	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
	prdsval.h	⊢ ( 𝜑 → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
	prdsval.x	⊢ ( 𝜑 → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
	prdsval.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	prdsval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
Assertion	prdsval	⊢ ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		prdsval.p	⊢ 𝑃 = ( 𝑆 X_s 𝑅 )
2		prdsval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
3		prdsval.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
4		prdsval.b	⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
5		prdsval.a	⊢ ( 𝜑 → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
6		prdsval.t	⊢ ( 𝜑 → × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
7		prdsval.m	⊢ ( 𝜑 → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
8		prdsval.j	⊢ ( 𝜑 → , = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
9		prdsval.o	⊢ ( 𝜑 → 𝑂 = ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) )
10		prdsval.l	⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
11		prdsval.d	⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
12		prdsval.h	⊢ ( 𝜑 → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
13		prdsval.x	⊢ ( 𝜑 → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
14		prdsval.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
15		prdsval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
16		df-prds	⊢ X_s = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) )
17	16	a1i	⊢ ( 𝜑 → X_s = ( 𝑠 ∈ V , 𝑟 ∈ V ↦ ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) ) )
18		vex	⊢ 𝑟 ∈ V
19	18	rnex	⊢ ran 𝑟 ∈ V
20	19	uniex	⊢ ∪ ran 𝑟 ∈ V
21	20	rnex	⊢ ran ∪ ran 𝑟 ∈ V
22	21	uniex	⊢ ∪ ran ∪ ran 𝑟 ∈ V
23		baseid	⊢ Base = Slot ( Base ‘ ndx )
24	23	strfvss	⊢ ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ( 𝑟 ‘ 𝑥 )
25		fvssunirn	⊢ ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran 𝑟
26		rnss	⊢ ( ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran 𝑟 → ran ( 𝑟 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑟 )
27		uniss	⊢ ( ran ( 𝑟 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑟 → ∪ ran ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑟 )
28	25 26 27	mp2b	⊢ ∪ ran ( 𝑟 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑟
29	24 28	sstri	⊢ ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
30	29	rgenw	⊢ ∀ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
31		iunss	⊢ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟 ↔ ∀ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟 )
32	30 31	mpbir	⊢ ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑟
33	22 32	ssexi	⊢ ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V
34		ixpssmap2g	⊢ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑_m dom 𝑟 ) )
35	33 34	ax-mp	⊢ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑_m dom 𝑟 )
36		ovex	⊢ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑_m dom 𝑟 ) ∈ V
37	36	ssex	⊢ ( X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ⊆ ( ∪ 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ↑_m dom 𝑟 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V )
38	35 37	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) ∈ V )
39		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
40	39	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑟 ‘ 𝑥 ) = ( 𝑅 ‘ 𝑥 ) )
41	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
42	41	ixpeq2dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
43	39	dmeqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → dom 𝑟 = dom 𝑅 )
44	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → dom 𝑅 = 𝐼 )
45	43 44	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → dom 𝑟 = 𝐼 )
46	45	ixpeq1d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) )
47	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
48	42 46 47	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) = 𝐵 )
49		prdsvallem	⊢ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V
50	49	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ V )
51		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝑣 = 𝐵 )
52	45	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → dom 𝑟 = 𝐼 )
53	52	ixpeq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
54	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) = ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) )
55	54	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
56	55	ixpeq2dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
57	56	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
58	53 57	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
59	51 51 58	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
60	12	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝐻 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
61	59 60	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = 𝐻 )
62		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑣 = 𝐵 )
63	62	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
64	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) = ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) )
65	64	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
66	45 65	mpteq12dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
67	66	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
68	51 51 67	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
69	68	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
70	5	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → + = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
71	69 70	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = + )
72	71	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( +_g ‘ ndx ) , + ⟩ )
73	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) = ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) )
74	73	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
75	45 74	mpteq12dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
76	75	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
77	51 51 76	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
78	77	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
79	6	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → × = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
80	78 79	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = × )
81	80	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( ._r ‘ ndx ) , × ⟩ )
82	63 72 81	tpeq123d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } )
83		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑠 = 𝑆 )
84	83	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ )
85		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → 𝑠 = 𝑆 )
86	85	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
87	86 2	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( Base ‘ 𝑠 ) = 𝐾 )
88	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) = ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) )
89	88	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
90	45 89	mpteq12dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
91	90	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
92	87 51 91	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
93	92	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
94	7	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
95	93 94	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = · )
96	95	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ = ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ )
97	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) = ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) )
98	97	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
99	45 98	mpteq12dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
100	99	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
101	85 100	oveq12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) )
102	51 51 101	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
103	102	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
104	8	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → , = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σ_g ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
105	103 104	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = , )
106	105	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ )
107	84 96 106	tpeq123d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } )
108	82 107	uneq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) )
109		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑟 = 𝑅 )
110	109	coeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( TopOpen ∘ 𝑟 ) = ( TopOpen ∘ 𝑅 ) )
111	110	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) = ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) )
112	9	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝑂 = ( ∏_t ‘ ( TopOpen ∘ 𝑅 ) ) )
113	111 112	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) = 𝑂 )
114	113	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ = ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ )
115	51	sseq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( { 𝑓 , 𝑔 } ⊆ 𝑣 ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 ) )
116	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( le ‘ ( 𝑟 ‘ 𝑥 ) ) = ( le ‘ ( 𝑅 ‘ 𝑥 ) ) )
117	116	breqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
118	45 117	raleqbidv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
119	118	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
120	115 119	anbi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
121	120	opabbidv	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
122	121	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
123	10	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
124	122 123	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = ≤ )
125	124	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
126	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) )
127	126	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
128	45 127	mpteq12dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
129	128	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
130	129	rneqd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) )
131	130	uneq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) = ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
132	131	supeq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) )
133	51 51 132	mpoeq123dv	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
134	133	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
135	11	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) )
136	134 135	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) = 𝐷 )
137	136	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ = ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ )
138	114 125 137	tpeq123d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } = { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
139		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
140	139	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( Hom ‘ ndx ) , ℎ ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
141	62	sqxpeqd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑣 × 𝑣 ) = ( 𝐵 × 𝐵 ) )
142	139	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) = ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) )
143	139	fveq1d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ℎ ‘ 𝑎 ) = ( 𝐻 ‘ 𝑎 ) )
144	40	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) = ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) )
145	144	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) = ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) )
146	145	oveqd	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) = ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) )
147	45 146	mpteq12dv	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) )
148	147	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) )
149	142 143 148	mpoeq123dv	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) = ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) )
150	141 62 149	mpoeq123dv	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
151	13	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ∙ = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) 𝐻 𝑐 ) , 𝑒 ∈ ( 𝐻 ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) )
152	150 151	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ∙ )
153	152	opeq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , ∙ ⟩ )
154	140 153	preq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } )
155	138 154	uneq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) = ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) )
156	108 155	uneq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) ∧ ℎ = 𝐻 ) → ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
157	50 61 156	csbied2	⊢ ( ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) ∧ 𝑣 = 𝐵 ) → ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
158	38 48 157	csbied2	⊢ ( ( ( 𝜑 ∧ 𝑠 = 𝑆 ) ∧ 𝑟 = 𝑅 ) → ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
159	158	anasss	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑟 = 𝑅 ) ) → ⦋ X 𝑥 ∈ dom 𝑟 ( Base ‘ ( 𝑟 ‘ 𝑥 ) ) / 𝑣 ⦌ ⦋ ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ X 𝑥 ∈ dom 𝑟 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) / ℎ ⦌ ( ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +_g ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +_g ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ._r ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ._r ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑠 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , ( 𝑓 ∈ ( Base ‘ 𝑠 ) , 𝑔 ∈ 𝑣 ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( 𝑓 ( ·_𝑠 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ ( 𝑠 Σ_g ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·_𝑖 ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( ∏_t ‘ ( TopOpen ∘ 𝑟 ) ) ⟩ , ⟨ ( le ‘ ndx ) , { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝑣 ∧ ∀ 𝑥 ∈ dom 𝑟 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑓 ∈ 𝑣 , 𝑔 ∈ 𝑣 ↦ sup ( ( ran ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ^* , < ) ) ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , ℎ ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑎 ∈ ( 𝑣 × 𝑣 ) , 𝑐 ∈ 𝑣 ↦ ( 𝑑 ∈ ( ( 2^nd ‘ 𝑎 ) ℎ 𝑐 ) , 𝑒 ∈ ( ℎ ‘ 𝑎 ) ↦ ( 𝑥 ∈ dom 𝑟 ↦ ( ( 𝑑 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2^nd ‘ 𝑎 ) ‘ 𝑥 ) ⟩ ( comp ‘ ( 𝑟 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ⟩ } ) ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
160	14	elexd	⊢ ( 𝜑 → 𝑆 ∈ V )
161	15	elexd	⊢ ( 𝜑 → 𝑅 ∈ V )
162		tpex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∈ V
163		tpex	⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ∈ V
164	162 163	unex	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∈ V
165		tpex	⊢ { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∈ V
166		prex	⊢ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ∈ V
167	165 166	unex	⊢ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ∈ V
168	164 167	unex	⊢ ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) ∈ V
169	168	a1i	⊢ ( 𝜑 → ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) ∈ V )
170	17 159 160 161 169	ovmpod	⊢ ( 𝜑 → ( 𝑆 X_s 𝑅 ) = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )
171	1 170	eqtrid	⊢ ( 𝜑 → 𝑃 = ( ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +_g ‘ ndx ) , + ⟩ , ⟨ ( ._r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·_𝑠 ‘ ndx ) , · ⟩ , ⟨ ( ·_𝑖 ‘ ndx ) , , ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , 𝑂 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∪ { ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , ∙ ⟩ } ) ) )

Metamath Proof Explorer

Theorem prdsval

Proof