Theorem ipdirilem 8432

Description: Lemma for ipdiri 8433.

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
ipdiri.8	|- A e. X
ipdiri.9	|- B e. X
ipdiri.10	|- C e. X

Assertion

Ref	Expression
ipdirilem	|- ((AGB)PC) = ((APC) + (BPC))

Proof of Theorem ipdirilem

Step	Hyp	Ref	Expression
1		2cn 5935	. . . . . . 7 |- 2 e. CC
2		2ne0 5945	. . . . . . 7 |- 2 =/= 0
3	1, 2	recid 5704	. . . . . 6 |- (2 x. (1 / 2)) = 1
4	3	opreq1i 3962	. . . . 5 |- ((2 x. (1 / 2))S(AGB)) = (1S(AGB))
5		ip1i.9	. . . . . . 7 |- U e. CPreHil
6	5	phnvi 8419	. . . . . 6 |- U e. NrmCVec
7	1, 2	reccl 5690	. . . . . . 7 |- (1 / 2) e. CC
8		ipdiri.8	. . . . . . . 8 |- A e. X
9		ipdiri.9	. . . . . . . 8 |- B e. X
10		ip1i.1	. . . . . . . . 9 |- X = (Base` U)
11		ip1i.2	. . . . . . . . 9 |- G = (+v` U)
12	10, 11	nvgcl 8191	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AGB) e. X)
13	6, 8, 9, 12	mp3an 914	. . . . . . 7 |- (AGB) e. X
14	1, 7, 13	3pm3.2i 817	. . . . . 6 |- (2 e. CC /\ (1 / 2) e. CC /\ (AGB) e. X)
15		ip1i.4	. . . . . . 7 |- S = (.s` U)
16	10, 15	nvsass 8201	. . . . . 6 |- ((U e. NrmCVec /\ (2 e. CC /\ (1 / 2) e. CC /\ (AGB) e. X)) -> ((2 x. (1 / 2))S(AGB)) = (2S((1 / 2)S(AGB))))
17	6, 14, 16	mp2an 696	. . . . 5 |- ((2 x. (1 / 2))S(AGB)) = (2S((1 / 2)S(AGB)))
18	10, 15	nvsid 8200	. . . . . 6 |- ((U e. NrmCVec /\ (AGB) e. X) -> (1S(AGB)) = (AGB))
19	6, 13, 18	mp2an 696	. . . . 5 |- (1S(AGB)) = (AGB)
20	4, 17, 19	3eqtr3 1500	. . . 4 |- (2S((1 / 2)S(AGB))) = (AGB)
21	20	opreq1i 3962	. . 3 |- ((2S((1 / 2)S(AGB)))PC) = ((AGB)PC)
22		ip1i.7	. . . 4 |- P = (.i` U)
23	10, 15	nvscl 8199	. . . . 5 |- ((U e. NrmCVec /\ (1 / 2) e. CC /\ (AGB) e. X) -> ((1 / 2)S(AGB)) e. X)
24	6, 7, 13, 23	mp3an 914	. . . 4 |- ((1 / 2)S(AGB)) e. X
25		ipdiri.10	. . . 4 |- C e. X
26	10, 11, 15, 22, 5, 24, 25	ip2i 8431	. . 3 |- ((2S((1 / 2)S(AGB)))PC) = (2 x. (((1 / 2)S(AGB))PC))
27	21, 26	eqtr3 1494	. 2 |- ((AGB)PC) = (2 x. (((1 / 2)S(AGB))PC))
28		ax1cn 5249	. . . . . . 7 |- 1 e. CC
29	28	negcl 5349	. . . . . 6 |- -u1 e. CC
30	10, 15	nvscl 8199	. . . . . 6 |- ((U e. NrmCVec /\ -u1 e. CC /\ B e. X) -> (-u1SB) e. X)
31	6, 29, 9, 30	mp3an 914	. . . . 5 |- (-u1SB) e. X
32	10, 11	nvgcl 8191	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ (-u1SB) e. X) -> (AG(-u1SB)) e. X)
33	6, 8, 31, 32	mp3an 914	. . . 4 |- (AG(-u1SB)) e. X
34	10, 15	nvscl 8199	. . . 4 |- ((U e. NrmCVec /\ (1 / 2) e. CC /\ (AG(-u1SB)) e. X) -> ((1 / 2)S(AG(-u1SB))) e. X)
35	6, 7, 33, 34	mp3an 914	. . 3 |- ((1 / 2)S(AG(-u1SB))) e. X
36	10, 11, 15, 22, 5, 24, 35, 25	ip1i 8430	. 2 |- (((((1 / 2)S(AGB))G((1 / 2)S(AG(-u1SB))))PC) + ((((1 / 2)S(AGB))G(-u1S((1 / 2)S(AG(-u1SB)))))PC)) = (2 x. (((1 / 2)S(AGB))PC))
37	7, 13, 33	3pm3.2i 817	. . . . . 6 |- ((1 / 2) e. CC /\ (AGB) e. X /\ (AG(-u1SB)) e. X)
38	10, 11, 15	nvdi 8203	. . . . . 6 |- ((U e. NrmCVec /\ ((1 / 2) e. CC /\ (AGB) e. X /\ (AG(-u1SB)) e. X)) -> ((1 / 2)S((AGB)G(AG(-u1SB)))) = (((1 / 2)S(AGB))G((1 / 2)S(AG(-u1SB)))))
39	6, 37, 38	mp2an 696	. . . . 5 |- ((1 / 2)S((AGB)G(AG(-u1SB)))) = (((1 / 2)S(AGB))G((1 / 2)S(AG(-u1SB))))
40		eqid 1473	. . . . . . . . . . . 12 |- (1st` U) = (1st` U)
41	40	nvvc 8186	. . . . . . . . . . 11 |- (U e. NrmCVec -> (1st` U) e. CVec)
42	6, 41	ax-mp 7	. . . . . . . . . 10 |- (1st` U) e. CVec
43	11	vafval 8174	. . . . . . . . . . 11 |- G = (1st` (1st` U))
44	43	vcabl 8128	. . . . . . . . . 10 |- ((1st` U) e. CVec -> G e. Abel)
45	42, 44	ax-mp 7	. . . . . . . . 9 |- G e. Abel
46	8, 9	pm3.2i 285	. . . . . . . . 9 |- (A e. X /\ B e. X)
47	8, 31	pm3.2i 285	. . . . . . . . 9 |- (A e. X /\ (-u1SB) e. X)
48	10, 11	bafval 8175	. . . . . . . . . 10 |- X = ran G
49	48	abl4 8056	. . . . . . . . 9 |- ((G e. Abel /\ (A e. X /\ B e. X) /\ (A e. X /\ (-u1SB) e. X)) -> ((AGB)G(AG(-u1SB))) = ((AGA)G(BG(-u1SB))))
50	45, 46, 47, 49	mp3an 914	. . . . . . . 8 |- ((AGB)G(AG(-u1SB))) = ((AGA)G(BG(-u1SB)))
51	15	smfval 8176	. . . . . . . . . . 11 |- S = (2nd` (1st` U))
52	43, 51, 48	vc2 8126	. . . . . . . . . 10 |- (((1st` U) e. CVec /\ A e. X) -> (AGA) = (2SA))
53	42, 8, 52	mp2an 696	. . . . . . . . 9 |- (AGA) = (2SA)
54		eqid 1473	. . . . . . . . . . 11 |- (0v` U) = (0v` U)
55	10, 11, 15, 54	nvrinv 8225	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X) -> (BG(-u1SB)) = (0v` U))
56	6, 9, 55	mp2an 696	. . . . . . . . 9 |- (BG(-u1SB)) = (0v` U)
57	53, 56	opreq12i 3964	. . . . . . . 8 |- ((AGA)G(BG(-u1SB))) = ((2SA)G(0v` U))
58	10, 15	nvscl 8199	. . . . . . . . . 10 |- ((U e. NrmCVec /\ 2 e. CC /\ A e. X) -> (2SA) e. X)
59	6, 1, 8, 58	mp3an 914	. . . . . . . . 9 |- (2SA) e. X
60	10, 11, 54	nv0rid 8208	. . . . . . . . 9 |- ((U e. NrmCVec /\ (2SA) e. X) -> ((2SA)G(0v` U)) = (2SA))
61	6, 59, 60	mp2an 696	. . . . . . . 8 |- ((2SA)G(0v` U)) = (2SA)
62	50, 57, 61	3eqtr 1496	. . . . . . 7 |- ((AGB)G(AG(-u1SB))) = (2SA)
63	62	opreq2i 3963	. . . . . 6 |- ((1 / 2)S((AGB)G(AG(-u1SB)))) = ((1 / 2)S(2SA))
64	7, 1, 8	3pm3.2i 817	. . . . . . 7 |- ((1 / 2) e. CC /\ 2 e. CC /\ A e. X)
65	10, 15	nvsass 8201	. . . . . . 7 |- ((U e. NrmCVec /\ ((1 / 2) e. CC /\ 2 e. CC /\ A e. X)) -> (((1 / 2) x. 2)SA) = ((1 / 2)S(2SA)))
66	6, 64, 65	mp2an 696	. . . . . 6 |- (((1 / 2) x. 2)SA) = ((1 / 2)S(2SA))
67	1, 28, 2	divcan1 5694	. . . . . . . 8 |- ((1 / 2) x. 2) = 1
68	67	opreq1i 3962	. . . . . . 7 |- (((1 / 2) x. 2)SA) = (1SA)
69	10, 15	nvsid 8200	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> (1SA) = A)
70	6, 8, 69	mp2an 696	. . . . . . 7 |- (1SA) = A
71	68, 70	eqtr 1492	. . . . . 6 |- (((1 / 2) x. 2)SA) = A
72	63, 66, 71	3eqtr2 1498	. . . . 5 |- ((1 / 2)S((AGB)G(AG(-u1SB)))) = A
73	39, 72	eqtr3 1494	. . . 4 |- (((1 / 2)S(AGB))G((1 / 2)S(AG(-u1SB)))) = A
74	73	opreq1i 3962	. . 3 |- ((((1 / 2)S(AGB))G((1 / 2)S(AG(-u1SB))))PC) = (APC)
75	10, 15	nvscl 8199	. . . . . . . . 9 |- ((U e. NrmCVec /\ -u1 e. CC /\ A e. X) -> (-u1SA) e. X)
76	6, 29, 8, 75	mp3an 914	. . . . . . . 8 |- (-u1SA) e. X
77	10, 11	nvgcl 8191	. . . . . . . 8 |- ((U e. NrmCVec /\ (-u1SA) e. X /\ B e. X) -> ((-u1SA)GB) e. X)
78	6, 76, 9, 77	mp3an 914	. . . . . . 7 |- ((-u1SA)GB) e. X
79	7, 13, 78	3pm3.2i 817	. . . . . 6 |- ((1 / 2) e. CC /\ (AGB) e. X /\ ((-u1SA)GB) e. X)
80	10, 11, 15	nvdi 8203	. . . . . 6 |- ((U e. NrmCVec /\ ((1 / 2) e. CC /\ (AGB) e. X /\ ((-u1SA)GB) e. X)) -> ((1 / 2)S((AGB)G