Metamath Proof Explorer


Theorem imasip

Description: The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses imasbas.u φU=F𝑠R
imasbas.v φV=BaseR
imasbas.f φF:VontoB
imasbas.r φRZ
imasip.i ,˙=𝑖R
imasip.w I=𝑖U
Assertion imasip φI=pVqVFpFqp,˙q

Proof

Step Hyp Ref Expression
1 imasbas.u φU=F𝑠R
2 imasbas.v φV=BaseR
3 imasbas.f φF:VontoB
4 imasbas.r φRZ
5 imasip.i ,˙=𝑖R
6 imasip.w I=𝑖U
7 eqid +R=+R
8 eqid R=R
9 eqid ScalarR=ScalarR
10 eqid BaseScalarR=BaseScalarR
11 eqid R=R
12 eqid TopOpenR=TopOpenR
13 eqid distR=distR
14 eqid R=R
15 eqid +U=+U
16 1 2 3 4 7 15 imasplusg φ+U=pVqVFpFqFp+Rq
17 eqid U=U
18 1 2 3 4 8 17 imasmulr φU=pVqVFpFqFpRq
19 eqid U=U
20 1 2 3 4 9 10 11 19 imasvsca φU=qVpBaseScalarR,xFqFpRq
21 eqidd φpVqVFpFqp,˙q=pVqVFpFqp,˙q
22 eqidd φTopOpenRqTopF=TopOpenRqTopF
23 eqid distU=distU
24 1 2 3 4 13 23 imasds φdistU=xB,yBsupuranzwV×V1u|F1stw1=xF2ndwu=yv1u1F2ndwv=F1stwv+1𝑠*distRz*<
25 eqidd φFRF-1=FRF-1
26 1 2 7 8 9 10 11 5 12 13 14 16 18 20 21 22 24 25 3 4 imasval φU=BasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qTopSetndxTopOpenRqTopFndxFRF-1distndxdistU
27 eqid BasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qTopSetndxTopOpenRqTopFndxFRF-1distndxdistU=BasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qTopSetndxTopOpenRqTopFndxFRF-1distndxdistU
28 27 imasvalstr BasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qTopSetndxTopOpenRqTopFndxFRF-1distndxdistUStruct112
29 ipid 𝑖=Slot𝑖ndx
30 snsstp3 𝑖ndxpVqVFpFqp,˙qScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙q
31 ssun2 ScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qBasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙q
32 30 31 sstri 𝑖ndxpVqVFpFqp,˙qBasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙q
33 ssun1 BasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qBasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qTopSetndxTopOpenRqTopFndxFRF-1distndxdistU
34 32 33 sstri 𝑖ndxpVqVFpFqp,˙qBasendxB+ndx+UndxUScalarndxScalarRndxU𝑖ndxpVqVFpFqp,˙qTopSetndxTopOpenRqTopFndxFRF-1distndxdistU
35 fvex BaseRV
36 2 35 eqeltrdi φVV
37 snex FpFqp,˙qV
38 37 rgenw qVFpFqp,˙qV
39 iunexg VVqVFpFqp,˙qVqVFpFqp,˙qV
40 36 38 39 sylancl φqVFpFqp,˙qV
41 40 ralrimivw φpVqVFpFqp,˙qV
42 iunexg VVpVqVFpFqp,˙qVpVqVFpFqp,˙qV
43 36 41 42 syl2anc φpVqVFpFqp,˙qV
44 26 28 29 34 43 6 strfv3 φI=pVqVFpFqp,˙q