Theorem ip1cnilem6 8386

Description: Lemma for ip1cni 8387.

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 ∘ − )
ip1cni.j	⊢ J = (Open ‘C)
ip1cni.k	⊢ K = (Open ‘D)
ip1cni.f	⊢ F = {⟨w, v⟩∣(w ∈ X ⋀ v = (wPA))}
ip1cni.9	⊢ U ∈ NrmCVec
ip1cni.a	⊢ A ∈ X
ip1cnilem.4	⊢ S = ( ·s ‘U)
ip1cnilem.6	⊢ N = (norm ‘U)
ip1cnilem.16	⊢ H = {⟨u, t⟩∣(u ∈ X ⋀ t = (((i↑k) · ((N ‘(uG((i↑k)SA)))↑2)) · (1 / 4)))}

Assertion

Ref	Expression
ip1cnilem6	⊢ F ∈ (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 6008	. 2 ⊢ 4 ∈ ℕ
2		ip1cni.9	. . . 4 ⊢ U ∈ NrmCVec
3		ip1cni.8	. . . . 5 ⊢ C = (IndMet ‘U)
4	3	imsmet 8332	. . . 4 ⊢ (U ∈ NrmCVec → C ∈ Met)
5	2, 4	ax-mp 7	. . 3 ⊢ C ∈ Met
6		ip1cni.1	. . . 4 ⊢ X = (Base ‘U)
7	6, 3, 2	imsbai 8330	. . 3 ⊢ X = dom dom C
8		ip1cni.d	. . 3 ⊢ D = (abs ∘ − )
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 ∈ X ⋀ v = (wPA))}
14		ip1cni.a	. . . 4 ⊢ A ∈ X
15		ip1cnilem.4	. . . 4 ⊢ S = ( ·s ‘U)
16		ip1cnilem.6	. . . 4 ⊢ N = (norm ‘U)
17		ip1cnilem.16	. . . 4 ⊢ H = {⟨u, t⟩∣(u ∈ X ⋀ t = (((i↑k) · ((N ‘(uG((i↑k)SA)))↑2)) · (1 / 4)))}
18	6, 11, 12, 3, 8, 9, 10, 13, 2, 14, 15, 16, 17	ip1cnilem5 8385	. . 3 ⊢ (k ∈ ℕ → H ∈ (J Cn K))
19		axmulcl 5286	. . . . . . . . . . . . 13 ⊢ (((i↑k) ∈ ℂ ⋀ ((N ‘(wG((i↑k)SA)))↑2) ∈ ℂ) → ((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ)
20		nnnn0t 6112	. . . . . . . . . . . . . . 15 ⊢ (k ∈ ℕ → k ∈ ℕ0)
21		axicn 5283	. . . . . . . . . . . . . . . 16 ⊢ i ∈ ℂ
22		expclt 6594	. . . . . . . . . . . . . . . 16 ⊢ ((i ∈ ℂ ⋀ k ∈ ℕ0) → (i↑k) ∈ ℂ)
23	21, 22	mpan 699	. . . . . . . . . . . . . . 15 ⊢ (k ∈ ℕ0 → (i↑k) ∈ ℂ)
24	20, 23	syl 10	. . . . . . . . . . . . . 14 ⊢ (k ∈ ℕ → (i↑k) ∈ ℂ)
25	24	adantl 390	. . . . . . . . . . . . 13 ⊢ ((w ∈ X ⋀ k ∈ ℕ) → (i↑k) ∈ ℂ)
26	6, 11	nvgcl 8247	. . . . . . . . . . . . . . . . . 18 ⊢ ((U ∈ NrmCVec ⋀ w ∈ X ⋀ ((i↑k)SA) ∈ X) → (wG((i↑k)SA)) ∈ X)
27	2, 26	mp3an1 907	. . . . . . . . . . . . . . . . 17 ⊢ ((w ∈ X ⋀ ((i↑k)SA) ∈ X) → (wG((i↑k)SA)) ∈ X)
28	6, 15	nvscl 8255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((U ∈ NrmCVec ⋀ (i↑k) ∈ ℂ ⋀ A ∈ X) → ((i↑k)SA) ∈ X)
29	2, 14, 28	mp3an13 911	. . . . . . . . . . . . . . . . . 18 ⊢ ((i↑k) ∈ ℂ → ((i↑k)SA) ∈ X)
30	24, 29	syl 10	. . . . . . . . . . . . . . . . 17 ⊢ (k ∈ ℕ → ((i↑k)SA) ∈ X)
31	27, 30	sylan2 454	. . . . . . . . . . . . . . . 16 ⊢ ((w ∈ X ⋀ k ∈ ℕ) → (wG((i↑k)SA)) ∈ X)
32	6, 16	nvcl 8295	. . . . . . . . . . . . . . . . 17 ⊢ ((U ∈ NrmCVec ⋀ (wG((i↑k)SA)) ∈ X) → (N ‘(wG((i↑k)SA))) ∈ ℝ)
33	2, 32	mpan 699	. . . . . . . . . . . . . . . 16 ⊢ ((wG((i↑k)SA)) ∈ X → (N ‘(wG((i↑k)SA))) ∈ ℝ)
34	31, 33	syl 10	. . . . . . . . . . . . . . 15 ⊢ ((w ∈ X ⋀ k ∈ ℕ) → (N ‘(wG((i↑k)SA))) ∈ ℝ)
35	34	recnd 5328	. . . . . . . . . . . . . 14 ⊢ ((w ∈ X ⋀ k ∈ ℕ) → (N ‘(wG((i↑k)SA))) ∈ ℂ)
36		sqclt 6624	. . . . . . . . . . . . . 14 ⊢ ((N ‘(wG((i↑k)SA))) ∈ ℂ → ((N ‘(wG((i↑k)SA)))↑2) ∈ ℂ)
37	35, 36	syl 10	. . . . . . . . . . . . 13 ⊢ ((w ∈ X ⋀ k ∈ ℕ) → ((N ‘(wG((i↑k)SA)))↑2) ∈ ℂ)
38	19, 25, 37	sylanc 474	. . . . . . . . . . . 12 ⊢ ((w ∈ X ⋀ k ∈ ℕ) → ((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ)
39		elfznnt 6444	. . . . . . . . . . . 12 ⊢ (k ∈ (1...4) → k ∈ ℕ)
40	38, 39	sylan2 454	. . . . . . . . . . 11 ⊢ ((w ∈ X ⋀ k ∈ (1...4)) → ((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ)
41	40	r19.21aiva 1721	. . . . . . . . . 10 ⊢ (w ∈ X → ∀k ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ)
42		elnnuz 6390	. . . . . . . . . . . 12 ⊢ (4 ∈ ℕ ↔ 4 ∈ (ℤ≥ ‘1))
43	1, 42	mpbi 189	. . . . . . . . . . 11 ⊢ 4 ∈ (ℤ≥ ‘1)
44		fsumclt 7029	. . . . . . . . . . 11 ⊢ ((4 ∈ (ℤ≥ ‘1) ⋀ ∀k ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ) → Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ)
45	43, 44	mpan 699	. . . . . . . . . 10 ⊢ (∀k ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ → Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ)
46	41, 45	syl 10	. . . . . . . . 9 ⊢ (w ∈ X → Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ)
47		4re 5988	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
48	47	recn 5327	. . . . . . . . . 10 ⊢ 4 ∈ ℂ
49		4pos 5998	. . . . . . . . . . 11 ⊢ 0 < 4
50	47, 49	gt0ne0i 5630	. . . . . . . . . 10 ⊢ 4 ≠ 0
51		divrect 5747	. . . . . . . . . 10 ⊢ ((Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ ⋀ 4 ∈ ℂ ⋀ 4 ≠ 0) → (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) / 4) = (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
52	48, 50, 51	mp3an23 912	. . . . . . . . 9 ⊢ (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ → (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) / 4) = (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
53	46, 52	syl 10	. . . . . . . 8 ⊢ (w ∈ X → (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) / 4) = (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
54	6, 11, 15, 16, 12	ipval 8361	. . . . . . . . 9 ⊢ ((U ∈ NrmCVec ⋀ w ∈ X ⋀ A ∈ X) → (wPA) = (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) / 4))
55	2, 14, 54	mp3an13 911	. . . . . . . 8 ⊢ (w ∈ X → (wPA) = (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) / 4))
56		opreq1 3982	. . . . . . . . . . . . . . 15 ⊢ (u = w → (uG((i↑k)SA)) = (wG((i↑k)SA)))
57	56	fveq2d 3742	. . . . . . . . . . . . . 14 ⊢ (u = w → (N ‘(uG((i↑k)SA))) = (N ‘(wG((i↑k)SA))))
58	57	opreq1d 3989	. . . . . . . . . . . . 13 ⊢ (u = w → ((N ‘(uG((i↑k)SA)))↑2) = ((N ‘(wG((i↑k)SA)))↑2))
59	58	opreq2d 3990	. . . . . . . . . . . 12 ⊢ (u = w → ((i↑k) · ((N ‘(uG((i↑k)SA)))↑2)) = ((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)))
60	59	opreq1d 3989	. . . . . . . . . . 11 ⊢ (u = w → (((i↑k) · ((N ‘(uG((i↑k)SA)))↑2)) · (1 / 4)) = (((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
61		oprex 3997	. . . . . . . . . . 11 ⊢ (((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)) ∈ V
62	60, 17, 61	fvopab4 3794	. . . . . . . . . 10 ⊢ (w ∈ X → (H ‘w) = (((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
63	62	sumeq2sdv 7007	. . . . . . . . 9 ⊢ (w ∈ X → Σk ∈ (1...4)(H ‘w) = Σk ∈ (1...4)(((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
64	48, 50	reccl 5726	. . . . . . . . . . 11 ⊢ (1 / 4) ∈ ℂ
65		fsummulc2 7048	. . . . . . . . . . 11 ⊢ ((4 ∈ (ℤ≥ ‘1) ⋀ (1 / 4) ∈ ℂ ⋀ ∀k ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ) → (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)) = Σk ∈ (1...4)(((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
66	43, 64, 65	mp3an12 910	. . . . . . . . . 10 ⊢ (∀k ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) ∈ ℂ → (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)) = Σk ∈ (1...4)(((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
67	41, 66	syl 10	. . . . . . . . 9 ⊢ (w ∈ X → (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)) = Σk ∈ (1...4)(((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
68	63, 67	eqtr4d 1517	. . . . . . . 8 ⊢ (w ∈ X → Σk ∈ (1...4)(H ‘w) = (Σk ∈ (1...4)((i↑k) · ((N ‘(wG((i↑k)SA)))↑2)) · (1 / 4)))
69	53, 55, 68	3eqtr4rd 1525	. . . . . . 7 ⊢ (w ∈ X → Σk ∈ (1...4)(H ‘w) = (wPA))
70	69	eqeq2d 1493	. . . . . 6 ⊢ (w ∈ X → (v = Σk ∈ (1...4)(H ‘w) ↔ v = (wPA)))
71	70	pm5.32i 648	. . . . 5 ⊢ ((w ∈ X ⋀ v = Σk ∈ (1...4)(H ‘w)) ↔ (w ∈ X ⋀ v = (wPA)))
72	71	opabbii 2684	. . . 4 ⊢ {⟨w, v⟩∣(w ∈ X ⋀ v = Σk ∈ (1...4)(H ‘w))} = {⟨w, v⟩∣(w ∈ X ⋀ v = (wPA))}
73	13, 72	eqtr4 1505	. . 3 ⊢ F = {⟨w, v⟩∣(w ∈ X ⋀ v = Σk ∈ (1...4)(H ‘w))}
74	5, 7, 8, 9, 10, 18, 73	fsumcn 7999	. 2 ⊢ (4 ∈ ℕ → F ∈ (J Cn K))
75	1, 74	ax-mp 7	1 ⊢ F ∈ (J Cn K)

Syntax hints:   ⋀ wa 223   = wceq 960   ∈ wcel 962   ≠ wne 1592  ∀wral 1652  {copab 2679   ∘ ccom 3188   ‘cfv 3196  (class class class)co 3977  ℂcc 5245  ℝcr 5246  0cc0 5247  1c1 5248  ici 5249   · cmul 5252   − cmin 5305   / cdiv 5307  ℕcn 5309  ℕ₀cn0 5310  2c2 5967  4c4 5969  ℤ_≥cuz 6367  ...cfz 6417  ↑cexp 6581  abscabs 6764  Σcsu 6993   Cn ccn 7761  Metcme 7798  Opencopn 7801  NrmCVeccnv 8211   +_v cpv 8212  Basecba 8213   ·_s cns 8214  normcnm 8217  IndMetcims 8218   ·_i cip 8357

This theorem is referenced by:  ip1cni 8387

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-rep 2706  ax-sep 2716  ax-nul 2723  ax-pow 2756  ax-pr 2793  ax-un 2880  ax-reg 4603  ax-inf2 4637  ax-ac 4756

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-nel 1595  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2010  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-pss 2064  df-nul 2290  df-if 2372  df-pw 2412  df-sn 2422  df-pr 2423  df-tp 2425  df-op 2426  df-uni 2516  df-int 2546  df-iun 2580  df-iin 2581  df-br 2633  df-opab 2680  df-tr 2694  df-eprel 2846  df-id 2849  df-po 2854  df-so 2864  df-fr 2931  df-we 2948  df-ord 2965  df-on 2966  df-lim 2967  df-suc 2968  df-om 3146  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-f1 3209  df-fo 3210  df-f1o 3211  df-fv 3212  df-rdg 3946  df-opr 3979  df-oprab 3980  df-1st 4093  df-2nd 4094  df-1o 4147  df-oadd 4149  df-omul 4150  df-er 4275  df-ec 4277  df-qs 4280  df-map 4338  df-en 4382  df-dom 4383  df-sdom 4384  df-sup 4584  df-r1 4655  df-rank 4656  df-ni 5013  df-pli 5014  df-mi 5015  df-lti 5016  df-plpq 5048  df-mpq 5049  df-enq 5050  df-nq 5051  df-plq 5052  df-mq 5053  df-rq 5054  df-ltq 5055  df-1q 5056  df-np 5099  df-1p 5100  df-plp 5101  df-mp 5102  df-ltp 5103  df-plpr 5177  df-mpr 5178  df-enr 5179  df-nr 5180  df-plr 5181  df-mr 5182  df-ltr 5183  df-0r 5184  df-1r 5185  df-m1r 5186  df-c 5253  df-0 5254  df-1 5255  df-i 5256  df-r 5257  df-plus 5258  df-mul 5259  df-lt 5260  df-sub 5369  df-neg 5371  df-pnf 5500  df-mnf 5501  df-xr 5502  df-ltxr 5503  df-le 5504  df-div 5716  df-n 5931  df-2 5976  df-3 5977  df-4 5978  df-n0 6106  df-z 6142  df-fl 6233  df-uz 6368  df-fz 6418  df-seq1 6491  df-shft 6524  df-seqz 6546  df-exp 6582  df-sqr 6684  df-re 6765  df-im 6766  df-cj 6767  df-abs 6768  df-clim 6989  df-sum 6994  df-top 7607  df-cn 7763  df-cnp 7764  df-met 7802  df-bl 7804  df-opn 7805  df-lm 7931  df-grp 8046  df-gid 8047  df-ginv 8048  df-gdiv 8049  df-abl 8108  df-vc 8173  df-nv 8219  df-va 8222  df-ba 8223  df-sm 8224  df-0v 8225  df-vs 8226  df-nm 8227  df-ims 8228  df-ip 8358

Copyright terms: Public domain