isnvlem

Description: Lemma for isnv . (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isnvlem.1	$⊢ X = ran G$
	isnvlem.2	$⊢ Z = GId (G)$
Assertion	isnvlem	$⊢ (G \in V \land S \in V \land N \in V) \to (⟨⟨G, S⟩, N⟩ \in NrmCVec \leftrightarrow (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y))))$

Proof

Step	Hyp	Ref	Expression
1		isnvlem.1	$⊢ X = ran G$
2		isnvlem.2	$⊢ Z = GId (G)$
3		df-nv	$⊢ NrmCVec = \{⟨⟨g, s⟩, n⟩ \| (⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)))\}$
4	3	eleq2i	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \leftrightarrow ⟨⟨G, S⟩, N⟩ \in \{⟨⟨g, s⟩, n⟩ \| (⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)))\}$
5		opeq1	$⊢ g = G \to ⟨g, s⟩ = ⟨G, s⟩$
6	5	eleq1d	$⊢ g = G \to (⟨g, s⟩ \in {CVec}_{OLD} \leftrightarrow ⟨G, s⟩ \in {CVec}_{OLD})$
7		rneq	$⊢ g = G \to ran g = ran G$
8	7 1	syl6eqr	$⊢ g = G \to ran g = X$
9	8	feq2d	$⊢ g = G \to (n : ran g ⟶ ℝ \leftrightarrow n : X ⟶ ℝ)$
10		fveq2	$⊢ g = G \to GId (g) = GId (G)$
11	10 2	syl6eqr	$⊢ g = G \to GId (g) = Z$
12	11	eqeq2d	$⊢ g = G \to (x = GId (g) \leftrightarrow x = Z)$
13	12	imbi2d	$⊢ g = G \to ((n (x) = 0 \to x = GId (g)) \leftrightarrow (n (x) = 0 \to x = Z))$
14		oveq	$⊢ g = G \to x g y = x G y$
15	14	fveq2d	$⊢ g = G \to n (x g y) = n (x G y)$
16	15	breq1d	$⊢ g = G \to (n (x g y) \leq n (x) + n (y) \leftrightarrow n (x G y) \leq n (x) + n (y))$
17	8 16	raleqbidv	$⊢ g = G \to (\forall y \in ran g n (x g y) \leq n (x) + n (y) \leftrightarrow \forall y \in X n (x G y) \leq n (x) + n (y))$
18	13 17	3anbi13d	$⊢ g = G \to (((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)) \leftrightarrow ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)))$
19	8 18	raleqbidv	$⊢ g = G \to (\forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)) \leftrightarrow \forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)))$
20	6 9 19	3anbi123d	$⊢ g = G \to ((⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y))) \leftrightarrow (⟨G, s⟩ \in {CVec}_{OLD} \land n : X ⟶ ℝ \land \forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y))))$
21		opeq2	$⊢ s = S \to ⟨G, s⟩ = ⟨G, S⟩$
22	21	eleq1d	$⊢ s = S \to (⟨G, s⟩ \in {CVec}_{OLD} \leftrightarrow ⟨G, S⟩ \in {CVec}_{OLD})$
23		oveq	$⊢ s = S \to y s x = y S x$
24	23	fveqeq2d	$⊢ s = S \to (n (y s x) = \|y\| n (x) \leftrightarrow n (y S x) = \|y\| n (x))$
25	24	ralbidv	$⊢ s = S \to (\forall y \in ℂ n (y s x) = \|y\| n (x) \leftrightarrow \forall y \in ℂ n (y S x) = \|y\| n (x))$
26	25	3anbi2d	$⊢ s = S \to (((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)) \leftrightarrow ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y S x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)))$
27	26	ralbidv	$⊢ s = S \to (\forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)) \leftrightarrow \forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y S x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)))$
28	22 27	3anbi13d	$⊢ s = S \to ((⟨G, s⟩ \in {CVec}_{OLD} \land n : X ⟶ ℝ \land \forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y))) \leftrightarrow (⟨G, S⟩ \in {CVec}_{OLD} \land n : X ⟶ ℝ \land \forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y S x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y))))$
29		feq1	$⊢ n = N \to (n : X ⟶ ℝ \leftrightarrow N : X ⟶ ℝ)$
30		fveq1	$⊢ n = N \to n (x) = N (x)$
31	30	eqeq1d	$⊢ n = N \to (n (x) = 0 \leftrightarrow N (x) = 0)$
32	31	imbi1d	$⊢ n = N \to ((n (x) = 0 \to x = Z) \leftrightarrow (N (x) = 0 \to x = Z))$
33		fveq1	$⊢ n = N \to n (y S x) = N (y S x)$
34	30	oveq2d	$⊢ n = N \to \|y\| n (x) = \|y\| N (x)$
35	33 34	eqeq12d	$⊢ n = N \to (n (y S x) = \|y\| n (x) \leftrightarrow N (y S x) = \|y\| N (x))$
36	35	ralbidv	$⊢ n = N \to (\forall y \in ℂ n (y S x) = \|y\| n (x) \leftrightarrow \forall y \in ℂ N (y S x) = \|y\| N (x))$
37		fveq1	$⊢ n = N \to n (x G y) = N (x G y)$
38		fveq1	$⊢ n = N \to n (y) = N (y)$
39	30 38	oveq12d	$⊢ n = N \to n (x) + n (y) = N (x) + N (y)$
40	37 39	breq12d	$⊢ n = N \to (n (x G y) \leq n (x) + n (y) \leftrightarrow N (x G y) \leq N (x) + N (y))$
41	40	ralbidv	$⊢ n = N \to (\forall y \in X n (x G y) \leq n (x) + n (y) \leftrightarrow \forall y \in X N (x G y) \leq N (x) + N (y))$
42	32 36 41	3anbi123d	$⊢ n = N \to (((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y S x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)) \leftrightarrow ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$
43	42	ralbidv	$⊢ n = N \to (\forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y S x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y)) \leftrightarrow \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y)))$
44	29 43	3anbi23d	$⊢ n = N \to ((⟨G, S⟩ \in {CVec}_{OLD} \land n : X ⟶ ℝ \land \forall x \in X ((n (x) = 0 \to x = Z) \land \forall y \in ℂ n (y S x) = \|y\| n (x) \land \forall y \in X n (x G y) \leq n (x) + n (y))) \leftrightarrow (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y))))$
45	20 28 44	eloprabg	$⊢ (G \in V \land S \in V \land N \in V) \to (⟨⟨G, S⟩, N⟩ \in \{⟨⟨g, s⟩, n⟩ \| (⟨g, s⟩ \in {CVec}_{OLD} \land n : ran g ⟶ ℝ \land \forall x \in ran g ((n (x) = 0 \to x = GId (g)) \land \forall y \in ℂ n (y s x) = \|y\| n (x) \land \forall y \in ran g n (x g y) \leq n (x) + n (y)))\} \leftrightarrow (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y))))$
46	4 45	syl5bb	$⊢ (G \in V \land S \in V \land N \in V) \to (⟨⟨G, S⟩, N⟩ \in NrmCVec \leftrightarrow (⟨G, S⟩ \in {CVec}_{OLD} \land N : X ⟶ ℝ \land \forall x \in X ((N (x) = 0 \to x = Z) \land \forall y \in ℂ N (y S x) = \|y\| N (x) \land \forall y \in X N (x G y) \leq N (x) + N (y))))$

Metamath Proof Explorer

Theorem isnvlem

Proof