ipval2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ipval2		Structured version Visualization version GIF version

Theorem ipval2 31342

Description: Expansion of the inner product value ipval 31338. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
dipfval.1	⊢ 𝑋 = (BaseSet‘𝑈)
dipfval.2	⊢ 𝐺 = ( +_𝑣 ‘𝑈)
dipfval.4	⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
dipfval.6	⊢ 𝑁 = (norm_CV‘𝑈)
dipfval.7	⊢ 𝑃 = (·_𝑖OLD‘𝑈)

**Assertion**
Ref	Expression
ipval2	⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))) / 4))

Proof of Theorem ipval2 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dipfval.1	. . 3 ⊢ 𝑋 = (BaseSet‘𝑈)
2		dipfval.2	. . 3 ⊢ 𝐺 = ( +_𝑣 ‘𝑈)
3		dipfval.4	. . 3 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
4		dipfval.6	. . 3 ⊢ 𝑁 = (norm_CV‘𝑈)
5		dipfval.7	. . 3 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
6	1, 2, 3, 4, 5	ipval 31338	. 2 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) / 4))
7		ax-icn 11289	. . . . . . . . 9 ⊢ i ∈ ℂ
8	1, 2, 3, 4, 5	ipval2lem4 31341	. . . . . . . . . 10 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ i ∈ ℂ) → ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) ∈ ℂ)
9	7, 8	mpan2 704	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) ∈ ℂ)
10		mulcl 11314	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) ∈ ℂ) → (i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) ∈ ℂ)
11	7, 9, 10	sylancr 599	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) ∈ ℂ)
12		neg1cn 12335	. . . . . . . . 9 ⊢ -1 ∈ ℂ
13	1, 2, 3, 4, 5	ipval2lem4 31341	. . . . . . . . 9 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ -1 ∈ ℂ) → ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2) ∈ ℂ)
14	12, 13	mpan2 704	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2) ∈ ℂ)
15	11, 14	subcld 11699	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) ∈ ℂ)
16		negicn 11588	. . . . . . . . 9 ⊢ -i ∈ ℂ
17	1, 2, 3, 4, 5	ipval2lem4 31341	. . . . . . . . 9 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ -i ∈ ℂ) → ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2) ∈ ℂ)
18	16, 17	mpan2 704	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2) ∈ ℂ)
19		mulcl 11314	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2) ∈ ℂ) → (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)) ∈ ℂ)
20	7, 18, 19	sylancr 599	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)) ∈ ℂ)
21	15, 20	negsubd 11705	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + -(i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) = (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
22	14	mulm1d 11798	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) = -((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))
23	22	oveq2d 7462	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + -((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)))
24	11, 14	negsubd 11705	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + -((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)))
25	23, 24	eqtrd 2798	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)))
26		mulneg1 11782	. . . . . . . 8 ⊢ ((i ∈ ℂ ∧ ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2) ∈ ℂ) → ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)) = -(i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))
27	7, 18, 26	sylancr 599	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)) = -(i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))
28	25, 27	oveq12d 7464	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) = (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + -(i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
29		subdi 11779	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) ∈ ℂ ∧ ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2) ∈ ℂ) → (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
30	7, 29	mp3an1 1478	. . . . . . . . 9 ⊢ ((((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) ∈ ℂ ∧ ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2) ∈ ℂ) → (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
31	9, 18, 30	syl2anc 596	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
32	31	oveq1d 7461	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) = (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)))
33	11, 20, 14	sub32d 11731	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) = (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
34	32, 33	eqtrd 2798	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) = (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) − (i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
35	21, 28, 34	3eqtr4d 2808	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) = ((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)))
36	1, 3	nvsid 31262	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵)
37	36	oveq2d 7462	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺(1𝑆𝐵)) = (𝐴𝐺𝐵))
38	37	fveq2d 6915	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (𝑁‘(𝐴𝐺(1𝑆𝐵))) = (𝑁‘(𝐴𝐺𝐵)))
39	38	oveq1d 7461	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2) = ((𝑁‘(𝐴𝐺𝐵))↑2))
40	39	3adant2 1149	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2) = ((𝑁‘(𝐴𝐺𝐵))↑2))
41	40	oveq2d 7462	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2)) = (1 · ((𝑁‘(𝐴𝐺𝐵))↑2)))
42	1, 2, 3, 4, 5	ipval2lem3 31340	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℝ)
43	42	recnd 11367	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑁‘(𝐴𝐺𝐵))↑2) ∈ ℂ)
44	43	mullidd 11357	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · ((𝑁‘(𝐴𝐺𝐵))↑2)) = ((𝑁‘(𝐴𝐺𝐵))↑2))
45	41, 44	eqtrd 2798	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2)) = ((𝑁‘(𝐴𝐺𝐵))↑2))
46	35, 45	oveq12d 7464	. . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) + (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2))) = (((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + ((𝑁‘(𝐴𝐺𝐵))↑2)))
47		nnuz 13034	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
48		df-4 12437	. . . . . 6 ⊢ 4 = (3 + 1)
49		oveq2 7454	. . . . . . . 8 ⊢ (𝑘 = 4 → (i↑𝑘) = (i↑4))
50		i4 14378	. . . . . . . 8 ⊢ (i↑4) = 1
51	49, 50	eqtrdi 2814	. . . . . . 7 ⊢ (𝑘 = 4 → (i↑𝑘) = 1)
52	51	oveq1d 7461	. . . . . . . . . 10 ⊢ (𝑘 = 4 → ((i↑𝑘)𝑆𝐵) = (1𝑆𝐵))
53	52	oveq2d 7462	. . . . . . . . 9 ⊢ (𝑘 = 4 → (𝐴𝐺((i↑𝑘)𝑆𝐵)) = (𝐴𝐺(1𝑆𝐵)))
54	53	fveq2d 6915	. . . . . . . 8 ⊢ (𝑘 = 4 → (𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵))) = (𝑁‘(𝐴𝐺(1𝑆𝐵))))
55	54	oveq1d 7461	. . . . . . 7 ⊢ (𝑘 = 4 → ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2) = ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2))
56	51, 55	oveq12d 7464	. . . . . 6 ⊢ (𝑘 = 4 → ((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2)))
57		nnnn0 12643	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
58		expcl 14252	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (i↑𝑘) ∈ ℂ)
59	7, 57, 58	sylancr 599	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (i↑𝑘) ∈ ℂ)
60	59	adantl 487	. . . . . . 7 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (i↑𝑘) ∈ ℂ)
61	1, 2, 3, 4, 5	ipval2lem4 31341	. . . . . . . 8 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (i↑𝑘) ∈ ℂ) → ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2) ∈ ℂ)
62	59, 61	sylan2 605	. . . . . . 7 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2) ∈ ℂ)
63	60, 62	mulcld 11359	. . . . . 6 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → ((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) ∈ ℂ)
64		df-3 12436	. . . . . . 7 ⊢ 3 = (2 + 1)
65		oveq2 7454	. . . . . . . . 9 ⊢ (𝑘 = 3 → (i↑𝑘) = (i↑3))
66		i3 14377	. . . . . . . . 9 ⊢ (i↑3) = -i
67	65, 66	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑘 = 3 → (i↑𝑘) = -i)
68	67	oveq1d 7461	. . . . . . . . . . 11 ⊢ (𝑘 = 3 → ((i↑𝑘)𝑆𝐵) = ( -i𝑆𝐵))
69	68	oveq2d 7462	. . . . . . . . . 10 ⊢ (𝑘 = 3 → (𝐴𝐺((i↑𝑘)𝑆𝐵)) = (𝐴𝐺( -i𝑆𝐵)))
70	69	fveq2d 6915	. . . . . . . . 9 ⊢ (𝑘 = 3 → (𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵))) = (𝑁‘(𝐴𝐺( -i𝑆𝐵))))
71	70	oveq1d 7461	. . . . . . . 8 ⊢ (𝑘 = 3 → ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2) = ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))
72	67, 71	oveq12d 7464	. . . . . . 7 ⊢ (𝑘 = 3 → ((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))
73		df-2 12435	. . . . . . . 8 ⊢ 2 = (1 + 1)
74		oveq2 7454	. . . . . . . . . 10 ⊢ (𝑘 = 2 → (i↑𝑘) = (i↑2))
75		i2 14376	. . . . . . . . . 10 ⊢ (i↑2) = -1
76	74, 75	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑘 = 2 → (i↑𝑘) = -1)
77	76	oveq1d 7461	. . . . . . . . . . . 12 ⊢ (𝑘 = 2 → ((i↑𝑘)𝑆𝐵) = ( -1𝑆𝐵))
78	77	oveq2d 7462	. . . . . . . . . . 11 ⊢ (𝑘 = 2 → (𝐴𝐺((i↑𝑘)𝑆𝐵)) = (𝐴𝐺( -1𝑆𝐵)))
79	78	fveq2d 6915	. . . . . . . . . 10 ⊢ (𝑘 = 2 → (𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵))) = (𝑁‘(𝐴𝐺( -1𝑆𝐵))))
80	79	oveq1d 7461	. . . . . . . . 9 ⊢ (𝑘 = 2 → ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2) = ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))
81	76, 80	oveq12d 7464	. . . . . . . 8 ⊢ (𝑘 = 2 → ((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)))
82		1z 12756	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
83		oveq2 7454	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (i↑𝑘) = (i↑1))
84		exp1 14240	. . . . . . . . . . . . . 14 ⊢ (i ∈ ℂ → (i↑1) = i)
85	7, 84	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (i↑1) = i
86	83, 85	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (i↑𝑘) = i)
87	86	oveq1d 7461	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ((i↑𝑘)𝑆𝐵) = (i𝑆𝐵))
88	87	oveq2d 7462	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (𝐴𝐺((i↑𝑘)𝑆𝐵)) = (𝐴𝐺(i𝑆𝐵)))
89	88	fveq2d 6915	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → (𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵))) = (𝑁‘(𝐴𝐺(i𝑆𝐵))))
90	89	oveq1d 7461	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2) = ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2))
91	86, 90	oveq12d 7464	. . . . . . . . . . 11 ⊢ (𝑘 = 1 → ((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = (i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)))
92	91	fsum1 15945	. . . . . . . . . 10 ⊢ ((1 ∈ ℤ ∧ (i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) ∈ ℂ) → Σ𝑘 ∈ (1...1)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = (i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)))
93	82, 11, 92	sylancr 599	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → Σ𝑘 ∈ (1...1)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = (i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)))
94		1nn 12376	. . . . . . . . 9 ⊢ 1 ∈ ℕ
95	93, 94	jctil 529	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (1 ∈ ℕ ∧ Σ𝑘 ∈ (1...1)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = (i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2))))
96		eqidd 2764	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))))
97	47, 73, 81, 63, 95, 96	fsump1i 15967	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (2 ∈ ℕ ∧ Σ𝑘 ∈ (1...2)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = ((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)))))
98		eqidd 2764	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) = (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))))
99	47, 64, 72, 63, 97, 98	fsump1i 15967	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (3 ∈ ℕ ∧ Σ𝑘 ∈ (1...3)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = (((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))))
100		eqidd 2764	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) + (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2))) = ((((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) + (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2))))
101	47, 48, 56, 63, 99, 100	fsump1i 15967	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (4 ∈ ℕ ∧ Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = ((((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) + (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2)))))
102	101	simprd 501	. . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = ((((i · ((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2)) + ( -1 · ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))) + ( -i · ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) + (1 · ((𝑁‘(𝐴𝐺(1𝑆𝐵)))↑2))))
103	43, 14	subcld 11699	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) ∈ ℂ)
104	9, 18	subcld 11699	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)) ∈ ℂ)
105		mulcl 11314	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)) ∈ ℂ) → (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) ∈ ℂ)
106	7, 104, 105	sylancr 599	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) ∈ ℂ)
107	103, 106	addcomd 11542	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))) = ((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) + (((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))))
108	106, 14, 43	subadd23d 11721	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + ((𝑁‘(𝐴𝐺𝐵))↑2)) = ((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) + (((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2))))
109	107, 108	eqtr4d 2801	. . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))) = (((i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2))) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + ((𝑁‘(𝐴𝐺𝐵))↑2)))
110	46, 102, 109	3eqtr4d 2808	. . 3 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) = ((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))))
111	110	oveq1d 7461	. 2 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴𝐺((i↑𝑘)𝑆𝐵)))↑2)) / 4) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))) / 4))
112	6, 111	eqtrd 2798	1 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (((((𝑁‘(𝐴𝐺𝐵))↑2) − ((𝑁‘(𝐴𝐺( -1𝑆𝐵)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐵)))↑2) − ((𝑁‘(𝐴𝐺( -i𝑆𝐵)))↑2)))) / 4))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ‘cfv 6561 (class class class)co 7446 ℂcc 11228 1c1 11231 ici 11232 + caddc 11233 · cmul 11235 − cmin 11571 -cneg 11572 / cdiv 12003 ℕcn 12365 2c2 12427 3c3 12428 4c4 12429 ℕ₀cn0 12636 ℤcz 12723 ...cfz 13669 ↑cexp 14234 Σcsu 15885 NrmCVeccnv 31219 +_𝑣 cpv 31220 BaseSetcba 31221 ·_𝑠OLD cns 31222 norm_CVcnmcv 31225 ·_𝑖OLDcdip 31335

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-inf2 9672 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-er 8748 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-sup 9464 df-oi 9534 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-n0 12637 df-z 12724 df-uz 12996 df-rp 13151 df-fz 13670 df-fzo 13819 df-seq 14175 df-exp 14235 df-hash 14505 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-clim 15687 df-sum 15886 df-grpo 31128 df-ablo 31180 df-vc 31194 df-nv 31227 df-va 31230 df-ba 31231 df-sm 31232 df-0v 31233 df-nmcv 31235 df-dip 31336

This theorem is used by: 4ipval2 31343 ipval3 31344 ipidsq 31345 dipcj 31349 dip0r 31352

W3C validator