Metamath Proof Explorer


Theorem imasle

Description: The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses imasbas.u φ U = F 𝑠 R
imasbas.v φ V = Base R
imasbas.f φ F : V onto B
imasbas.r φ R Z
imasle.n N = R
imasle.l ˙ = U
Assertion imasle φ ˙ = F N F -1

Proof

Step Hyp Ref Expression
1 imasbas.u φ U = F 𝑠 R
2 imasbas.v φ V = Base R
3 imasbas.f φ F : V onto B
4 imasbas.r φ R Z
5 imasle.n N = R
6 imasle.l ˙ = U
7 eqid + R = + R
8 eqid R = R
9 eqid Scalar R = Scalar R
10 eqid Base Scalar R = Base Scalar R
11 eqid R = R
12 eqid 𝑖 R = 𝑖 R
13 eqid TopOpen R = TopOpen R
14 eqid dist R = dist R
15 eqid + U = + U
16 1 2 3 4 7 15 imasplusg φ + U = p V q V F p F q F p + R q
17 eqid U = U
18 1 2 3 4 8 17 imasmulr φ U = p V q V F p F q F p R q
19 eqid U = U
20 1 2 3 4 9 10 11 19 imasvsca φ U = q V p Base Scalar R , x F q F p R q
21 eqidd φ p V q V F p F q p 𝑖 R q = p V q V F p F q p 𝑖 R q
22 eqid TopSet U = TopSet U
23 1 2 3 4 13 22 imastset φ TopSet U = TopOpen R qTop F
24 eqid dist U = dist U
25 1 2 3 4 14 24 imasds φ dist U = x B , y B sup u ran z w V × V 1 u | F 1 st w 1 = x F 2 nd w u = y v 1 u 1 F 2 nd w v = F 1 st w v + 1 𝑠 * dist R z * <
26 eqidd φ F N F -1 = F N F -1
27 1 2 7 8 9 10 11 12 13 14 5 16 18 20 21 23 25 26 3 4 imasval φ U = Base ndx B + ndx + U ndx U Scalar ndx Scalar R ndx U 𝑖 ndx p V q V F p F q p 𝑖 R q TopSet ndx TopSet U ndx F N F -1 dist ndx dist U
28 eqid Base ndx B + ndx + U ndx U Scalar ndx Scalar R ndx U 𝑖 ndx p V q V F p F q p 𝑖 R q TopSet ndx TopSet U ndx F N F -1 dist ndx dist U = Base ndx B + ndx + U ndx U Scalar ndx Scalar R ndx U 𝑖 ndx p V q V F p F q p 𝑖 R q TopSet ndx TopSet U ndx F N F -1 dist ndx dist U
29 28 imasvalstr Base ndx B + ndx + U ndx U Scalar ndx Scalar R ndx U 𝑖 ndx p V q V F p F q p 𝑖 R q TopSet ndx TopSet U ndx F N F -1 dist ndx dist U Struct 1 12
30 pleid le = Slot ndx
31 snsstp2 ndx F N F -1 TopSet ndx TopSet U ndx F N F -1 dist ndx dist U
32 ssun2 TopSet ndx TopSet U ndx F N F -1 dist ndx dist U Base ndx B + ndx + U ndx U Scalar ndx Scalar R ndx U 𝑖 ndx p V q V F p F q p 𝑖 R q TopSet ndx TopSet U ndx F N F -1 dist ndx dist U
33 31 32 sstri ndx F N F -1 Base ndx B + ndx + U ndx U Scalar ndx Scalar R ndx U 𝑖 ndx p V q V F p F q p 𝑖 R q TopSet ndx TopSet U ndx F N F -1 dist ndx dist U
34 fof F : V onto B F : V B
35 3 34 syl φ F : V B
36 fvex Base R V
37 2 36 eqeltrdi φ V V
38 35 37 fexd φ F V
39 5 fvexi N V
40 coexg F V N V F N V
41 38 39 40 sylancl φ F N V
42 cnvexg F V F -1 V
43 38 42 syl φ F -1 V
44 coexg F N V F -1 V F N F -1 V
45 41 43 44 syl2anc φ F N F -1 V
46 27 29 30 33 45 6 strfv3 φ ˙ = F N F -1