imasval

Description: Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 11-Jul-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 6-Oct-2020)

	Ref	Expression
Hypotheses	imasval.u	$⊢ φ \to U = F “_{𝑠} R$
	imasval.v	$⊢ φ \to V = {Base}_{R}$
	imasval.p	$⊢ \underset{˙}{+} = +_{R}$
	imasval.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
	imasval.g	$⊢ G = Scalar (R)$
	imasval.k	$⊢ K = {Base}_{G}$
	imasval.q	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	imasval.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (R)$
	imasval.j	$⊢ J = TopOpen (R)$
	imasval.e	$⊢ E = dist (R)$
	imasval.n	$⊢ N = \leq_{R}$
	imasval.a	$⊢ φ \to \underset{˙}{✚} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{+} q)⟩\}$
	imasval.t	$⊢ φ \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\times} q)⟩\}$
	imasval.s	$⊢ φ \to \underset{˙}{\otimes} = ⋃_{q \in V} (p \in K, x \in \{F (q)\} ⟼ F (p \underset{˙}{\cdot} q))$
	imasval.w	$⊢ φ \to I = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \underset{˙}{,} q⟩\}$
	imasval.o	$⊢ φ \to O = J qTop F$
	imasval.d	$⊢ φ \to D = (x \in B, y \in B ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <))$
	imasval.l	$⊢ φ \to \underset{˙}{\leq} = (F \circ N) \circ F^{-1}$
	imasval.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasval.r	$⊢ φ \to R \in Z$
Assertion	imasval	$⊢ φ \to U = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) \cup \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$

Proof

Step	Hyp	Ref	Expression
1		imasval.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasval.v	$⊢ φ \to V = {Base}_{R}$
3		imasval.p	$⊢ \underset{˙}{+} = +_{R}$
4		imasval.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
5		imasval.g	$⊢ G = Scalar (R)$
6		imasval.k	$⊢ K = {Base}_{G}$
7		imasval.q	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		imasval.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (R)$
9		imasval.j	$⊢ J = TopOpen (R)$
10		imasval.e	$⊢ E = dist (R)$
11		imasval.n	$⊢ N = \leq_{R}$
12		imasval.a	$⊢ φ \to \underset{˙}{✚} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{+} q)⟩\}$
13		imasval.t	$⊢ φ \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\times} q)⟩\}$
14		imasval.s	$⊢ φ \to \underset{˙}{\otimes} = ⋃_{q \in V} (p \in K, x \in \{F (q)\} ⟼ F (p \underset{˙}{\cdot} q))$
15		imasval.w	$⊢ φ \to I = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \underset{˙}{,} q⟩\}$
16		imasval.o	$⊢ φ \to O = J qTop F$
17		imasval.d	$⊢ φ \to D = (x \in B, y \in B ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <))$
18		imasval.l	$⊢ φ \to \underset{˙}{\leq} = (F \circ N) \circ F^{-1}$
19		imasval.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
20		imasval.r	$⊢ φ \to R \in Z$
21		df-imas	$⊢ “_{𝑠} = (f \in V, r \in V ⟼ ⦋ {Base}_{r} / v ⦌ ((\{⟨{Base}_{ndx}, ran f⟩, ⟨+_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (r) qTop f⟩, ⟨\leq_{ndx}, (f \circ \leq_{r}) \circ f^{-1}⟩, ⟨dist (ndx), (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <))⟩\}))$
22	21	a1i	$⊢ φ \to “_{𝑠} = (f \in V, r \in V ⟼ ⦋ {Base}_{r} / v ⦌ ((\{⟨{Base}_{ndx}, ran f⟩, ⟨+_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (r) qTop f⟩, ⟨\leq_{ndx}, (f \circ \leq_{r}) \circ f^{-1}⟩, ⟨dist (ndx), (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <))⟩\}))$
23		fvexd	$⊢ (φ \land (f = F \land r = R)) \to {Base}_{r} \in V$
24		simplrl	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f = F$
25	24	rneqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ran f = ran F$
26		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
27	19 26	syl	$⊢ φ \to ran F = B$
28	27	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ran F = B$
29	25 28	eqtrd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ran f = B$
30	29	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨{Base}_{ndx}, ran f⟩ = ⟨{Base}_{ndx}, B⟩$
31		simplrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to r = R$
32	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to {Base}_{r} = {Base}_{R}$
33		simpr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to v = {Base}_{r}$
34	2	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to V = {Base}_{R}$
35	32 33 34	3eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to v = V$
36	24	fveq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (p) = F (p)$
37	24	fveq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (q) = F (q)$
38	36 37	opeq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨f (p), f (q)⟩ = ⟨F (p), F (q)⟩$
39	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to +_{r} = +_{R}$
40	39 3	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to +_{r} = \underset{˙}{+}$
41	40	oveqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to p +_{r} q = p \underset{˙}{+} q$
42	24 41	fveq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (p +_{r} q) = F (p \underset{˙}{+} q)$
43	38 42	opeq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩ = ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{+} q)⟩$
44	43	sneqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\} = \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{+} q)⟩\}$
45	35 44	iuneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\} = ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{+} q)⟩\}$
46	35 45	iuneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{+} q)⟩\}$
47	12	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \underset{˙}{✚} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{+} q)⟩\}$
48	46 47	eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\} = \underset{˙}{✚}$
49	48	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨+_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\}⟩ = ⟨+_{ndx}, \underset{˙}{✚}⟩$
50	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \cdot_{r} = \cdot_{R}$
51	50 4	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \cdot_{r} = \underset{˙}{\times}$
52	51	oveqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to p \cdot_{r} q = p \underset{˙}{\times} q$
53	24 52	fveq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (p \cdot_{r} q) = F (p \underset{˙}{\times} q)$
54	38 53	opeq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩ = ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\times} q)⟩$
55	54	sneqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\} = \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\times} q)⟩\}$
56	35 55	iuneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\} = ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\times} q)⟩\}$
57	35 56	iuneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\times} q)⟩\}$
58	13	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\times} q)⟩\}$
59	57 58	eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\} = \underset{˙}{∙}$
60	59	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨\cdot_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\}⟩ = ⟨\cdot_{ndx}, \underset{˙}{∙}⟩$
61	30 49 60	tpeq123d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{⟨{Base}_{ndx}, ran f⟩, ⟨+_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\}$
62	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to Scalar (r) = Scalar (R)$
63	62 5	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to Scalar (r) = G$
64	63	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨Scalar (ndx), Scalar (r)⟩ = ⟨Scalar (ndx), G⟩$
65	63	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to {Base}_{Scalar (r)} = {Base}_{G}$
66	65 6	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to {Base}_{Scalar (r)} = K$
67	37	sneqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{f (q)\} = \{F (q)\}$
68	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \cdot_{r} = \cdot_{R}$
69	68 7	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \cdot_{r} = \underset{˙}{\cdot}$
70	69	oveqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to p \cdot_{r} q = p \underset{˙}{\cdot} q$
71	24 70	fveq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (p \cdot_{r} q) = F (p \underset{˙}{\cdot} q)$
72	66 67 71	mpoeq123dv	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q)) = (p \in K, x \in \{F (q)\} ⟼ F (p \underset{˙}{\cdot} q))$
73	72	iuneq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{q \in V} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q)) = ⋃_{q \in V} (p \in K, x \in \{F (q)\} ⟼ F (p \underset{˙}{\cdot} q))$
74	35	iuneq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q)) = ⋃_{q \in V} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))$
75	14	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \underset{˙}{\otimes} = ⋃_{q \in V} (p \in K, x \in \{F (q)\} ⟼ F (p \underset{˙}{\cdot} q))$
76	73 74 75	3eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q)) = \underset{˙}{\otimes}$
77	76	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨\cdot_{ndx}, ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))⟩ = ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩$
78	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \cdot_{𝑖} (r) = \cdot_{𝑖} (R)$
79	78 8	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \cdot_{𝑖} (r) = \underset{˙}{,}$
80	79	oveqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to p \cdot_{𝑖} (r) q = p \underset{˙}{,} q$
81	38 80	opeq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩ = ⟨⟨F (p), F (q)⟩, p \underset{˙}{,} q⟩$
82	81	sneqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\} = \{⟨⟨F (p), F (q)⟩, p \underset{˙}{,} q⟩\}$
83	35 82	iuneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\} = ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \underset{˙}{,} q⟩\}$
84	35 83	iuneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \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 \underset{˙}{,} q⟩\}$
85	15	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to I = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, p \underset{˙}{,} q⟩\}$
86	84 85	eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\} = I$
87	86	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨\cdot_{𝑖} (ndx), ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\}⟩ = ⟨\cdot_{𝑖} (ndx), I⟩$
88	64 77 87	tpeq123d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\}⟩\} = \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}$
89	61 88	uneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{⟨{Base}_{ndx}, ran f⟩, ⟨+_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}$
90	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to TopOpen (r) = TopOpen (R)$
91	90 9	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to TopOpen (r) = J$
92	91 24	oveq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to TopOpen (r) qTop f = J qTop F$
93	16	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to O = J qTop F$
94	92 93	eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to TopOpen (r) qTop f = O$
95	94	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨TopSet (ndx), TopOpen (r) qTop f⟩ = ⟨TopSet (ndx), O⟩$
96	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \leq_{r} = \leq_{R}$
97	96 11	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \leq_{r} = N$
98	24 97	coeq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f \circ \leq_{r} = F \circ N$
99	24	cnveqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f^{-1} = F^{-1}$
100	98 99	coeq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (f \circ \leq_{r}) \circ f^{-1} = (F \circ N) \circ F^{-1}$
101	18	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \underset{˙}{\leq} = (F \circ N) \circ F^{-1}$
102	100 101	eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (f \circ \leq_{r}) \circ f^{-1} = \underset{˙}{\leq}$
103	102	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨\leq_{ndx}, (f \circ \leq_{r}) \circ f^{-1}⟩ = ⟨\leq_{ndx}, \underset{˙}{\leq}⟩$
104	35	sqxpeqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to v \times v = V \times V$
105	104	oveq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to {(v \times v)}^{(1 \dots n)} = {(V \times V)}^{(1 \dots n)}$
106	24	fveq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (1^{st} (h (1))) = F (1^{st} (h (1)))$
107	106	eqeq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (f (1^{st} (h (1))) = x \leftrightarrow F (1^{st} (h (1))) = x)$
108	24	fveq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (2^{nd} (h (n))) = F (2^{nd} (h (n)))$
109	108	eqeq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (f (2^{nd} (h (n))) = y \leftrightarrow F (2^{nd} (h (n))) = y)$
110	24	fveq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (2^{nd} (h (i))) = F (2^{nd} (h (i)))$
111	24	fveq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to f (1^{st} (h (i + 1))) = F (1^{st} (h (i + 1)))$
112	110 111	eqeq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))) \leftrightarrow F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))$
113	112	ralbidv	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (\forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))) \leftrightarrow \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))$
114	107 109 113	3anbi123d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ((f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1)))) \leftrightarrow (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1)))))$
115	105 114	rabeqbidv	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} = \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\}$
116	31	fveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to dist (r) = dist (R)$
117	116 10	syl6eqr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to dist (r) = E$
118	117	coeq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to dist (r) \circ g = E \circ g$
119	118	oveq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g) = \sum_{ℝ_{𝑠}^{}} (E \circ g)$
120	115 119	mpteq12dv	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) = (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
121	120	rneqd	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) = ran (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
122	121	iuneq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) = ⋃_{n \in ℕ} ran (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g))$
123	122	infeq1d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <) = sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <)$
124	29 29 123	mpoeq123dv	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <)) = (x \in B, y \in B ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <))$
125	17	ad2antrr	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to D = (x \in B, y \in B ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(V \times V)}^{(1 \dots n)}) \| (F (1^{st} (h (1))) = x \land F (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) F (2^{nd} (h (i))) = F (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (E \circ g)) ℝ^{} <))$
126	124 125	eqtr4d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <)) = D$
127	126	opeq2d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to ⟨dist (ndx), (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <))⟩ = ⟨dist (ndx), D⟩$
128	95 103 127	tpeq123d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to \{⟨TopSet (ndx), TopOpen (r) qTop f⟩, ⟨\leq_{ndx}, (f \circ \leq_{r}) \circ f^{-1}⟩, ⟨dist (ndx), (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <))⟩\} = \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
129	89 128	uneq12d	$⊢ ((φ \land (f = F \land r = R)) \land v = {Base}_{r}) \to (\{⟨{Base}_{ndx}, ran f⟩, ⟨+_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (r) qTop f⟩, ⟨\leq_{ndx}, (f \circ \leq_{r}) \circ f^{-1}⟩, ⟨dist (ndx), (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <))⟩\} = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) \cup \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
130	23 129	csbied	$⊢ (φ \land (f = F \land r = R)) \to ⦋ {Base}_{r} / v ⦌ ((\{⟨{Base}_{ndx}, ran f⟩, ⟨+_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p +_{r} q)⟩\}⟩, ⟨\cdot_{ndx}, ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, f (p \cdot_{r} q)⟩\}⟩\} \cup \{⟨Scalar (ndx), Scalar (r)⟩, ⟨\cdot_{ndx}, ⋃_{q \in v} (p \in {Base}_{Scalar (r)}, x \in \{f (q)\} ⟼ f (p \cdot_{r} q))⟩, ⟨\cdot_{𝑖} (ndx), ⋃_{p \in v} ⋃_{q \in v} \{⟨⟨f (p), f (q)⟩, p \cdot_{𝑖} (r) q⟩\}⟩\}) \cup \{⟨TopSet (ndx), TopOpen (r) qTop f⟩, ⟨\leq_{ndx}, (f \circ \leq_{r}) \circ f^{-1}⟩, ⟨dist (ndx), (x \in ran f, y \in ran f ⟼ sup (⋃_{n \in ℕ} ran (g \in \{h \in ({(v \times v)}^{(1 \dots n)}) \| (f (1^{st} (h (1))) = x \land f (2^{nd} (h (n))) = y \land \forall i \in (1 \dots n - 1) f (2^{nd} (h (i))) = f (1^{st} (h (i + 1))))\} ⟼ \sum_{ℝ_{𝑠}^{}} (dist (r) \circ g)) ℝ^{} <))⟩\}) = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) \cup \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
131		fof	$⊢ F : V \underset{onto}{⟶} B \to F : V ⟶ B$
132	19 131	syl	$⊢ φ \to F : V ⟶ B$
133		fvex	$⊢ {Base}_{R} \in V$
134	2 133	eqeltrdi	$⊢ φ \to V \in V$
135		fex	$⊢ (F : V ⟶ B \land V \in V) \to F \in V$
136	132 134 135	syl2anc	$⊢ φ \to F \in V$
137	20	elexd	$⊢ φ \to R \in V$
138		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \in V$
139		tpex	$⊢ \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\} \in V$
140	138 139	unex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\} \in V$
141		tpex	$⊢ \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \in V$
142	140 141	unex	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) \cup \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \in V$
143	142	a1i	$⊢ φ \to (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) \cup \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} \in V$
144	22 130 136 137 143	ovmpod	$⊢ φ \to F “_{𝑠} R = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) \cup \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
145	1 144	eqtrd	$⊢ φ \to U = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{✚}⟩, ⟨\cdot_{ndx}, \underset{˙}{∙}⟩\} \cup \{⟨Scalar (ndx), G⟩, ⟨\cdot_{ndx}, \underset{˙}{\otimes}⟩, ⟨\cdot_{𝑖} (ndx), I⟩\}) \cup \{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$

Metamath Proof Explorer

Theorem imasval

Proof