Theorem ipdirilem 29545

Description: Lemma for ipdiri 29546. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ip1i.1	⊢ 𝑋 = (BaseSet‘𝑈)
ip1i.2	⊢ 𝐺 = ( +𝑣 ‘𝑈)
ip1i.4	⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)
ip1i.7	⊢ 𝑃 = (·𝑖OLD‘𝑈)
ip1i.9	⊢ 𝑈 ∈ CPreHilOLD
ipdiri.8	⊢ 𝐴 ∈ 𝑋
ipdiri.9	⊢ 𝐵 ∈ 𝑋
ipdiri.10	⊢ 𝐶 ∈ 𝑋

Assertion

Ref	Expression
ipdirilem	⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))

Proof of Theorem ipdirilem

Step	Hyp	Ref	Expression
1		2cn 12158	. . . . . . 7 ⊢ 2 ∈ ℂ
2		2ne0 12187	. . . . . . 7 ⊢ 2 ≠ 0
3	1, 2	recidi 11816	. . . . . 6 ⊢ (2 · (1 / 2)) = 1
4	3	oveq1i 7356	. . . . 5 ⊢ ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (1𝑆(𝐴𝐺𝐵))
5		ip1i.9	. . . . . . 7 ⊢ 𝑈 ∈ CPreHilOLD
6	5	phnvi 29532	. . . . . 6 ⊢ 𝑈 ∈ NrmCVec
7		halfcn 12298	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
8		ipdiri.8	. . . . . . . 8 ⊢ 𝐴 ∈ 𝑋
9		ipdiri.9	. . . . . . . 8 ⊢ 𝐵 ∈ 𝑋
10		ip1i.1	. . . . . . . . 9 ⊢ 𝑋 = (BaseSet‘𝑈)
11		ip1i.2	. . . . . . . . 9 ⊢ 𝐺 = ( +𝑣 ‘𝑈)
12	10, 11	nvgcl 29336	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
13	6, 8, 9, 12	mp3an 1461	. . . . . . 7 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
14	1, 7, 13	3pm3.2i 1339	. . . . . 6 ⊢ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋)
15		ip1i.4	. . . . . . 7 ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈)
16	10, 15	nvsass 29344	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋)) → ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵))))
17	6, 14, 16	mp2an 690	. . . . 5 ⊢ ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))
18	10, 15	nvsid 29343	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋) → (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵))
19	6, 13, 18	mp2an 690	. . . . 5 ⊢ (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵)
20	4, 17, 19	3eqtr3i 2773	. . . 4 ⊢ (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵))) = (𝐴𝐺𝐵)
21	20	oveq1i 7356	. . 3 ⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = ((𝐴𝐺𝐵)𝑃𝐶)
22		ip1i.7	. . . 4 ⊢ 𝑃 = (·𝑖OLD‘𝑈)
23	10, 15	nvscl 29342	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋) → ((1 / 2)𝑆(𝐴𝐺𝐵)) ∈ 𝑋)
24	6, 7, 13, 23	mp3an 1461	. . . 4 ⊢ ((1 / 2)𝑆(𝐴𝐺𝐵)) ∈ 𝑋
25		ipdiri.10	. . . 4 ⊢ 𝐶 ∈ 𝑋
26	10, 11, 15, 22, 5, 24, 25	ip2i 29544	. . 3 ⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
27	21, 26	eqtr3i 2767	. 2 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
28		neg1cn 12197	. . . . . 6 ⊢ -1 ∈ ℂ
29	10, 15	nvscl 29342	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (-1𝑆𝐵) ∈ 𝑋)
30	6, 28, 9, 29	mp3an 1461	. . . . 5 ⊢ (-1𝑆𝐵) ∈ 𝑋
31	10, 11	nvgcl 29336	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
32	6, 8, 30, 31	mp3an 1461	. . . 4 ⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
33	10, 15	nvscl 29342	. . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋) → ((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))) ∈ 𝑋)
34	6, 7, 32, 33	mp3an 1461	. . 3 ⊢ ((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))) ∈ 𝑋
35	10, 11, 15, 22, 5, 24, 34, 25	ip1i 29543	. 2 ⊢ (((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
36		eqid 2737	. . . . . . . . . . . 12 ⊢ (1st ‘𝑈) = (1st ‘𝑈)
37	36	nvvc 29331	. . . . . . . . . . 11 ⊢ (𝑈 ∈ NrmCVec → (1st ‘𝑈) ∈ CVecOLD)
38	6, 37	ax-mp 5	. . . . . . . . . 10 ⊢ (1st ‘𝑈) ∈ CVecOLD
39	11	vafval 29319	. . . . . . . . . . 11 ⊢ 𝐺 = (1st ‘(1st ‘𝑈))
40	39	vcablo 29285	. . . . . . . . . 10 ⊢ ((1st ‘𝑈) ∈ CVecOLD → 𝐺 ∈ AbelOp)
41	38, 40	ax-mp 5	. . . . . . . . 9 ⊢ 𝐺 ∈ AbelOp
42	8, 9	pm3.2i 472	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)
43	8, 30	pm3.2i 472	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)
44	10, 11	bafval 29320	. . . . . . . . . 10 ⊢ 𝑋 = ran 𝐺
45	44	ablo4 29266	. . . . . . . . 9 ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))))
46	41, 42, 43, 45	mp3an 1461	. . . . . . . 8 ⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵)))
47	15	smfval 29321	. . . . . . . . . . 11 ⊢ 𝑆 = (2nd ‘(1st ‘𝑈))
48	39, 47, 44	vc2OLD 29284	. . . . . . . . . 10 ⊢ (((1st ‘𝑈) ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴))
49	38, 8, 48	mp2an 690	. . . . . . . . 9 ⊢ (𝐴𝐺𝐴) = (2𝑆𝐴)
50		eqid 2737	. . . . . . . . . . 11 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
51	10, 11, 15, 50	nvrinv 29367	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺(-1𝑆𝐵)) = (0vec‘𝑈))
52	6, 9, 51	mp2an 690	. . . . . . . . 9 ⊢ (𝐵𝐺(-1𝑆𝐵)) = (0vec‘𝑈)
53	49, 52	oveq12i 7358	. . . . . . . 8 ⊢ ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))) = ((2𝑆𝐴)𝐺(0vec‘𝑈))
54	10, 15	nvscl 29342	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (2𝑆𝐴) ∈ 𝑋)
55	6, 1, 8, 54	mp3an 1461	. . . . . . . . 9 ⊢ (2𝑆𝐴) ∈ 𝑋
56	10, 11, 50	nv0rid 29351	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (2𝑆𝐴) ∈ 𝑋) → ((2𝑆𝐴)𝐺(0vec‘𝑈)) = (2𝑆𝐴))
57	6, 55, 56	mp2an 690	. . . . . . . 8 ⊢ ((2𝑆𝐴)𝐺(0vec‘𝑈)) = (2𝑆𝐴)
58	46, 53, 57	3eqtri 2769	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = (2𝑆𝐴)
59	58	oveq2i 7357	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆(2𝑆𝐴))
60	7, 1, 8	3pm3.2i 1339	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋)
61	10, 15	nvsass 29344	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋)) → (((1 / 2) · 2)𝑆𝐴) = ((1 / 2)𝑆(2𝑆𝐴)))
62	6, 60, 61	mp2an 690	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐴) = ((1 / 2)𝑆(2𝑆𝐴))
63	59, 62	eqtr4i 2768	. . . . 5 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2) · 2)𝑆𝐴)
64	7, 13, 32	3pm3.2i 1339	. . . . . 6 ⊢ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
65	10, 11, 15	nvdi 29346	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))
66	6, 64, 65	mp2an 690	. . . . 5 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))
67		ax-1cn 11039	. . . . . . . 8 ⊢ 1 ∈ ℂ
68	67, 1, 2	divcan1i 11829	. . . . . . 7 ⊢ ((1 / 2) · 2) = 1
69	68	oveq1i 7356	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐴) = (1𝑆𝐴)
70	10, 15	nvsid 29343	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
71	6, 8, 70	mp2an 690	. . . . . 6 ⊢ (1𝑆𝐴) = 𝐴
72	69, 71	eqtri 2765	. . . . 5 ⊢ (((1 / 2) · 2)𝑆𝐴) = 𝐴
73	63, 66, 72	3eqtr3i 2773	. . . 4 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) = 𝐴
74	73	oveq1i 7356	. . 3 ⊢ ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) = (𝐴𝑃𝐶)
75	28, 7	mulcomi 11093	. . . . . . . . 9 ⊢ (-1 · (1 / 2)) = ((1 / 2) · -1)
76	75	oveq1i 7356	. . . . . . . 8 ⊢ ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵)))
77	28, 7, 32	3pm3.2i 1339	. . . . . . . . 9 ⊢ (-1 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
78	10, 15	nvsass 29344	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))
79	6, 77, 78	mp2an 690	. . . . . . . 8 ⊢ ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))
80	7, 28, 32	3pm3.2i 1339	. . . . . . . . . 10 ⊢ ((1 / 2) ∈ ℂ ∧ -1 ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
81	10, 15	nvsass 29344	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ -1 ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵)))))
82	6, 80, 81	mp2an 690	. . . . . . . . 9 ⊢ (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵))))
83	28, 8, 30	3pm3.2i 1339	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)
84	10, 11, 15	nvdi 29346	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))))
85	6, 83, 84	mp2an 690	. . . . . . . . . . 11 ⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵)))
86		neg1mulneg1e1 12296	. . . . . . . . . . . . . 14 ⊢ (-1 · -1) = 1
87	86	oveq1i 7356	. . . . . . . . . . . . 13 ⊢ ((-1 · -1)𝑆𝐵) = (1𝑆𝐵)
88	28, 28, 9	3pm3.2i 1339	. . . . . . . . . . . . . 14 ⊢ (-1 ∈ ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋)
89	10, 15	nvsass 29344	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → ((-1 · -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵)))
90	6, 88, 89	mp2an 690	. . . . . . . . . . . . 13 ⊢ ((-1 · -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵))
91	10, 15	nvsid 29343	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵)
92	6, 9, 91	mp2an 690	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐵) = 𝐵
93	87, 90, 92	3eqtr3i 2773	. . . . . . . . . . . 12 ⊢ (-1𝑆(-1𝑆𝐵)) = 𝐵
94	93	oveq2i 7357	. . . . . . . . . . 11 ⊢ ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵)
95	85, 94	eqtri 2765	. . . . . . . . . 10 ⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵)
96	95	oveq2i 7357	. . . . . . . . 9 ⊢ ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))
97	82, 96	eqtri 2765	. . . . . . . 8 ⊢ (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))
98	76, 79, 97	3eqtr3i 2773	. . . . . . 7 ⊢ (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))
99	98	oveq2i 7357	. . . . . 6 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)))
100	10, 15	nvscl 29342	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (-1𝑆𝐴) ∈ 𝑋)
101	6, 28, 8, 100	mp3an 1461	. . . . . . . . 9 ⊢ (-1𝑆𝐴) ∈ 𝑋
102	10, 11	nvgcl 29336	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)
103	6, 101, 9, 102	mp3an 1461	. . . . . . . 8 ⊢ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋
104	7, 13, 103	3pm3.2i 1339	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)
105	10, 11, 15	nvdi 29346	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)) → ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))))
106	6, 104, 105	mp2an 690	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)))
107	99, 106	eqtr4i 2768	. . . . 5 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)))
108	101, 9	pm3.2i 472	. . . . . . . . 9 ⊢ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)
109	44	ablo4 29266	. . . . . . . . 9 ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)))
110	41, 42, 108, 109	mp3an 1461	. . . . . . . 8 ⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵))
111	10, 11, 15, 50	nvrinv 29367	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐴)) = (0vec‘𝑈))
112	6, 8, 111	mp2an 690	. . . . . . . . . 10 ⊢ (𝐴𝐺(-1𝑆𝐴)) = (0vec‘𝑈)
113	112	oveq1i 7356	. . . . . . . . 9 ⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = ((0vec‘𝑈)𝐺(𝐵𝐺𝐵))
114	10, 11	nvgcl 29336	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) ∈ 𝑋)
115	6, 9, 9, 114	mp3an 1461	. . . . . . . . . 10 ⊢ (𝐵𝐺𝐵) ∈ 𝑋
116	10, 11, 50	nv0lid 29352	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐵𝐺𝐵) ∈ 𝑋) → ((0vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵))
117	6, 115, 116	mp2an 690	. . . . . . . . 9 ⊢ ((0vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵)
118	113, 117	eqtri 2765	. . . . . . . 8 ⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵)
119	39, 47, 44	vc2OLD 29284	. . . . . . . . 9 ⊢ (((1st ‘𝑈) ∈ CVecOLD ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) = (2𝑆𝐵))
120	38, 9, 119	mp2an 690	. . . . . . . 8 ⊢ (𝐵𝐺𝐵) = (2𝑆𝐵)
121	110, 118, 120	3eqtri 2769	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = (2𝑆𝐵)
122	121	oveq2i 7357	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = ((1 / 2)𝑆(2𝑆𝐵))
123	7, 1, 9	3pm3.2i 1339	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋)
124	10, 15	nvsass 29344	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → (((1 / 2) · 2)𝑆𝐵) = ((1 / 2)𝑆(2𝑆𝐵)))
125	6, 123, 124	mp2an 690	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐵) = ((1 / 2)𝑆(2𝑆𝐵))
126	68	oveq1i 7356	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐵) = (1𝑆𝐵)
127	122, 125, 126	3eqtr2i 2771	. . . . 5 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (1𝑆𝐵)
128	107, 127, 92	3eqtri 2769	. . . 4 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = 𝐵
129	128	oveq1i 7356	. . 3 ⊢ ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶) = (𝐵𝑃𝐶)
130	74, 129	oveq12i 7358	. 2 ⊢ (((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))
131	27, 35, 130	3eqtr2i 2771	1 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))

Syntax hints:   ∧ wa 397   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ‘cfv 6488  (class class class)co 7346  1^st c1st 7906  ℂcc 10979  1c1 10982   + caddc 10984   · cmul 10986  -cneg 11316   / cdiv 11742  2c2 12138  AbelOpcablo 29260  CVec_OLDcvc 29274  NrmCVeccnv 29300   +_𝑣 cpv 29301  BaseSetcba 29302   ·_𝑠OLD cns 29303  0_veccn0v 29304  ·_𝑖OLDcdip 29416  CPreHil_OLDccphlo 29528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5237  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659  ax-inf2 9507  ax-cnex 11037  ax-resscn 11038  ax-1cn 11039  ax-icn 11040  ax-addcl 11041  ax-addrcl 11042  ax-mulcl 11043  ax-mulrcl 11044  ax-mulcom 11045  ax-addass 11046  ax-mulass 11047  ax-distr 11048  ax-i2m1 11049  ax-1ne0 11050  ax-1rid 11051  ax-rnegex 11052  ax-rrecex 11053  ax-cnre 11054  ax-pre-lttri 11055  ax-pre-lttrn 11056  ax-pre-ltadd 11057  ax-pre-mulgt0 11058  ax-pre-sup 11059

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-int 4903  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5184  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-se 5583  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7302  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7790  df-1st 7908  df-2nd 7909  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-1o 8376  df-er 8578  df-en 8814  df-dom 8815  df-sdom 8816  df-fin 8817  df-sup 9308  df-oi 9376  df-card 9805  df-pnf 11121  df-mnf 11122  df-xr 11123  df-ltxr 11124  df-le 11125  df-sub 11317  df-neg 11318  df-div 11743  df-nn 12084  df-2 12146  df-3 12147  df-4 12148  df-n0 12344  df-z 12430  df-uz 12693  df-rp 12841  df-fz 13350  df-fzo 13493  df-seq 13832  df-exp 13893  df-hash 14155  df-cj 14914  df-re 14915  df-im 14916  df-sqrt 15050  df-abs 15051  df-clim 15301  df-sum 15502  df-grpo 29209  df-gid 29210  df-ginv 29211  df-ablo 29261  df-vc 29275  df-nv 29308  df-va 29311  df-ba 29312  df-sm 29313  df-0v 29314  df-nmcv 29316  df-dip 29417  df-ph 29529

This theorem is referenced by:  ipdiri  29546