imastset

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

	Ref	Expression
Hypotheses	imasbas.u	$⊢ φ \to U = F “_{𝑠} R$
	imasbas.v	$⊢ φ \to V = {Base}_{R}$
	imasbas.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasbas.r	$⊢ φ \to R \in Z$
	imastset.j	$⊢ J = TopOpen (R)$
	imastset.o	$⊢ O = TopSet (U)$
Assertion	imastset	$⊢ φ \to O = J qTop F$

Proof

Step	Hyp	Ref	Expression
1		imasbas.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasbas.v	$⊢ φ \to V = {Base}_{R}$
3		imasbas.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
4		imasbas.r	$⊢ φ \to R \in Z$
5		imastset.j	$⊢ J = TopOpen (R)$
6		imastset.o	$⊢ O = TopSet (U)$
7		eqid	$⊢ +_{R} = +_{R}$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9		eqid	$⊢ Scalar (R) = Scalar (R)$
10		eqid	$⊢ {Base}_{Scalar (R)} = {Base}_{Scalar (R)}$
11		eqid	$⊢ \cdot_{R} = \cdot_{R}$
12		eqid	$⊢ \cdot_{𝑖} (R) = \cdot_{𝑖} (R)$
13		eqid	$⊢ dist (R) = dist (R)$
14		eqid	$⊢ \leq_{R} = \leq_{R}$
15		eqid	$⊢ +_{U} = +_{U}$
16	1 2 3 4 7 15	imasplusg	$⊢ φ \to +_{U} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p +_{R} q)⟩\}$
17		eqid	$⊢ \cdot_{U} = \cdot_{U}$
18	1 2 3 4 8 17	imasmulr	$⊢ φ \to \cdot_{U} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \cdot_{R} q)⟩\}$
19		eqid	$⊢ \cdot_{U} = \cdot_{U}$
20	1 2 3 4 9 10 11 19	imasvsca	$⊢ φ \to \cdot_{U} = ⋃_{q \in V} (p \in {Base}_{Scalar (R)}, x \in \{F (q)\} ⟼ F (p \cdot_{R} q))$
21		eqidd	$⊢ φ \to ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}$
22		eqidd	$⊢ φ \to J qTop F = J qTop F$
23		eqid	$⊢ dist (U) = dist (U)$
24	1 2 3 4 13 23	imasds	$⊢ φ \to dist (U) = (x \in B, y \in B ⟼ sup (⋃_{u \in ℕ} ran (z \in \{w \in ({(V \times V)}^{(1 \dots u)}) \| (F (1^{st} (w (1))) = x \land F (2^{nd} (w (u))) = y \land \forall v \in (1 \dots u - 1) F (2^{nd} (w (v))) = F (1^{st} (w (v + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (R) \circ z)) ℝ^{} <))$
25		eqidd	$⊢ φ \to (F \circ \leq_{R}) \circ F^{-1} = (F \circ \leq_{R}) \circ F^{-1}$
26	1 2 7 8 9 10 11 12 5 13 14 16 18 20 21 22 24 25 3 4	imasval	$⊢ φ \to U = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\}$
27	26	fveq2d	$⊢ φ \to TopSet (U) = TopSet ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\})$
28		ovex	$⊢ J qTop F \in V$
29		eqid	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\} = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\}$
30	29	imasvalstr	$⊢ ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\}) Struct ⟨1, 12⟩$
31		tsetid	$⊢ TopSet = Slot TopSet (ndx)$
32		snsstp1	$⊢ \{⟨TopSet (ndx), J qTop F⟩\} \subseteq \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\}$
33		ssun2	$⊢ \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\}$
34	32 33	sstri	$⊢ \{⟨TopSet (ndx), J qTop F⟩\} \subseteq (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\}$
35	30 31 34	strfv	$⊢ J qTop F \in V \to J qTop F = TopSet ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\})$
36	28 35	ax-mp	$⊢ J qTop F = TopSet ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, +_{U}⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩\} \cup \{⟨Scalar (ndx), Scalar (R)⟩, ⟨\cdot_{ndx}, \cdot_{U}⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \cdot_{𝑖} (R) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), J qTop F⟩, ⟨\leq_{ndx}, (F \circ \leq_{R}) \circ F^{-1}⟩, ⟨dist (ndx), dist (U)⟩\})$
37	27 6 36	3eqtr4g	$⊢ φ \to O = J qTop F$

Metamath Proof Explorer

Theorem imastset

Proof