Description: The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | imasbas.u | |
|
imasbas.v | |
||
imasbas.f | |
||
imasbas.r | |
||
imasip.i | |
||
imasip.w | |
||
Assertion | imasip | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imasbas.u | |
|
2 | imasbas.v | |
|
3 | imasbas.f | |
|
4 | imasbas.r | |
|
5 | imasip.i | |
|
6 | imasip.w | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 1 2 3 4 7 15 | imasplusg | |
17 | eqid | |
|
18 | 1 2 3 4 8 17 | imasmulr | |
19 | eqid | |
|
20 | 1 2 3 4 9 10 11 19 | imasvsca | |
21 | eqidd | |
|
22 | eqidd | |
|
23 | eqid | |
|
24 | 1 2 3 4 13 23 | imasds | |
25 | eqidd | |
|
26 | 1 2 7 8 9 10 11 5 12 13 14 16 18 20 21 22 24 25 3 4 | imasval | |
27 | eqid | |
|
28 | 27 | imasvalstr | |
29 | ipid | |
|
30 | snsstp3 | |
|
31 | ssun2 | |
|
32 | 30 31 | sstri | |
33 | ssun1 | |
|
34 | 32 33 | sstri | |
35 | fvex | |
|
36 | 2 35 | eqeltrdi | |
37 | snex | |
|
38 | 37 | rgenw | |
39 | iunexg | |
|
40 | 36 38 39 | sylancl | |
41 | 40 | ralrimivw | |
42 | iunexg | |
|
43 | 36 41 42 | syl2anc | |
44 | 26 28 29 34 43 6 | strfv3 | |