Theorem 4ipval2 8354

Description: Four times the inner product value ipval3 8355, useful for simplifying certain proofs.

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

Proof of Theorem 4ipval2

Step	Hyp	Ref	Expression
1		ipfval.1	. . . 4 |- X = (Base` U)
2		ipfval.2	. . . 4 |- G = (+v` U)
3		ipfval.4	. . . 4 |- S = (.s` U)
4		ipfval.6	. . . 4 |- N = (norm` U)
5		ipfval.7	. . . 4 |- P = (.i` U)
6	1, 2, 3, 4, 5	ipval2 8353	. . 3 |- ((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))
7	6	opreq2d 3982	. 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (4 x. (APB)) = (4 x. (((((N` (AGB))^2) - ((N` (AG(-u1SB)))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2)))) / 4)))
8		axaddcl 5283	. . . 4 |- (((((N` (AGB))^2) - ((N` (AG(-u1SB)))^2)) e. CC /\ (i x. (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2))) e. CC) -> ((((N` (AGB))^2) - ((N` (AG(-u1SB)))^2)) + (i x. (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2)))) e. CC)
9		subclt 5379	. . . . 5 |- ((((N` (AGB))^2) e. CC /\ ((N` (AG(-u1SB)))^2) e. CC) -> (((N` (AGB))^2) - ((N` (AG(-u1SB)))^2)) e. CC)
10	1, 4	nvcl 8283	. . . . . . . 8 |- ((U e. NrmCVec /\ (AGB) e. X) -> (N` (AGB)) e. RR)
11		3simp1 790	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> U e. NrmCVec)
12	1, 2	nvgcl 8235	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AGB) e. X)
13	10, 11, 12	sylanc 473	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AGB)) e. RR)
14	13	recnd 5327	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AGB)) e. CC)
15		sqclt 6612	. . . . . 6 |- ((N` (AGB)) e. CC -> ((N` (AGB))^2) e. CC)
16	14, 15	syl 10	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AGB))^2) e. CC)
17	1, 4	nvcl 8283	. . . . . . . 8 |- ((U e. NrmCVec /\ (AG(-u1SB)) e. X) -> (N` (AG(-u1SB))) e. RR)
18	1, 2	nvgcl 8235	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ (-u1SB) e. X) -> (AG(-u1SB)) e. X)
19		ax1cn 5281	. . . . . . . . . . . 12 |- 1 e. CC
20	19	negcl 5381	. . . . . . . . . . 11 |- -u1 e. CC
21	1, 3	nvscl 8243	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ -u1 e. CC /\ B e. X) -> (-u1SB) e. X)
22	20, 21	mp3an2 906	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X) -> (-u1SB) e. X)
23	22	3adant2 800	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-u1SB) e. X)
24	18, 23	syld3an3 872	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(-u1SB)) e. X)
25	17, 11, 24	sylanc 473	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(-u1SB))) e. RR)
26	25	recnd 5327	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(-u1SB))) e. CC)
27		sqclt 6612	. . . . . 6 |- ((N` (AG(-u1SB))) e. CC -> ((N` (AG(-u1SB)))^2) e. CC)
28	26, 27	syl 10	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(-u1SB)))^2) e. CC)
29	9, 16, 28	sylanc 473	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((N` (AGB))^2) - ((N` (AG(-u1SB)))^2)) e. CC)
30		subclt 5379	. . . . . 6 |- ((((N` (AG(iSB)))^2) e. CC /\ ((N` (AG(-uiSB)))^2) e. CC) -> (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2)) e. CC)
31	1, 4	nvcl 8283	. . . . . . . . 9 |- ((U e. NrmCVec /\ (AG(iSB)) e. X) -> (N` (AG(iSB))) e. RR)
32	1, 2	nvgcl 8235	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ (iSB) e. X) -> (AG(iSB)) e. X)
33		axicn 5282	. . . . . . . . . . . 12 |- i e. CC
34	1, 3	nvscl 8243	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ i e. CC /\ B e. X) -> (iSB) e. X)
35	33, 34	mp3an2 906	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X) -> (iSB) e. X)
36	35	3adant2 800	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (iSB) e. X)
37	32, 36	syld3an3 872	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(iSB)) e. X)
38	31, 11, 37	sylanc 473	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(iSB))) e. RR)
39	38	recnd 5327	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(iSB))) e. CC)
40		sqclt 6612	. . . . . . 7 |- ((N` (AG(iSB))) e. CC -> ((N` (AG(iSB)))^2) e. CC)
41	39, 40	syl 10	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(iSB)))^2) e. CC)
42	1, 4	nvcl 8283	. . . . . . . . 9 |- ((U e. NrmCVec /\ (AG(-uiSB)) e. X) -> (N` (AG(-uiSB))) e. RR)
43	1, 2	nvgcl 8235	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ (-uiSB) e. X) -> (AG(-uiSB)) e. X)
44	33	negcl 5381	. . . . . . . . . . . 12 |- -ui e. CC
45	1, 3	nvscl 8243	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ -ui e. CC /\ B e. X) -> (-uiSB) e. X)
46	44, 45	mp3an2 906	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ B e. X) -> (-uiSB) e. X)
47	46	3adant2 800	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-uiSB) e. X)
48	43, 47	syld3an3 872	. . . . . . . . 9 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(-uiSB)) e. X)
49	42, 11, 48	sylanc 473	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(-uiSB))) e. RR)
50	49	recnd 5327	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(-uiSB))) e. CC)
51		sqclt 6612	. . . . . . 7 |- ((N` (AG(-uiSB))) e. CC -> ((N` (AG(-uiSB)))^2) e. CC)
52	50, 51	syl 10	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((N` (AG(-uiSB)))^2) e. CC)
53	30, 41, 52	sylanc 473	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2)) e. CC)
54		axmulcl 5285	. . . . . 6 |- ((i e. CC /\ (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2)) e. CC) -> (i x. (((N` (AG(iSB)))^2) - ((N` (AG(-uiSB)))^2))) e. CC)
55	33, 54	mpan 697	. . . . 5 |- (((