Theorem ip1cnilem6 8312

Description: Lemma for ip1cni 8313.

Hypotheses

Ref	Expression
ip1cni.1	|- X = (Base` U)
ip1cni.2	|- G = (+v` U)
ip1cni.7	|- P = (.i` U)
ip1cni.8	|- C = (IndMet` U)
ip1cni.d	|- D = (abs o. - )
ip1cni.j	|- J = (Open` C)
ip1cni.k	|- K = (Open` D)
ip1cni.f	|- F = {<.w, v>. | (w e. X /\ v = (wPA))}
ip1cni.9	|- U e. NrmCVec
ip1cni.a	|- A e. X
ip1cnilem.4	|- S = (.s` U)
ip1cnilem.6	|- N = (norm` U)
ip1cnilem.16	|- H = {<.u, t>. | (u e. X /\ t = (((i^k) x. ((N` (uG((i^k)SA)))^2)) x. (1 / 4)))}

Assertion

Ref	Expression
ip1cnilem6	|- F e. (J Cn K)

Distinct variable groups:   t,k,u,v,w,A   u,C,w   u,D,w   k,G,t,u,v,w   v,H,w   k,J,u,w   k,K,u,w   k,N,t,u,v,w   S,k,t,u,v,w   U,k,t,u,v,w   k,X,t,u,v,w

Proof of Theorem ip1cnilem6

Step	Hyp	Ref	Expression
1		4nn 5949	. 2 |- 4 e. NN
2		ip1cni.9	. . . 4 |- U e. NrmCVec
3		ip1cni.8	. . . . 5 |- C = (IndMet` U)
4	3	imsmet 8262	. . . 4 |- (U e. NrmCVec -> C e. Met)
5	2, 4	ax-mp 7	. . 3 |- C e. Met
6		ip1cni.1	. . . 4 |- X = (Base` U)
7	6, 3, 2	imsbai 8260	. . 3 |- X = dom dom C
8		ip1cni.d	. . 3 |- D = (abs o. - )
9		ip1cni.j	. . 3 |- J = (Open` C)
10		ip1cni.k	. . 3 |- K = (Open` D)
11		ip1cni.2	. . . 4 |- G = (+v` U)
12		ip1cni.7	. . . 4 |- P = (.i` U)
13		ip1cni.f	. . . 4 |- F = {<.w, v>. | (w e. X /\ v = (wPA))}
14		ip1cni.a	. . . 4 |- A e. X
15		ip1cnilem.4	. . . 4 |- S = (.s` U)
16		ip1cnilem.6	. . . 4 |- N = (norm` U)
17		ip1cnilem.16	. . . 4 |- H = {<.u, t>. | (u e. X /\ t = (((i^k) x. ((N` (uG((i^k)SA)))^2)) x. (1 / 4)))}
18	6, 11, 12, 3, 8, 9, 10, 13, 2, 14, 15, 16, 17	ip1cnilem5 8311	. . 3 |- (k e. NN -> H e. (J Cn K))
19		axmulcl 5245	. . . . . . . . . . . . 13 |- (((i^k) e. CC /\ ((N` (wG((i^k)SA)))^2) e. CC) -> ((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC)
20		nnnn0t 6053	. . . . . . . . . . . . . . 15 |- (k e. NN -> k e. NN0)
21		axicn 5242	. . . . . . . . . . . . . . . 16 |- i e. CC
22		expclt 6513	. . . . . . . . . . . . . . . 16 |- ((i e. CC /\ k e. NN0) -> (i^k) e. CC)
23	21, 22	mpan 693	. . . . . . . . . . . . . . 15 |- (k e. NN0 -> (i^k) e. CC)
24	20, 23	syl 10	. . . . . . . . . . . . . 14 |- (k e. NN -> (i^k) e. CC)
25	24	adantl 388	. . . . . . . . . . . . 13 |- ((w e. X /\ k e. NN) -> (i^k) e. CC)
26	6, 11	nvgcl 8179	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ w e. X /\ ((i^k)SA) e. X) -> (wG((i^k)SA)) e. X)
27	2, 26	mp3an1 900	. . . . . . . . . . . . . . . . 17 |- ((w e. X /\ ((i^k)SA) e. X) -> (wG((i^k)SA)) e. X)
28	6, 15	nvscl 8187	. . . . . . . . . . . . . . . . . . 19 |- ((U e. NrmCVec /\ (i^k) e. CC /\ A e. X) -> ((i^k)SA) e. X)
29	2, 14, 28	mp3an13 904	. . . . . . . . . . . . . . . . . 18 |- ((i^k) e. CC -> ((i^k)SA) e. X)
30	24, 29	syl 10	. . . . . . . . . . . . . . . . 17 |- (k e. NN -> ((i^k)SA) e. X)
31	27, 30	sylan2 451	. . . . . . . . . . . . . . . 16 |- ((w e. X /\ k e. NN) -> (wG((i^k)SA)) e. X)
32	6, 16	nvcl 8227	. . . . . . . . . . . . . . . . 17 |- ((U e. NrmCVec /\ (wG((i^k)SA)) e. X) -> (N` (wG((i^k)SA))) e. RR)
33	2, 32	mpan 693	. . . . . . . . . . . . . . . 16 |- ((wG((i^k)SA)) e. X -> (N` (wG((i^k)SA))) e. RR)
34	31, 33	syl 10	. . . . . . . . . . . . . . 15 |- ((w e. X /\ k e. NN) -> (N` (wG((i^k)SA))) e. RR)
35	34	recnd 5287	. . . . . . . . . . . . . 14 |- ((w e. X /\ k e. NN) -> (N` (wG((i^k)SA))) e. CC)
36		sqclt 6542	. . . . . . . . . . . . . 14 |- ((N` (wG((i^k)SA))) e. CC -> ((N` (wG((i^k)SA)))^2) e. CC)
37	35, 36	syl 10	. . . . . . . . . . . . 13 |- ((w e. X /\ k e. NN) -> ((N` (wG((i^k)SA)))^2) e. CC)
38	19, 25, 37	sylanc 471	. . . . . . . . . . . 12 |- ((w e. X /\ k e. NN) -> ((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC)
39		elfznnt 6426	. . . . . . . . . . . 12 |- (k e. (1...4) -> k e. NN)
40	38, 39	sylan2 451	. . . . . . . . . . 11 |- ((w e. X /\ k e. (1...4)) -> ((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC)
41	40	r19.21aiva 1706	. . . . . . . . . 10 |- (w e. X -> A.k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC)
42		elnnuz 6372	. . . . . . . . . . . 12 |- (4 e. NN <-> 4 e. (ZZ>` 1))
43	1, 42	mpbi 189	. . . . . . . . . . 11 |- 4 e. (ZZ>` 1)
44		fsumclt 6953	. . . . . . . . . . 11 |- ((4 e. (ZZ>` 1) /\ A.k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC) -> sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC)
45	43, 44	mpan 693	. . . . . . . . . 10 |- (A.k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC -> sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC)
46	41, 45	syl 10	. . . . . . . . 9 |- (w e. X -> sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC)
47		4re 5929	. . . . . . . . . . 11 |- 4 e. RR
48	47	recn 5286	. . . . . . . . . 10 |- 4 e. CC
49		4pos 5939	. . . . . . . . . . 11 |- 0 < 4
50	47, 49	gt0ne0i 5591	. . . . . . . . . 10 |- 4 =/= 0
51		divrect 5702	. . . . . . . . . 10 |- ((sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC /\ 4 e. CC /\ 4 =/= 0) -> (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) / 4) = (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) x. (1 / 4)))
52	48, 50, 51	mp3an23 905	. . . . . . . . 9 |- (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) e. CC -> (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) / 4) = (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) x. (1 / 4)))
53	46, 52	syl 10	. . . . . . . 8 |- (w e. X -> (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) / 4) = (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) x. (1 / 4)))
54	6, 11, 15, 16, 12	ipval 8287	. . . . . . . . 9 |- ((U e. NrmCVec /\ w e. X /\ A e. X) -> (wPA) = (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) / 4))
55	2, 14, 54	mp3an13 904	. . . . . . . 8 |- (w e. X -> (wPA) = (sum_k e. (1...4)((i^k) x. ((N` (wG((i^k)SA)))^2)) / 4))
56		opreq1 3953	. . . . . . . . . . . . . . 15 |- (u = w -> (uG((i^k)SA)) = (wG((i^k)SA)))
57	56	fveq2d 3713	. . . . . . . . . . . . . 14 |- (u = w -> (N` (uG((i^k)SA))) = (N` (wG((i^k)SA))))
58	57	opreq1d 3960	. . . . . . . . . . . . 13 |- (u = w -> ((N` (uG((i^k)SA)))^2) = ((N` (wG((i^k)SA)))^2))
59	58	opreq2d 3961	. . . . . . . . . . . 12 |- (u = w -> ((i^k) x. ((N` (uG((i^k)SA)))^2)) = ((i^k) x. ((N` (wG((i^k)SA)))^2)))
60	59	opreq1d 3960	. . . . . . . . . . 11 |- (u = w