tngval

Description: Value of the function which augments a given structure G with a norm N . (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	tngval.t	$⊢ T = G toNrmGrp N$
	tngval.m	$⊢ \underset{˙}{-} = -_{G}$
	tngval.d	$⊢ D = N \circ \underset{˙}{-}$
	tngval.j	$⊢ J = MetOpen (D)$
Assertion	tngval	$⊢ (G \in V \land N \in W) \to T = (G sSet ⟨dist (ndx), D⟩) sSet ⟨TopSet (ndx), J⟩$

Proof

Step	Hyp	Ref	Expression
1		tngval.t	$⊢ T = G toNrmGrp N$
2		tngval.m	$⊢ \underset{˙}{-} = -_{G}$
3		tngval.d	$⊢ D = N \circ \underset{˙}{-}$
4		tngval.j	$⊢ J = MetOpen (D)$
5		elex	$⊢ G \in V \to G \in V$
6		elex	$⊢ N \in W \to N \in V$
7		simpl	$⊢ (g = G \land f = N) \to g = G$
8		simpr	$⊢ (g = G \land f = N) \to f = N$
9	7	fveq2d	$⊢ (g = G \land f = N) \to -_{g} = -_{G}$
10	9 2	eqtr4di	$⊢ (g = G \land f = N) \to -_{g} = \underset{˙}{-}$
11	8 10	coeq12d	$⊢ (g = G \land f = N) \to f \circ -_{g} = N \circ \underset{˙}{-}$
12	11 3	eqtr4di	$⊢ (g = G \land f = N) \to f \circ -_{g} = D$
13	12	opeq2d	$⊢ (g = G \land f = N) \to ⟨dist (ndx), f \circ -_{g}⟩ = ⟨dist (ndx), D⟩$
14	7 13	oveq12d	$⊢ (g = G \land f = N) \to g sSet ⟨dist (ndx), f \circ -_{g}⟩ = G sSet ⟨dist (ndx), D⟩$
15	12	fveq2d	$⊢ (g = G \land f = N) \to MetOpen (f \circ -_{g}) = MetOpen (D)$
16	15 4	eqtr4di	$⊢ (g = G \land f = N) \to MetOpen (f \circ -_{g}) = J$
17	16	opeq2d	$⊢ (g = G \land f = N) \to ⟨TopSet (ndx), MetOpen (f \circ -_{g})⟩ = ⟨TopSet (ndx), J⟩$
18	14 17	oveq12d	$⊢ (g = G \land f = N) \to (g sSet ⟨dist (ndx), f \circ -_{g}⟩) sSet ⟨TopSet (ndx), MetOpen (f \circ -_{g})⟩ = (G sSet ⟨dist (ndx), D⟩) sSet ⟨TopSet (ndx), J⟩$
19		df-tng	$⊢ toNrmGrp = (g \in V, f \in V ⟼ (g sSet ⟨dist (ndx), f \circ -_{g}⟩) sSet ⟨TopSet (ndx), MetOpen (f \circ -_{g})⟩)$
20		ovex	$⊢ (G sSet ⟨dist (ndx), D⟩) sSet ⟨TopSet (ndx), J⟩ \in V$
21	18 19 20	ovmpoa	$⊢ (G \in V \land N \in V) \to G toNrmGrp N = (G sSet ⟨dist (ndx), D⟩) sSet ⟨TopSet (ndx), J⟩$
22	5 6 21	syl2an	$⊢ (G \in V \land N \in W) \to G toNrmGrp N = (G sSet ⟨dist (ndx), D⟩) sSet ⟨TopSet (ndx), J⟩$
23	1 22	eqtrid	$⊢ (G \in V \land N \in W) \to T = (G sSet ⟨dist (ndx), D⟩) sSet ⟨TopSet (ndx), J⟩$

Metamath Proof Explorer

Theorem tngval

Proof