Theorem isnvlem 8229

Description: Lemma for isnv 8231.

Hypotheses

Ref	Expression
isnvlem.1	|- X = ran G
isnvlem.2	|- Z = (Id` G)

Assertion

Ref	Expression
isnvlem	|- ((G e. V /\ S e. V /\ N e. V) -> (<.<.G, S>., N>. e. NrmCVec <-> (<.G, S>. e. CVec /\ N:X-->RR /\ A.x e. X (((N` x) = 0 -> x = Z) /\ A.y e. CC (N` (ySx)) = ((abs` y) x. (N` x)) /\ A.y e. X (N` (xGy)) <_ ((N` x) + (N` y))))))

Distinct variable groups:   x,y,G   x,N,y   x,S,y   x,X,y

Proof of Theorem isnvlem

Step	Hyp	Ref	Expression
1		opeq1 2487	. . . . 5 |- (g = G -> <.g, s>. = <.G, s>.)
2	1	eleq1d 1540	. . . 4 |- (g = G -> (<.g, s>. e. CVec <-> <.G, s>. e. CVec))
3		rneq 3339	. . . . . 6 |- (g = G -> ran g = ran G)
4		isnvlem.1	. . . . . 6 |- X = ran G
5	3, 4	syl6eqr 1525	. . . . 5 |- (g = G -> ran g = X)
6		feq2 3621	. . . . 5 |- (ran g = X -> (n:ran g-->RR <-> n:X-->RR))
7	5, 6	syl 10	. . . 4 |- (g = G -> (n:ran g-->RR <-> n:X-->RR))
8		fveq2 3724	. . . . . . . . 9 |- (g = G -> (Id` g) = (Id` G))
9		isnvlem.2	. . . . . . . . 9 |- Z = (Id` G)
10	8, 9	syl6eqr 1525	. . . . . . . 8 |- (g = G -> (Id` g) = Z)
11	10	eqeq2d 1486	. . . . . . 7 |- (g = G -> (x = (Id` g) <-> x = Z))
12	11	imbi2d 612	. . . . . 6 |- (g = G -> (((n` x) = 0 -> x = (Id` g)) <-> ((n` x) = 0 -> x = Z)))
13		opreq 3967	. . . . . . . . 9 |- (g = G -> (xgy) = (xGy))
14	13	fveq2d 3728	. . . . . . . 8 |- (g = G -> (n` (xgy)) = (n` (xGy)))
15	14	breq1d 2629	. . . . . . 7 |- (g = G -> ((n` (xgy)) <_ ((n` x) + (n` y)) <-> (n` (xGy)) <_ ((n` x) + (n` y))))
16	5, 15	raleq12d 1794	. . . . . 6 |- (g = G -> (A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y)) <-> A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))))
17	12, 16	3anbi13d 895	. . . . 5 |- (g = G -> ((((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))) <-> (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))))
18	5, 17	raleq12d 1794	. . . 4 |- (g = G -> (A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))) <-> A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))))
19	2, 7, 18	3anbi123d 893	. . 3 |- (g = G -> ((<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y)))) <-> (<.G, s>. e. CVec /\ n:X-->RR /\ A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))))))
20		opeq2 2488	. . . . 5 |- (s = S -> <.G, s>. = <.G, S>.)
21	20	eleq1d 1540	. . . 4 |- (s = S -> (<.G, s>. e. CVec <-> <.G, S>. e. CVec))
22		opreq 3967	. . . . . . . . 9 |- (s = S -> (ysx) = (ySx))
23	22	fveq2d 3728	. . . . . . . 8 |- (s = S -> (n` (ysx)) = (n` (ySx)))
24	23	eqeq1d 1483	. . . . . . 7 |- (s = S -> ((n` (ysx)) = ((abs` y) x. (n` x)) <-> (n` (ySx)) = ((abs` y) x. (n` x))))
25	24	ralbidv 1663	. . . . . 6 |- (s = S -> (A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) <-> A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x))))
26	25	3anbi2d 898	. . . . 5 |- (s = S -> ((((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))) <-> (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))))
27	26	ralbidv 1663	. . . 4 |- (s = S -> (A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))) <-> A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))))
28	21, 27	3anbi13d 895	. . 3 |- (s = S -> ((<.G, s>. e. CVec /\ n:X-->RR /\ A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y)))) <-> (<.G, S>. e. CVec /\ n:X-->RR /\ A.x e. X (((n` x) = 0 -> x = Z) /\ A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x)) /\ A.y e. X (n` (xGy)) <_ ((n` x) + (n` y))))))
29		feq1 3620	. . . 4 |- (n = N -> (n:X-->RR <-> N:X-->RR))
30		fveq1 3723	. . . . . . . 8 |- (n = N -> (n` x) = (N` x))
31	30	eqeq1d 1483	. . . . . . 7 |- (n = N -> ((n` x) = 0 <-> (N` x) = 0))
32	31	imbi1d 613	. . . . . 6 |- (n = N -> (((n` x) = 0 -> x = Z) <-> ((N` x) = 0 -> x = Z)))
33		fveq1 3723	. . . . . . . 8 |- (n = N -> (n` (ySx)) = (N` (ySx)))
34	30	opreq2d 3976	. . . . . . . 8 |- (n = N -> ((abs` y) x. (n` x)) = ((abs` y) x. (N` x)))
35	33, 34	eqeq12d 1489	. . . . . . 7 |- (n = N -> ((n` (ySx)) = ((abs` y) x. (n` x)) <-> (N` (ySx)) = ((abs` y) x. (N` x))))
36	35	ralbidv 1663	. . . . . 6 |- (n = N -> (A.y e. CC (n` (ySx)) = ((abs` y) x. (n` x)) <-> A.y e. CC (N` (ySx)) = ((abs` y) x. (N` x))))
37		fveq1 3723	. . . . . . . 8 |- (n = N -> (n` (xGy)) = (N` (xGy)))
38		fveq1 3723	. . . . . . . . 9 |- (n = N -> (n` y) = (N` y))
39	30, 38	opreq12d 3978	. . . . . . . 8 |- (n = N -> ((n` x) + (n` y)) = ((N` x) + (N` y)))
40	37, 39	breq12d 2631	. . . . . . 7 |- (n = N -> ((n` (