Step |
Hyp |
Ref |
Expression |
1 |
|
prdsbas.p |
⊢ 𝑃 = ( 𝑆 Xs 𝑅 ) |
2 |
|
prdsbas.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) |
3 |
|
prdsbas.r |
⊢ ( 𝜑 → 𝑅 ∈ 𝑊 ) |
4 |
|
prdsbas.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
5 |
|
prdsbas.i |
⊢ ( 𝜑 → dom 𝑅 = 𝐼 ) |
6 |
|
prdsvsca.k |
⊢ 𝐾 = ( Base ‘ 𝑆 ) |
7 |
|
prdsvsca.m |
⊢ · = ( ·𝑠 ‘ 𝑃 ) |
8 |
1 2 3 4 5
|
prdsbas |
⊢ ( 𝜑 → 𝐵 = X 𝑥 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) |
9 |
|
eqid |
⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 ) |
10 |
1 2 3 4 5 9
|
prdsplusg |
⊢ ( 𝜑 → ( +g ‘ 𝑃 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) |
11 |
|
eqid |
⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 ) |
12 |
1 2 3 4 5 11
|
prdsmulr |
⊢ ( 𝜑 → ( .r ‘ 𝑃 ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) |
13 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) |
14 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) |
15 |
|
eqidd |
⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) |
16 |
|
eqidd |
⊢ ( 𝜑 → { 〈 𝑓 , 𝑔 〉 ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { 〈 𝑓 , 𝑔 〉 ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ) |
17 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( dist ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) ) |
18 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) |
19 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) 〉 ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) = ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) 〉 ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) ) |
20 |
1 6 5 8 10 12 13 14 15 16 17 18 19 2 3
|
prdsval |
⊢ ( 𝜑 → 𝑃 = ( ( { 〈 ( 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 ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) 〉 ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) 〉 } ) ) ) |
21 |
|
vscaid |
⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx ) |
22 |
|
ovssunirn |
⊢ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) |
23 |
21
|
strfvss |
⊢ ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ( 𝑅 ‘ 𝑥 ) |
24 |
|
fvssunirn |
⊢ ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran 𝑅 |
25 |
|
rnss |
⊢ ( ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran 𝑅 → ran ( 𝑅 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑅 ) |
26 |
|
uniss |
⊢ ( ran ( 𝑅 ‘ 𝑥 ) ⊆ ran ∪ ran 𝑅 → ∪ ran ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑅 ) |
27 |
24 25 26
|
mp2b |
⊢ ∪ ran ( 𝑅 ‘ 𝑥 ) ⊆ ∪ ran ∪ ran 𝑅 |
28 |
23 27
|
sstri |
⊢ ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅 |
29 |
|
rnss |
⊢ ( ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran 𝑅 → ran ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ran ∪ ran ∪ ran 𝑅 ) |
30 |
|
uniss |
⊢ ( ran ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ran ∪ ran ∪ ran 𝑅 → ∪ ran ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑅 ) |
31 |
28 29 30
|
mp2b |
⊢ ∪ ran ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑅 |
32 |
22 31
|
sstri |
⊢ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑅 |
33 |
|
ovex |
⊢ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ V |
34 |
33
|
elpw |
⊢ ( ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↔ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ⊆ ∪ ran ∪ ran ∪ ran 𝑅 ) |
35 |
32 34
|
mpbir |
⊢ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 |
36 |
35
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ∈ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ) |
37 |
36
|
fmpttd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ) |
38 |
|
rnexg |
⊢ ( 𝑅 ∈ 𝑊 → ran 𝑅 ∈ V ) |
39 |
|
uniexg |
⊢ ( ran 𝑅 ∈ V → ∪ ran 𝑅 ∈ V ) |
40 |
3 38 39
|
3syl |
⊢ ( 𝜑 → ∪ ran 𝑅 ∈ V ) |
41 |
|
rnexg |
⊢ ( ∪ ran 𝑅 ∈ V → ran ∪ ran 𝑅 ∈ V ) |
42 |
|
uniexg |
⊢ ( ran ∪ ran 𝑅 ∈ V → ∪ ran ∪ ran 𝑅 ∈ V ) |
43 |
40 41 42
|
3syl |
⊢ ( 𝜑 → ∪ ran ∪ ran 𝑅 ∈ V ) |
44 |
|
rnexg |
⊢ ( ∪ ran ∪ ran 𝑅 ∈ V → ran ∪ ran ∪ ran 𝑅 ∈ V ) |
45 |
|
uniexg |
⊢ ( ran ∪ ran ∪ ran 𝑅 ∈ V → ∪ ran ∪ ran ∪ ran 𝑅 ∈ V ) |
46 |
|
pwexg |
⊢ ( ∪ ran ∪ ran ∪ ran 𝑅 ∈ V → 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ∈ V ) |
47 |
43 44 45 46
|
4syl |
⊢ ( 𝜑 → 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ∈ V ) |
48 |
3
|
dmexd |
⊢ ( 𝜑 → dom 𝑅 ∈ V ) |
49 |
5 48
|
eqeltrrd |
⊢ ( 𝜑 → 𝐼 ∈ V ) |
50 |
47 49
|
elmapd |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ↔ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) : 𝐼 ⟶ 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ) ) |
51 |
37 50
|
mpbird |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ) |
52 |
51
|
ralrimivw |
⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ) |
53 |
52
|
ralrimivw |
⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐾 ∀ 𝑔 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ) |
54 |
|
eqid |
⊢ ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) |
55 |
54
|
fmpo |
⊢ ( ∀ 𝑓 ∈ 𝐾 ∀ 𝑔 ∈ 𝐵 ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ∈ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ↔ ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ) |
56 |
53 55
|
sylib |
⊢ ( 𝜑 → ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ) |
57 |
6
|
fvexi |
⊢ 𝐾 ∈ V |
58 |
4
|
fvexi |
⊢ 𝐵 ∈ V |
59 |
57 58
|
xpex |
⊢ ( 𝐾 × 𝐵 ) ∈ V |
60 |
|
ovex |
⊢ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ∈ V |
61 |
|
fex2 |
⊢ ( ( ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ∧ ( 𝐾 × 𝐵 ) ∈ V ∧ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) ∈ V ) → ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ∈ V ) |
62 |
59 60 61
|
mp3an23 |
⊢ ( ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) : ( 𝐾 × 𝐵 ) ⟶ ( 𝒫 ∪ ran ∪ ran ∪ ran 𝑅 ↑m 𝐼 ) → ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ∈ V ) |
63 |
56 62
|
syl |
⊢ ( 𝜑 → ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ∈ V ) |
64 |
|
snsstp2 |
⊢ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 } ⊆ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) 〉 } |
65 |
|
ssun2 |
⊢ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) 〉 } ⊆ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑃 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑃 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) 〉 } ) |
66 |
64 65
|
sstri |
⊢ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 } ⊆ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑃 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑃 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) 〉 } ) |
67 |
|
ssun1 |
⊢ ( { 〈 ( Base ‘ ndx ) , 𝐵 〉 , 〈 ( +g ‘ ndx ) , ( +g ‘ 𝑃 ) 〉 , 〈 ( .r ‘ ndx ) , ( .r ‘ 𝑃 ) 〉 } ∪ { 〈 ( Scalar ‘ ndx ) , 𝑆 〉 , 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 , 〈 ( ·𝑖 ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑆 Σg ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) ( ·𝑖 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) 〉 } ) ⊆ ( ( { 〈 ( 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 ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) 〉 ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) 〉 } ) ) |
68 |
66 67
|
sstri |
⊢ { 〈 ( ·𝑠 ‘ ndx ) , ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) 〉 } ⊆ ( ( { 〈 ( 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 ) , ( 𝑎 ∈ ( 𝐵 × 𝐵 ) , 𝑐 ∈ 𝐵 ↦ ( 𝑑 ∈ ( ( 2nd ‘ 𝑎 ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) 𝑐 ) , 𝑒 ∈ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ X 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ‘ 𝑎 ) ↦ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑑 ‘ 𝑥 ) ( 〈 ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) , ( ( 2nd ‘ 𝑎 ) ‘ 𝑥 ) 〉 ( comp ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑐 ‘ 𝑥 ) ) ( 𝑒 ‘ 𝑥 ) ) ) ) ) 〉 } ) ) |
69 |
20 7 21 63 68
|
prdsbaslem |
⊢ ( 𝜑 → · = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐵 ↦ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ( ·𝑠 ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ) ) ) |