Metamath Proof Explorer


Theorem 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)

Ref Expression
Hypotheses prdsval.p P = S 𝑠 R
prdsval.k K = Base S
prdsval.i φ dom R = I
prdsval.b φ B = x I Base R x
prdsval.a φ + ˙ = f B , g B x I f x + R x g x
prdsval.t φ × ˙ = f B , g B x I f x R x g x
prdsval.m φ · ˙ = f K , g B x I f R x g x
prdsval.j φ , ˙ = f B , g B S x I f x 𝑖 R x g x
prdsval.o φ O = 𝑡 TopOpen R
prdsval.l φ ˙ = f g | f g B x I f x R x g x
prdsval.d φ D = f B , g B sup ran x I f x dist R x g x 0 * <
prdsval.h φ H = f B , g B x I f x Hom R x g x
prdsval.x φ ˙ = a B × B , c B d c H 2 nd a , e H a x I d x 1 st a x 2 nd a x comp R x c x e x
prdsval.s φ S W
prdsval.r φ R Z
Assertion prdsval φ P = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙

Proof

Step Hyp Ref Expression
1 prdsval.p P = S 𝑠 R
2 prdsval.k K = Base S
3 prdsval.i φ dom R = I
4 prdsval.b φ B = x I Base R x
5 prdsval.a φ + ˙ = f B , g B x I f x + R x g x
6 prdsval.t φ × ˙ = f B , g B x I f x R x g x
7 prdsval.m φ · ˙ = f K , g B x I f R x g x
8 prdsval.j φ , ˙ = f B , g B S x I f x 𝑖 R x g x
9 prdsval.o φ O = 𝑡 TopOpen R
10 prdsval.l φ ˙ = f g | f g B x I f x R x g x
11 prdsval.d φ D = f B , g B sup ran x I f x dist R x g x 0 * <
12 prdsval.h φ H = f B , g B x I f x Hom R x g x
13 prdsval.x φ ˙ = a B × B , c B d c H 2 nd a , e H a x I d x 1 st a x 2 nd a x comp R x c x e x
14 prdsval.s φ S W
15 prdsval.r φ R Z
16 df-prds 𝑠 = s V , r V x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
17 16 a1i φ 𝑠 = s V , r V x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
18 vex r V
19 18 rnex ran r V
20 19 uniex ran r V
21 20 rnex ran ran r V
22 21 uniex ran ran r V
23 baseid Base = Slot Base ndx
24 23 strfvss Base r x ran r x
25 fvssunirn r x ran r
26 rnss r x ran r ran r x ran ran r
27 uniss ran r x ran ran r ran r x ran ran r
28 25 26 27 mp2b ran r x ran ran r
29 24 28 sstri Base r x ran ran r
30 29 rgenw x dom r Base r x ran ran r
31 iunss x dom r Base r x ran ran r x dom r Base r x ran ran r
32 30 31 mpbir x dom r Base r x ran ran r
33 22 32 ssexi x dom r Base r x V
34 ixpssmap2g x dom r Base r x V x dom r Base r x x dom r Base r x dom r
35 33 34 ax-mp x dom r Base r x x dom r Base r x dom r
36 ovex x dom r Base r x dom r V
37 36 ssex x dom r Base r x x dom r Base r x dom r x dom r Base r x V
38 35 37 mp1i φ s = S r = R x dom r Base r x V
39 simpr φ s = S r = R r = R
40 39 fveq1d φ s = S r = R r x = R x
41 40 fveq2d φ s = S r = R Base r x = Base R x
42 41 ixpeq2dv φ s = S r = R x I Base r x = x I Base R x
43 39 dmeqd φ s = S r = R dom r = dom R
44 3 ad2antrr φ s = S r = R dom R = I
45 43 44 eqtrd φ s = S r = R dom r = I
46 45 ixpeq1d φ s = S r = R x dom r Base r x = x I Base r x
47 4 ad2antrr φ s = S r = R B = x I Base R x
48 42 46 47 3eqtr4d φ s = S r = R x dom r Base r x = B
49 ovex ran ran ran r dom r V
50 ovssunirn f x Hom r x g x ran Hom r x
51 df-hom Hom = Slot 14
52 51 strfvss Hom r x ran r x
53 52 28 sstri Hom r x ran ran r
54 rnss Hom r x ran ran r ran Hom r x ran ran ran r
55 uniss ran Hom r x ran ran ran r ran Hom r x ran ran ran r
56 53 54 55 mp2b ran Hom r x ran ran ran r
57 50 56 sstri f x Hom r x g x ran ran ran r
58 57 rgenw x dom r f x Hom r x g x ran ran ran r
59 ss2ixp x dom r f x Hom r x g x ran ran ran r x dom r f x Hom r x g x x dom r ran ran ran r
60 58 59 ax-mp x dom r f x Hom r x g x x dom r ran ran ran r
61 18 dmex dom r V
62 22 rnex ran ran ran r V
63 62 uniex ran ran ran r V
64 61 63 ixpconst x dom r ran ran ran r = ran ran ran r dom r
65 60 64 sseqtri x dom r f x Hom r x g x ran ran ran r dom r
66 49 65 elpwi2 x dom r f x Hom r x g x 𝒫 ran ran ran r dom r
67 66 rgen2w f v g v x dom r f x Hom r x g x 𝒫 ran ran ran r dom r
68 eqid f v , g v x dom r f x Hom r x g x = f v , g v x dom r f x Hom r x g x
69 68 fmpo f v g v x dom r f x Hom r x g x 𝒫 ran ran ran r dom r f v , g v x dom r f x Hom r x g x : v × v 𝒫 ran ran ran r dom r
70 67 69 mpbi f v , g v x dom r f x Hom r x g x : v × v 𝒫 ran ran ran r dom r
71 vex v V
72 71 71 xpex v × v V
73 49 pwex 𝒫 ran ran ran r dom r V
74 fex2 f v , g v x dom r f x Hom r x g x : v × v 𝒫 ran ran ran r dom r v × v V 𝒫 ran ran ran r dom r V f v , g v x dom r f x Hom r x g x V
75 70 72 73 74 mp3an f v , g v x dom r f x Hom r x g x V
76 75 a1i φ s = S r = R v = B f v , g v x dom r f x Hom r x g x V
77 simpr φ s = S r = R v = B v = B
78 45 adantr φ s = S r = R v = B dom r = I
79 78 ixpeq1d φ s = S r = R v = B x dom r f x Hom r x g x = x I f x Hom r x g x
80 40 fveq2d φ s = S r = R Hom r x = Hom R x
81 80 oveqd φ s = S r = R f x Hom r x g x = f x Hom R x g x
82 81 ixpeq2dv φ s = S r = R x I f x Hom r x g x = x I f x Hom R x g x
83 82 adantr φ s = S r = R v = B x I f x Hom r x g x = x I f x Hom R x g x
84 79 83 eqtrd φ s = S r = R v = B x dom r f x Hom r x g x = x I f x Hom R x g x
85 77 77 84 mpoeq123dv φ s = S r = R v = B f v , g v x dom r f x Hom r x g x = f B , g B x I f x Hom R x g x
86 12 ad3antrrr φ s = S r = R v = B H = f B , g B x I f x Hom R x g x
87 85 86 eqtr4d φ s = S r = R v = B f v , g v x dom r f x Hom r x g x = H
88 simplr φ s = S r = R v = B h = H v = B
89 88 opeq2d φ s = S r = R v = B h = H Base ndx v = Base ndx B
90 40 fveq2d φ s = S r = R + r x = + R x
91 90 oveqd φ s = S r = R f x + r x g x = f x + R x g x
92 45 91 mpteq12dv φ s = S r = R x dom r f x + r x g x = x I f x + R x g x
93 92 adantr φ s = S r = R v = B x dom r f x + r x g x = x I f x + R x g x
94 77 77 93 mpoeq123dv φ s = S r = R v = B f v , g v x dom r f x + r x g x = f B , g B x I f x + R x g x
95 94 adantr φ s = S r = R v = B h = H f v , g v x dom r f x + r x g x = f B , g B x I f x + R x g x
96 5 ad4antr φ s = S r = R v = B h = H + ˙ = f B , g B x I f x + R x g x
97 95 96 eqtr4d φ s = S r = R v = B h = H f v , g v x dom r f x + r x g x = + ˙
98 97 opeq2d φ s = S r = R v = B h = H + ndx f v , g v x dom r f x + r x g x = + ndx + ˙
99 40 fveq2d φ s = S r = R r x = R x
100 99 oveqd φ s = S r = R f x r x g x = f x R x g x
101 45 100 mpteq12dv φ s = S r = R x dom r f x r x g x = x I f x R x g x
102 101 adantr φ s = S r = R v = B x dom r f x r x g x = x I f x R x g x
103 77 77 102 mpoeq123dv φ s = S r = R v = B f v , g v x dom r f x r x g x = f B , g B x I f x R x g x
104 103 adantr φ s = S r = R v = B h = H f v , g v x dom r f x r x g x = f B , g B x I f x R x g x
105 6 ad4antr φ s = S r = R v = B h = H × ˙ = f B , g B x I f x R x g x
106 104 105 eqtr4d φ s = S r = R v = B h = H f v , g v x dom r f x r x g x = × ˙
107 106 opeq2d φ s = S r = R v = B h = H ndx f v , g v x dom r f x r x g x = ndx × ˙
108 89 98 107 tpeq123d φ s = S r = R v = B h = H Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x = Base ndx B + ndx + ˙ ndx × ˙
109 simp-4r φ s = S r = R v = B h = H s = S
110 109 opeq2d φ s = S r = R v = B h = H Scalar ndx s = Scalar ndx S
111 simpllr φ s = S r = R v = B s = S
112 111 fveq2d φ s = S r = R v = B Base s = Base S
113 112 2 syl6eqr φ s = S r = R v = B Base s = K
114 40 fveq2d φ s = S r = R r x = R x
115 114 oveqd φ s = S r = R f r x g x = f R x g x
116 45 115 mpteq12dv φ s = S r = R x dom r f r x g x = x I f R x g x
117 116 adantr φ s = S r = R v = B x dom r f r x g x = x I f R x g x
118 113 77 117 mpoeq123dv φ s = S r = R v = B f Base s , g v x dom r f r x g x = f K , g B x I f R x g x
119 118 adantr φ s = S r = R v = B h = H f Base s , g v x dom r f r x g x = f K , g B x I f R x g x
120 7 ad4antr φ s = S r = R v = B h = H · ˙ = f K , g B x I f R x g x
121 119 120 eqtr4d φ s = S r = R v = B h = H f Base s , g v x dom r f r x g x = · ˙
122 121 opeq2d φ s = S r = R v = B h = H ndx f Base s , g v x dom r f r x g x = ndx · ˙
123 40 fveq2d φ s = S r = R 𝑖 r x = 𝑖 R x
124 123 oveqd φ s = S r = R f x 𝑖 r x g x = f x 𝑖 R x g x
125 45 124 mpteq12dv φ s = S r = R x dom r f x 𝑖 r x g x = x I f x 𝑖 R x g x
126 125 adantr φ s = S r = R v = B x dom r f x 𝑖 r x g x = x I f x 𝑖 R x g x
127 111 126 oveq12d φ s = S r = R v = B s x dom r f x 𝑖 r x g x = S x I f x 𝑖 R x g x
128 77 77 127 mpoeq123dv φ s = S r = R v = B f v , g v s x dom r f x 𝑖 r x g x = f B , g B S x I f x 𝑖 R x g x
129 128 adantr φ s = S r = R v = B h = H f v , g v s x dom r f x 𝑖 r x g x = f B , g B S x I f x 𝑖 R x g x
130 8 ad4antr φ s = S r = R v = B h = H , ˙ = f B , g B S x I f x 𝑖 R x g x
131 129 130 eqtr4d φ s = S r = R v = B h = H f v , g v s x dom r f x 𝑖 r x g x = , ˙
132 131 opeq2d φ s = S r = R v = B h = H 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x = 𝑖 ndx , ˙
133 110 122 132 tpeq123d φ s = S r = R v = B h = H Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x = Scalar ndx S ndx · ˙ 𝑖 ndx , ˙
134 108 133 uneq12d φ s = S r = R v = B h = H Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙
135 simpllr φ s = S r = R v = B h = H r = R
136 135 coeq2d φ s = S r = R v = B h = H TopOpen r = TopOpen R
137 136 fveq2d φ s = S r = R v = B h = H 𝑡 TopOpen r = 𝑡 TopOpen R
138 9 ad4antr φ s = S r = R v = B h = H O = 𝑡 TopOpen R
139 137 138 eqtr4d φ s = S r = R v = B h = H 𝑡 TopOpen r = O
140 139 opeq2d φ s = S r = R v = B h = H TopSet ndx 𝑡 TopOpen r = TopSet ndx O
141 77 sseq2d φ s = S r = R v = B f g v f g B
142 40 fveq2d φ s = S r = R r x = R x
143 142 breqd φ s = S r = R f x r x g x f x R x g x
144 45 143 raleqbidv φ s = S r = R x dom r f x r x g x x I f x R x g x
145 144 adantr φ s = S r = R v = B x dom r f x r x g x x I f x R x g x
146 141 145 anbi12d φ s = S r = R v = B f g v x dom r f x r x g x f g B x I f x R x g x
147 146 opabbidv φ s = S r = R v = B f g | f g v x dom r f x r x g x = f g | f g B x I f x R x g x
148 147 adantr φ s = S r = R v = B h = H f g | f g v x dom r f x r x g x = f g | f g B x I f x R x g x
149 10 ad4antr φ s = S r = R v = B h = H ˙ = f g | f g B x I f x R x g x
150 148 149 eqtr4d φ s = S r = R v = B h = H f g | f g v x dom r f x r x g x = ˙
151 150 opeq2d φ s = S r = R v = B h = H ndx f g | f g v x dom r f x r x g x = ndx ˙
152 40 fveq2d φ s = S r = R dist r x = dist R x
153 152 oveqd φ s = S r = R f x dist r x g x = f x dist R x g x
154 45 153 mpteq12dv φ s = S r = R x dom r f x dist r x g x = x I f x dist R x g x
155 154 adantr φ s = S r = R v = B x dom r f x dist r x g x = x I f x dist R x g x
156 155 rneqd φ s = S r = R v = B ran x dom r f x dist r x g x = ran x I f x dist R x g x
157 156 uneq1d φ s = S r = R v = B ran x dom r f x dist r x g x 0 = ran x I f x dist R x g x 0
158 157 supeq1d φ s = S r = R v = B sup ran x dom r f x dist r x g x 0 * < = sup ran x I f x dist R x g x 0 * <
159 77 77 158 mpoeq123dv φ s = S r = R v = B f v , g v sup ran x dom r f x dist r x g x 0 * < = f B , g B sup ran x I f x dist R x g x 0 * <
160 159 adantr φ s = S r = R v = B h = H f v , g v sup ran x dom r f x dist r x g x 0 * < = f B , g B sup ran x I f x dist R x g x 0 * <
161 11 ad4antr φ s = S r = R v = B h = H D = f B , g B sup ran x I f x dist R x g x 0 * <
162 160 161 eqtr4d φ s = S r = R v = B h = H f v , g v sup ran x dom r f x dist r x g x 0 * < = D
163 162 opeq2d φ s = S r = R v = B h = H dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < = dist ndx D
164 140 151 163 tpeq123d φ s = S r = R v = B h = H TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < = TopSet ndx O ndx ˙ dist ndx D
165 simpr φ s = S r = R v = B h = H h = H
166 165 opeq2d φ s = S r = R v = B h = H Hom ndx h = Hom ndx H
167 88 sqxpeqd φ s = S r = R v = B h = H v × v = B × B
168 165 oveqd φ s = S r = R v = B h = H c h 2 nd a = c H 2 nd a
169 165 fveq1d φ s = S r = R v = B h = H h a = H a
170 40 fveq2d φ s = S r = R comp r x = comp R x
171 170 oveqd φ s = S r = R 1 st a x 2 nd a x comp r x c x = 1 st a x 2 nd a x comp R x c x
172 171 oveqd φ s = S r = R d x 1 st a x 2 nd a x comp r x c x e x = d x 1 st a x 2 nd a x comp R x c x e x
173 45 172 mpteq12dv φ s = S r = R x dom r d x 1 st a x 2 nd a x comp r x c x e x = x I d x 1 st a x 2 nd a x comp R x c x e x
174 173 ad2antrr φ s = S r = R v = B h = H x dom r d x 1 st a x 2 nd a x comp r x c x e x = x I d x 1 st a x 2 nd a x comp R x c x e x
175 168 169 174 mpoeq123dv φ s = S r = R v = B h = H d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = d c H 2 nd a , e H a x I d x 1 st a x 2 nd a x comp R x c x e x
176 167 88 175 mpoeq123dv φ s = S r = R v = B h = H a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = a B × B , c B d c H 2 nd a , e H a x I d x 1 st a x 2 nd a x comp R x c x e x
177 13 ad4antr φ s = S r = R v = B h = H ˙ = a B × B , c B d c H 2 nd a , e H a x I d x 1 st a x 2 nd a x comp R x c x e x
178 176 177 eqtr4d φ s = S r = R v = B h = H a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = ˙
179 178 opeq2d φ s = S r = R v = B h = H comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = comp ndx ˙
180 166 179 preq12d φ s = S r = R v = B h = H Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = Hom ndx H comp ndx ˙
181 164 180 uneq12d φ s = S r = R v = B h = H TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙
182 134 181 uneq12d φ s = S r = R v = B h = H Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙
183 76 87 182 csbied2 φ s = S r = R v = B f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙
184 38 48 183 csbied2 φ s = S r = R x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙
185 184 anasss φ s = S r = R x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d c h 2 nd a , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙
186 14 elexd φ S V
187 15 elexd φ R V
188 tpex Base ndx B + ndx + ˙ ndx × ˙ V
189 tpex Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ V
190 188 189 unex Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ V
191 tpex TopSet ndx O ndx ˙ dist ndx D V
192 prex Hom ndx H comp ndx ˙ V
193 191 192 unex TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙ V
194 190 193 unex Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙ V
195 194 a1i φ Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙ V
196 17 185 186 187 195 ovmpod φ S 𝑠 R = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙
197 1 196 syl5eq φ P = Base ndx B + ndx + ˙ ndx × ˙ Scalar ndx S ndx · ˙ 𝑖 ndx , ˙ TopSet ndx O ndx ˙ dist ndx D Hom ndx H comp ndx ˙