Theorem ipasslem11 8496

Description: Lemma for ipassi 8497. Show the inner product associative law for all complex numbers.

Hypotheses

Ref	Expression
ip1i.1	|- X = (Base` U)
ip1i.2	|- G = (+v` U)
ip1i.4	|- S = (.s` U)
ip1i.7	|- P = (.i` U)
ip1i.9	|- U e. CPreHil
ipasslem11.a	|- A e. X
ipasslem11.b	|- B e. X

Assertion

Ref	Expression
ipasslem11	|- (C e. CC -> ((CSA)PB) = (C x. (APB)))

Proof of Theorem ipasslem11

Step	Hyp	Ref	Expression
1		axcnre 5298	. 2 |- (C e. CC -> E.x e. RR E.y e. RR C = (x + (i x. y)))
2		recnt 5325	. . . . . . . 8 |- (y e. RR -> y e. CC)
3		axicn 5282	. . . . . . . . 9 |- i e. CC
4		mulcomt 5318	. . . . . . . . 9 |- ((i e. CC /\ y e. CC) -> (i x. y) = (y x. i))
5	3, 4	mpan 697	. . . . . . . 8 |- (y e. CC -> (i x. y) = (y x. i))
6	2, 5	syl 10	. . . . . . 7 |- (y e. RR -> (i x. y) = (y x. i))
7	6	adantl 390	. . . . . 6 |- ((x e. RR /\ y e. RR) -> (i x. y) = (y x. i))
8	7	opreq2d 3982	. . . . 5 |- ((x e. RR /\ y e. RR) -> (x + (i x. y)) = (x + (y x. i)))
9	8	eqeq2d 1489	. . . 4 |- ((x e. RR /\ y e. RR) -> (C = (x + (i x. y)) <-> C = (x + (y x. i))))
10		opreq1 3974	. . . . . . 7 |- (C = (x + (y x. i)) -> (CSA) = ((x + (y x. i))SA))
11	10	opreq1d 3981	. . . . . 6 |- (C = (x + (y x. i)) -> ((CSA)PB) = (((x + (y x. i))SA)PB))
12		opreq1 3974	. . . . . 6 |- (C = (x + (y x. i)) -> (C x. (APB)) = ((x + (y x. i)) x. (APB)))
13	11, 12	eqeq12d 1492	. . . . 5 |- (C = (x + (y x. i)) -> (((CSA)PB) = (C x. (APB)) <-> (((x + (y x. i))SA)PB) = ((x + (y x. i)) x. (APB))))
14		ipasslem11.a	. . . . . . . . . 10 |- A e. X
15		ip1i.9	. . . . . . . . . . . 12 |- U e. CPreHil
16	15	phnvi 8471	. . . . . . . . . . 11 |- U e. NrmCVec
17		ip1i.1	. . . . . . . . . . . 12 |- X = (Base` U)
18		ip1i.2	. . . . . . . . . . . 12 |- G = (+v` U)
19		ip1i.4	. . . . . . . . . . . 12 |- S = (.s` U)
20	17, 18, 19	nvdir 8248	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (x e. CC /\ (y x. i) e. CC /\ A e. X)) -> ((x + (y x. i))SA) = ((xSA)G((y x. i)SA)))
21	16, 20	mpan 697	. . . . . . . . . 10 |- ((x e. CC /\ (y x. i) e. CC /\ A e. X) -> ((x + (y x. i))SA) = ((xSA)G((y x. i)SA)))
22	14, 21	mp3an3 907	. . . . . . . . 9 |- ((x e. CC /\ (y x. i) e. CC) -> ((x + (y x. i))SA) = ((xSA)G((y x. i)SA)))
23		recnt 5325	. . . . . . . . 9 |- (x e. RR -> x e. CC)
24		axmulcl 5285	. . . . . . . . . . 11 |- ((y e. CC /\ i e. CC) -> (y x. i) e. CC)
25	3, 24	mpan2 698	. . . . . . . . . 10 |- (y e. CC -> (y x. i) e. CC)
26	2, 25	syl 10	. . . . . . . . 9 |- (y e. RR -> (y x. i) e. CC)
27	22, 23, 26	syl2an 456	. . . . . . . 8 |- ((x e. RR /\ y e. RR) -> ((x + (y x. i))SA) = ((xSA)G((y x. i)SA)))
28	27	opreq1d 3981	. . . . . . 7 |- ((x e. RR /\ y e. RR) -> (((x + (y x. i))SA)PB) = (((xSA)G((y x. i)SA))PB))
29		ipasslem11.b	. . . . . . . . 9 |- B e. X
30		ip1i.7	. . . . . . . . . 10 |- P = (.i` U)
31	17, 18, 19, 30, 15	ipdiri 8485	. . . . . . . . 9 |- (((xSA) e. X /\ ((y x. i)SA) e. X /\ B e. X) -> (((xSA)G((y x. i)SA))PB) = (((xSA)PB) + (((y x. i)SA)PB)))
32	29, 31	mp3an3 907	. . . . . . . 8 |- (((xSA) e. X /\ ((y x. i)SA) e. X) -> (((xSA)G((y x. i)SA))PB) = (((xSA)PB) + (((y x. i)SA)PB)))
33	17, 19	nvscl 8243	. . . . . . . . . 10 |- ((U e. NrmCVec /\ x e. CC /\ A e. X) -> (xSA) e. X)
34	16, 14, 33	mp3an13 909	. . . . . . . . 9 |- (x e. CC -> (xSA) e. X)
35	23, 34	syl 10	. . . . . . . 8 |- (x e. RR -> (xSA) e. X)
36	17, 19	nvscl 8243	. . . . . . . . . 10 |- ((U e. NrmCVec /\ (y x. i) e. CC /\ A e. X) -> ((y x. i)SA) e. X)
37	16, 14, 36	mp3an13 909	. . . . . . . . 9 |- ((y x. i) e. CC -> ((y x. i)SA) e. X)
38	26, 37	syl 10	. . . . . . . 8 |- (y e. RR -> ((y x. i)SA) e. X)
39	32, 35, 38	syl2an 456	. . . . . . 7 |- ((x e. RR /\ y e. RR) -> (((xSA)G((y x. i)SA))PB) = (((xSA)PB) + (((y x. i)SA)PB)))
40	17, 18, 19, 30, 15, 14, 29	ipasslem9 8494	. . . . . . . 8 |- (x e. RR -> ((xSA)PB) = (x x. (APB)))
41	17, 19	nvscl 8243	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ i e. CC /\ A e. X) -> (iSA) e. X)
42	16, 3, 14, 41	mp3an 918	. . . . . . . . . 10 |- (iSA) e. X
43	17, 18, 19, 30, 15, 42, 29	ipasslem9 8494	. . . . . . . . 9 |- (y e. RR -> ((yS(iSA))PB) = (y x. ((iSA)PB)))
44	17, 19	nvsass 8245	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (y e. CC /\ i e. CC /\ A e. X)) -> ((y x. i)SA) = (yS(iSA)))
45	16, 44	mpan 697	. . . . . . . . . . . 12 |- ((y e. CC /\ i e. CC /\ A e. X) -> ((y x. i)SA) = (yS(iSA)))
46	3, 14, 45	mp3an23 910	. . . . . . . . . . 11 |- (y e. CC -> ((y x. i)SA) = (yS(iSA)))
47	2, 46	syl 10	. . . . . . . . . 10 |- (y e. RR -> ((y x. i)SA) = (yS(iSA)))
48	47	opreq1d 3981	. . . . . . . . 9 |- (y e. RR -> (((y x. i)SA)PB) = ((yS(iSA))PB))
49	17, 30	ipcl 8361	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (APB) e. CC)
50	16, 14, 29, 49	mp3an 918	. . . . . . . . . . . 12 |- (APB) e. CC
51		axmulass 5290	. . . . . . . . . . . 12 |- ((y e. CC /\ i e. CC /\ (APB) e. CC) -> ((y x. i) x. (APB)) = (y x. (i x. (APB))))
52	3, 50, 51	mp3an23 910	. . . . . . . . . . 11 |- (y e. CC -> ((y x. i) x. (APB)) = (y x. (i x. (APB))))
53	2, 52	syl 10	. . . . . . . . . 10 |- (y e. RR -> ((y x. i) x. (APB)) = (y x. (i x. (APB))))
54		eqid 1478	. . . . . . . . . . . 12 |- (norm` U) = (norm` U)
55	17, 18, 19, 30, 15, 14, 29, 54	ipasslem10 8495	. . . . . . . . . . 11 |- ((iSA)PB) = (i x. (APB))
56	55	opreq2i 3978	. . . . . . . . . 10 |- (y x. ((iSA)PB)) = (y x. (i x. (APB)))
57	53, 56	syl6eqr 1528	. . . . . . . . 9 |- (y e. RR -> ((y x. i) x. (APB)) = (y x. ((iSA)PB)))
58	43, 48, 57	3eqtr4d 1520	. . . . . . . 8 |- (y e. RR -> (((y x. i)SA)PB) = ((y x. i) x. (APB)))
59	40, 58	opreqan12d 3985	. . . . . . 7 |- ((x e. RR /\ y e. RR) -> (((xSA)PB) + (((y x. i)SA)PB)) = ((x x. (APB)) + ((y x. i) x. (APB))))
60	28, 39, 59	3eqtrd 1514	. . . . . 6 |- ((x e. RR /\ y e. RR) -> (((x + (y x. i))SA)PB) = ((x x. (APB)) + ((y x. i) x. (APB))))
61		adddirt 5331	. . . . . . . 8 |- ((x e. CC /\ (y x. i) e. CC /\ (APB) e. CC) -> ((x + (y x. i)) x. (APB)) = ((x x. (APB)) + ((y x. i) x. (APB))))
62	50, 61	mp3an3 907	. . . . . . 7 |- ((x e. CC /\ (y x. i) e. CC) -> ((x + (y x. i)) x. (APB)) = ((x x. (APB)) + ((y x. i) x. (APB))))
63	62, 23, 26	syl2an 456	. . . . . 6 |- ((x e. RR /\ y e. RR) -> ((x + (y x. i)) x. (APB)) = ((x x. (APB)) + ((y x. i) x. (APB))))
64	60, 63	eqtr4d 1513	. . . . 5 |- ((x e. RR /\ y e. RR) -> (((x + (y x. i))SA)PB) = ((x + (y x. i)) x. (APB)))
65	13, 64