Theorem imasle

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

	Ref	Expression
Hypotheses	imasbas.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasbas.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasbas.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imasbas.r	$$⊢\phi \to R\in Z$$
	imasle.n	$$⊢N={\le }_R$$
	imasle.l	$$⊢\underset{\dot{}}{\le }={\le }_U$$
Assertion	imasle	$$⊢\phi \to \underset{\dot{}}{\le }=\left(F\circ N\right)\circ F^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		imasbas.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
2		imasbas.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		imasbas.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
4		imasbas.r	$$⊢\phi \to R\in Z$$
5		imasle.n	$$⊢N={\le }_R$$
6		imasle.l	$$⊢\underset{\dot{}}{\le }={\le }_U$$
7		eqid	$$⊢{+}_R={+}_R$$
8		eqid	$$⊢{\cdot }_R={\cdot }_R$$
9		eqid	$$⊢\mathrm{Scalar}\left(R\right)=\mathrm{Scalar}\left(R\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)}$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12		eqid	$$⊢{\cdot }_{𝑖}\left(R\right)={\cdot }_{𝑖}\left(R\right)$$
13		eqid	$$⊢\mathrm{TopOpen}\left(R\right)=\mathrm{TopOpen}\left(R\right)$$
14		eqid	$$⊢\mathrm{dist}\left(R\right)=\mathrm{dist}\left(R\right)$$
15		eqid	$$⊢{+}_U={+}_U$$
16	1 2 3 4 7 15	imasplusg	$$⊢\phi \to {+}_U=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{+}_{R}q\right)⟩\right\}$$
17		eqid	$$⊢{\cdot }_U={\cdot }_U$$
18	1 2 3 4 8 17	imasmulr	$$⊢\phi \to {\cdot }_U=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p{\cdot }_{R}q\right)⟩\right\}$$
19		eqid	$$⊢{\cdot }_U={\cdot }_U$$
20	1 2 3 4 9 10 11 19	imasvsca	$$⊢\phi \to {\cdot }_U=\bigcup _{q\in V}\left(p\in {\mathrm{Base}}_{\mathrm{Scalar}\left(R\right)},x\in \left\{F\left(q\right)\right\}⟼F\left(p{\cdot }_{R}q\right)\right)$$
21		eqidd	$$⊢\phi \to \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}$$
22		eqid	$$⊢\mathrm{TopSet}\left(U\right)=\mathrm{TopSet}\left(U\right)$$
23	1 2 3 4 13 22	imastset	$$⊢\phi \to \mathrm{TopSet}\left(U\right)=\mathrm{TopOpen}\left(R\right)\mathrm{qTop}F$$
24		eqid	$$⊢\mathrm{dist}\left(U\right)=\mathrm{dist}\left(U\right)$$
25	1 2 3 4 14 24	imasds	$$⊢\phi \to \mathrm{dist}\left(U\right)=\left(x\in B,y\in B⟼sup\left(\bigcup _{u\in \mathbb{N}}\mathrm{ran}\left(z\in \left\{w\in \left({\left(V\times V\right)}^{\left(1\dots u\right)}\right)|\left(F\left(1^{st}\left(w\left(1\right)\right)\right)=x\wedge F\left(2^{nd}\left(w\left(u\right)\right)\right)=y\wedge \forall v\in \left(1\dots u-1\right)F\left(2^{nd}\left(w\left(v\right)\right)\right)=F\left(1^{st}\left(w\left(v+1\right)\right)\right)\right)\right\}⟼{\sum }_{{ℝ}_{𝑠}^{*}}\left(\mathrm{dist}\left(R\right)\circ z\right)\right),{ℝ}^{*},<\right)\right)$$
26		eqidd	$$⊢\phi \to \left(F\circ N\right)\circ F^{-1}=\left(F\circ N\right)\circ F^{-1}$$
27	1 2 7 8 9 10 11 12 13 14 5 16 18 20 21 23 25 26 3 4	imasval	$$⊢\phi \to U=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{+}_U⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}$$
28		eqid	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{+}_U⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{+}_U⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}$$
29	28	imasvalstr	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{+}_U⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}\right)\mathrm{Struct}⟨1,12⟩$$
30		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
31		snsstp2	$$⊢\left\{⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩\right\}\subseteq \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}$$
32		ssun2	$$⊢\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{+}_U⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}$$
33	31 32	sstri	$$⊢\left\{⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{+}_U⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{Scalar}\left(R\right)⟩,⟨{\cdot }_{\mathrm{ndx}},{\cdot }_U⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,p{\cdot }_{𝑖}\left(R\right)q⟩\right\}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{TopSet}\left(U\right)⟩,⟨{\le }_{\mathrm{ndx}},\left(F\circ N\right)\circ F^{-1}⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{dist}\left(U\right)⟩\right\}$$
34		fof	$$⊢F:V\underset{onto}{⟶}B\to F:V⟶B$$
35	3 34	syl	$$⊢\phi \to F:V⟶B$$
36		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
37	2 36	eqeltrdi	$$⊢\phi \to V\in \mathrm{V}$$
38	35 37	fexd	$$⊢\phi \to F\in \mathrm{V}$$
39	5	fvexi	$$⊢N\in \mathrm{V}$$
40		coexg	$$⊢\left(F\in \mathrm{V}\wedge N\in \mathrm{V}\right)\to F\circ N\in \mathrm{V}$$
41	38 39 40	sylancl	$$⊢\phi \to F\circ N\in \mathrm{V}$$
42		cnvexg	$$⊢F\in \mathrm{V}\to F^{-1}\in \mathrm{V}$$
43	38 42	syl	$$⊢\phi \to F^{-1}\in \mathrm{V}$$
44		coexg	$$⊢\left(F\circ N\in \mathrm{V}\wedge F^{-1}\in \mathrm{V}\right)\to \left(F\circ N\right)\circ F^{-1}\in \mathrm{V}$$
45	41 43 44	syl2anc	$$⊢\phi \to \left(F\circ N\right)\circ F^{-1}\in \mathrm{V}$$
46	27 29 30 33 45 6	strfv3	$$⊢\phi \to \underset{\dot{}}{\le }=\left(F\circ N\right)\circ F^{-1}$$