Theorem va1cnlem 8345

Description: Lemma for va1cn 8346.

Hypotheses

Ref	Expression
va1cn.1	|- X = (Base` U)
va1cn.2	|- G = (+v` U)
va1cn.8	|- D = (IndMet` U)
va1cn.j	|- J = (Open` D)
va1cn.f	|- F = {<.w, v>. | (w e. X /\ v = (wGA))}
va1cn.9	|- U e. NrmCVec
va1cnlem.6	|- N = (norm` U)

Assertion

Ref	Expression
va1cnlem	|- (A e. X -> F e. (J Cn J))

Distinct variable groups:   w,v,A   v,G,w   v,X,w

Proof of Theorem va1cnlem

Step	Hyp	Ref	Expression
1		va1cn.9	. . . . . . 7 |- U e. NrmCVec
2		va1cn.1	. . . . . . . 8 |- X = (Base` U)
3		va1cn.2	. . . . . . . 8 |- G = (+v` U)
4	2, 3	nvgcl 8239	. . . . . . 7 |- ((U e. NrmCVec /\ w e. X /\ A e. X) -> (wGA) e. X)
5	1, 4	mp3an1 903	. . . . . 6 |- ((w e. X /\ A e. X) -> (wGA) e. X)
6	5	ancoms 436	. . . . 5 |- ((A e. X /\ w e. X) -> (wGA) e. X)
7	6	r19.21aiva 1714	. . . 4 |- (A e. X -> A.w e. X (wGA) e. X)
8		va1cn.f	. . . . 5 |- F = {<.w, v>. | (w e. X /\ v = (wGA))}
9	8	fopab2 3823	. . . 4 |- (A.w e. X (wGA) e. X <-> F:X-->X)
10	7, 9	sylib 198	. . 3 |- (A e. X -> F:X-->X)
11		idd 61	. . . . . . . . . 10 |- (u e. X -> ((rDu) < s -> (rDu) < s))
12	11	rgen 1698	. . . . . . . . 9 |- A.u e. X ((rDu) < s -> (rDu) < s)
13		breq2 2623	. . . . . . . . . . 11 |- (t = s -> (0 < t <-> 0 < s))
14		breq2 2623	. . . . . . . . . . . . 13 |- (t = s -> ((rDu) < t <-> (rDu) < s))
15	14	imbi1d 613	. . . . . . . . . . . 12 |- (t = s -> (((rDu) < t -> (rDu) < s) <-> ((rDu) < s -> (rDu) < s)))
16	15	ralbidv 1663	. . . . . . . . . . 11 |- (t = s -> (A.u e. X ((rDu) < t -> (rDu) < s) <-> A.u e. X ((rDu) < s -> (rDu) < s)))
17	13, 16	anbi12d 628	. . . . . . . . . 10 |- (t = s -> ((0 < t /\ A.u e. X ((rDu) < t -> (rDu) < s)) <-> (0 < s /\ A.u e. X ((rDu) < s -> (rDu) < s))))
18	17	rcla4ev 1877	. . . . . . . . 9 |- ((s e. RR /\ (0 < s /\ A.u e. X ((rDu) < s -> (rDu) < s))) -> E.t e. RR (0 < t /\ A.u e. X ((rDu) < t -> (rDu) < s)))
19	12, 18	mpanr2 710	. . . . . . . 8 |- ((s e. RR /\ 0 < s) -> E.t e. RR (0 < t /\ A.u e. X ((rDu) < t -> (rDu) < s)))
20	19	adantll 392	. . . . . . 7 |- (((r e. X /\ s e. RR) /\ 0 < s) -> E.t e. RR (0 < t /\ A.u e. X ((rDu) < t -> (rDu) < s)))
21	20	adantl 388	. . . . . 6 |- ((A e. X /\ ((r e. X /\ s e. RR) /\ 0 < s)) -> E.t e. RR (0 < t /\ A.u e. X ((rDu) < t -> (rDu) < s)))
22		opreq1 3968	. . . . . . . . . . . . . . . . 17 |- (w = r -> (wGA) = (rGA))
23		oprex 3983	. . . . . . . . . . . . . . . . 17 |- (rGA) e. V
24	22, 8, 23	fvopab4 3780	. . . . . . . . . . . . . . . 16 |- (r e. X -> (F` r) = (rGA))
25		opreq1 3968	. . . . . . . . . . . . . . . . 17 |- (w = u -> (wGA) = (uGA))
26		oprex 3983	. . . . . . . . . . . . . . . . 17 |- (uGA) e. V
27	25, 8, 26	fvopab4 3780	. . . . . . . . . . . . . . . 16 |- (u e. X -> (F` u) = (uGA))
28	24, 27	opreqan12d 3979	. . . . . . . . . . . . . . 15 |- ((r e. X /\ u e. X) -> ((F` r)D(F` u)) = ((rGA)D(uGA)))
29	28	adantll 392	. . . . . . . . . . . . . 14 |- (((A e. X /\ r e. X) /\ u e. X) -> ((F` r)D(F` u)) = ((rGA)D(uGA)))
30	3	nvgrp 8236	. . . . . . . . . . . . . . . . . . . 20 |- (U e. NrmCVec -> G e. Grp)
31	1, 30	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- G e. Grp
32	2, 3	bafval 8223	. . . . . . . . . . . . . . . . . . . 20 |- X = ran G
33		eqid 1475	. . . . . . . . . . . . . . . . . . . . 21 |- (-v` U) = (-v` U)
34	3, 33	vsfval 8254	. . . . . . . . . . . . . . . . . . . 20 |- (-v` U) = ( /g ` G)
35	32, 34	grppnpcan2 8092	. . . . . . . . . . . . . . . . . . 19 |- ((G e. Grp /\ (r e. X /\ u e. X /\ A e. X)) -> ((rGA)(-v` U)(uGA)) = (r(-v` U)u))
36	31, 35	mpan 695	. . . . . . . . . . . . . . . . . 18 |- ((r e. X /\ u e. X /\ A e. X) -> ((rGA)(-v` U)(uGA)) = (r(-v` U)u))
37	36	fveq2d 3728	. . . . . . . . . . . . . . . . 17 |- ((r e. X /\ u e. X /\ A e. X) -> (N` ((rGA)(-v` U)(uGA))) = (N` (r(-v` U)u)))
38		va1cnlem.6	. . . . . . . . . . . . . . . . . . . 20 |- N = (norm` U)
39		va1cn.8	. . . . . . . . . . . . . . . . . . . 20 |- D = (IndMet` U)
40	2, 33, 38, 39	imsdval 8317	. . . . . . . . . . . . . . . . . . 19 |- ((U e. NrmCVec /\ (rGA) e. X /\ (uGA) e. X) -> ((rGA)D(uGA)) = (N` ((rGA)(-v` U)(uGA))))
41	1, 40	mp3an1 903	. . . . . . . . . . . . . . . . . 18 |- (((rGA) e. X /\ (uGA) e. X) -> ((rGA)D(uGA)) = (N` ((rGA)(-v` U)(uGA))))
42	2, 3	nvgcl 8239	. . . . . . . . . . . . . . . . . . . 20 |- ((U e. NrmCVec /\ r e. X /\ A e. X) -> (rGA) e. X)
43	1, 42	mp3an1 903	. . . . . . . . . . . . . . . . . . 19 |- ((r e. X /\ A e. X) -> (rGA) e. X)
44	43	3adant2 798	. . . . . . . . . . . . . . . . . 18 |- ((r e. X /\ u e. X /\ A e. X) -> (rGA) e. X)
45	2, 3	nvgcl 8239	. . . . . . . . . . . . . . . . . . . 20 |- ((U e. NrmCVec /\ u e. X /\ A e. X) -> (uGA) e. X)
46	1, 45	mp3an1 903	. . . . . . . . . . . . . . . . . . 19 |- ((u e. X /\ A e. X) -> (uGA) e. X)
47	46	3adant1 797	. . . . . . . . . . . . . . . . . 18 |- ((r e. X /\ u e. X /\ A e. X) -> (uGA) e. X)
48	41, 44, 47	sylanc 471	. . . . . . . . . . . . . . . . 17 |- ((r e. X /\ u e. X /\ A e. X) -> ((rGA)D(uGA)) = (N` ((rGA)(-v` U)(uGA))))
49	2, 33, 38, 39	imsdval 8317	. . . . . . . . . . . . . . . . . . 19 |- ((U e. NrmCVec /\ r e. X /\ u e. X) -> (rDu) = (N` (r(-v` U)u)))
50	1, 49	mp3an1 903	. . . . . . . . . . . . . . . . . 18 |- ((r e. X /\ u e. X) -> (rDu) = (N` (r(-v` U)u)))
51	50	3adant3 799	. . . . . . . . . . . . . . . . 17 |- ((r e. X /\ u e. X /\ A e. X) -> (rDu) = (N` (r(-v` U)u)))
52	37, 48, 51	3eqtr4d 1517	. . . . . . . . . . . . . . . 16 |- ((r e. X /\ u e. X /\ A e. X) -> ((rGA)D(uGA)) = (rDu))
53	52	3comr 841	. . . . . . . . . . . . . . 15 |- ((A e. X /\ r e. X /\ u e. X) -> ((rGA)D(uGA)) = (rDu))
54	53	3expa 833	. . . . . . . . . . . . . 14 |- (((A e. X /\ r e. X) /\ u e. X) -> ((rGA)D(uGA)) = (rDu))
55	29, 54	eqtrd 1507	. . . . . . . . . . . . 13 |- (((A e. X /\ r e. X) /\ u e. X) -> ((F` r)D(F` u)) = (rDu))
56	55	breq1d 2629	. . . . . . . . . . . 12 |- (((A e. X /\ r e. X) /\ u e. X) -> (((F` r)D(F` u)) < s <-> (rDu) < s))
57	56	imbi2d 612	. . . . . . . . . . 11 |- (((A e. X /\ r e. X) /\ u e. X) -> (((rDu) < t -> ((F` r)D(F` u)) < s) <-> ((rDu) < t -> (rDu) < s)))
58	57	ralbidva 1659	. . . . . . . . . 10 |- ((A e. X /\ r e. X) -> (A.u e. X ((rDu) < t -> ((F` r)D(F` u)) < s) <-> A.u e. X ((rDu) < t -> (rDu) < s)))
59	58	anbi2d 616	. . . . . . . . 9 |- ((A e. X /\ r e. X) -> ((0 < t /\ A.u e. X ((rDu) < t -> ((F` r)D(F` u)) < s)) <-> (0 < t /\ A.u e. X ((rDu) < t -> (rDu) < s))))
60	59	rexbidv 1664	. . . . . . . 8 |- ((A e. X /\ r e. X) -> (E.t e. RR (0 < t /\ A.u e. X ((rDu) < t -> ((F` r)D(F` u)) < s)) <-> E.t e. RR (0 < t /\ A.u e. X ((rDu) < t -> (rDu) < s))))
61	60	adantrr 395	. . . . . . 7 |- ((A e. X /\ (r e. X /\ s e. RR)) -> (E.t e. RR (0 < t /\ A.u e. X ((rD