Theorem ipval2 8353

Description: Expansion of the inner product value ipval 8349. Warning: The HTML proof page is 0.5MB in size.

Hypotheses

Ref	Expression
ipfval.1	|- X = (Base` U)
ipfval.2	|- G = (+v` U)
ipfval.4	|- S = (.s` U)
ipfval.6	|- N = (norm` U)
ipfval.7	|- P = (.i` U)

Assertion

Ref	Expression
ipval2	|- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) = (((((N` (AGB))^2) - ((N` (AG(-u1SB)))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2)))) / 4))

Proof of Theorem ipval2

Step	Hyp	Ref	Expression
1		ipfval.1	. . 3 |- X = (Base` U)
2		ipfval.2	. . 3 |- G = (+v` U)
3		ipfval.4	. . 3 |- S = (.s` U)
4		ipfval.6	. . 3 |- N = (norm` U)
5		ipfval.7	. . 3 |- P = (.i` U)
6	1, 2, 3, 4, 5	ipval 8349	. 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) = (sum_k e. (1...4)((i^k) x. ((N` (AG((i^k)SB)))^2)) / 4))
7		negsubt 5394	. . . . . . 7 |- ((((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)) e. CC /\ (i x. ((N` (AG(-uiSB)))^2)) e. CC) -> (((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)) + -u(i x. ((N` (AG(-uiSB)))^2))) = (((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)) - (i x. ((N` (AG(-uiSB)))^2))))
8		subclt 5379	. . . . . . . 8 |- (((i x. ((N` (AG(iSB)))^2)) e. CC /\ ((N` (AG(-u1SB)))^2) e. CC) -> ((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)) e. CC)
9		axicn 5282	. . . . . . . . . 10 |- i e. CC
10	1, 2, 3, 4, 5	ipval2lem4 8352	. . . . . . . . . 10 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ i e. CC) -> ((N` (AG(iSB)))^2) e. CC)
11	9, 10	mpan2 698	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(iSB)))^2) e. CC)
12		axmulcl 5285	. . . . . . . . . 10 |- ((i e. CC /\ ((N` (AG(iSB)))^2) e. CC) -> (i x. ((N` (AG(iSB)))^2)) e. CC)
13	9, 12	mpan 697	. . . . . . . . 9 |- (((N` (AG(iSB)))^2) e. CC -> (i x. ((N` (AG(iSB)))^2)) e. CC)
14	11, 13	syl 10	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (i x. ((N` (AG(iSB)))^2)) e. CC)
15		ax1cn 5281	. . . . . . . . . 10 |- 1 e. CC
16	15	negcl 5381	. . . . . . . . 9 |- -u1 e. CC
17	1, 2, 3, 4, 5	ipval2lem4 8352	. . . . . . . . 9 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ -u1 e. CC) -> ((N` (AG(-u1SB)))^2) e. CC)
18	16, 17	mpan2 698	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(-u1SB)))^2) e. CC)
19	8, 14, 18	sylanc 473	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)) e. CC)
20	9	negcl 5381	. . . . . . . . 9 |- -ui e. CC
21	1, 2, 3, 4, 5	ipval2lem4 8352	. . . . . . . . 9 |- (((U e. NrmCVec /\ A e. X /\ B e. X) /\ -ui e. CC) -> ((N` (AG(-uiSB)))^2) e. CC)
22	20, 21	mpan2 698	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(-uiSB)))^2) e. CC)
23		axmulcl 5285	. . . . . . . . 9 |- ((i e. CC /\ ((N` (AG(-uiSB)))^2) e. CC) -> (i x. ((N` (AG(-uiSB)))^2)) e. CC)
24	9, 23	mpan 697	. . . . . . . 8 |- (((N` (AG(-uiSB)))^2) e. CC -> (i x. ((N` (AG(-uiSB)))^2)) e. CC)
25	22, 24	syl 10	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (i x. ((N` (AG(-uiSB)))^2)) e. CC)
26	7, 19, 25	sylanc 473	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)) + -u(i x. ((N` (AG(-uiSB)))^2))) = (((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)) - (i x. ((N` (AG(-uiSB)))^2))))
27		mulm1t 5483	. . . . . . . . . 10 |- (((N` (AG(-u1SB)))^2) e. CC -> (-u1 x. ((N` (AG(-u1SB)))^2)) = -u((N` (AG(-u1SB)))^2))
28	18, 27	syl 10	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-u1 x. ((N` (AG(-u1SB)))^2)) = -u((N` (AG(-u1SB)))^2))
29	28	opreq2d 3982	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((i x. ((N` (AG(iSB)))^2)) + (-u1 x. ((N` (AG(-u1SB)))^2))) = ((i x. ((N` (AG(iSB)))^2)) + -u((N` (AG(-u1SB)))^2)))
30		negsubt 5394	. . . . . . . . 9 |- (((i x. ((N` (AG(iSB)))^2)) e. CC /\ ((N` (AG(-u1SB)))^2) e. CC) -> ((i x. ((N` (AG(iSB)))^2)) + -u((N` (AG(-u1SB)))^2)) = ((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)))
31	30, 14, 18	sylanc 473	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((i x. ((N` (AG(iSB)))^2)) + -u((N` (AG(-u1SB)))^2)) = ((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)))
32	29, 31	eqtrd 1510	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((i x. ((N` (AG(iSB)))^2)) + (-u1 x. ((N` (AG(-u1SB)))^2))) = ((i x. ((N` (AG(iSB)))^2)) - ((N` (AG(-u1SB)))^2)))
33		mulneg1t 5463	. . . . . . . . 9 |- ((i e. CC /\ ((N` (AG(-uiSB)))^2) e. CC) -> (-ui x. ((N` (AG(-uiSB)))^2)) = -u(i x. ((N` (AG(-uiSB)))^2)))
34	9, 33	mpan 697	. . . . . . . 8 |- (((N` (AG(-uiSB)))^2) e. CC -> (-ui x. ((N` (AG(-uiSB)))^2)) = -u(i x. ((N` (AG(-uiSB)))^2)))
35	22, 34	syl 10	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-ui x. ((N` (AG(-uiSB)))^2)) = -u(i x. ((N` (AG(-uiSB)))^2)))
36	32, 35	opreq12d 3984	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((i x. ((N` (AG(iSB)))^2)) + (-u1 x. ((N` (AG(-u1SB)))^