ipdirilem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ipdirilem		Structured version Visualization version GIF version

Theorem ipdirilem 30765

Description: Lemma for ipdiri 30766. (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	⊢ 𝑈 ∈ CPreHil_OLD
ipdiri.8	⊢ 𝐴 ∈ 𝑋
ipdiri.9	⊢ 𝐵 ∈ 𝑋
ipdiri.10	⊢ 𝐶 ∈ 𝑋

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

**Proof of Theorem ipdirilem**
Step	Hyp	Ref	Expression
1		2cn 12268	. . . . . . 7 ⊢ 2 ∈ ℂ
2		2ne0 12297	. . . . . . 7 ⊢ 2 ≠ 0
3	1, 2	recidi 11920	. . . . . 6 ⊢ (2 · (1 / 2)) = 1
4	3	oveq1i 7400	. . . . 5 ⊢ ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (1𝑆(𝐴𝐺𝐵))
5		ip1i.9	. . . . . . 7 ⊢ 𝑈 ∈ CPreHil_OLD
6	5	phnvi 30752	. . . . . 6 ⊢ 𝑈 ∈ NrmCVec
7		halfcn 12403	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
8		ipdiri.8	. . . . . . . 8 ⊢ 𝐴 ∈ 𝑋
9		ipdiri.9	. . . . . . . 8 ⊢ 𝐵 ∈ 𝑋
10		ip1i.1	. . . . . . . . 9 ⊢ 𝑋 = (BaseSet‘𝑈)
11		ip1i.2	. . . . . . . . 9 ⊢ 𝐺 = ( +_𝑣 ‘𝑈)
12	10, 11	nvgcl 30556	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
13	6, 8, 9, 12	mp3an 1463	. . . . . . 7 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
14	1, 7, 13	3pm3.2i 1340	. . . . . 6 ⊢ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋)
15		ip1i.4	. . . . . . 7 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
16	10, 15	nvsass 30564	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋)) → ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵))))
17	6, 14, 16	mp2an 692	. . . . 5 ⊢ ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))
18	10, 15	nvsid 30563	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋) → (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵))
19	6, 13, 18	mp2an 692	. . . . 5 ⊢ (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵)
20	4, 17, 19	3eqtr3i 2761	. . . 4 ⊢ (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵))) = (𝐴𝐺𝐵)
21	20	oveq1i 7400	. . 3 ⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = ((𝐴𝐺𝐵)𝑃𝐶)
22		ip1i.7	. . . 4 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
23	10, 15	nvscl 30562	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋) → ((1 / 2)𝑆(𝐴𝐺𝐵)) ∈ 𝑋)
24	6, 7, 13, 23	mp3an 1463	. . . 4 ⊢ ((1 / 2)𝑆(𝐴𝐺𝐵)) ∈ 𝑋
25		ipdiri.10	. . . 4 ⊢ 𝐶 ∈ 𝑋
26	10, 11, 15, 22, 5, 24, 25	ip2i 30764	. . 3 ⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
27	21, 26	eqtr3i 2755	. 2 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
28		neg1cn 12178	. . . . . 6 ⊢ -1 ∈ ℂ
29	10, 15	nvscl 30562	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (-1𝑆𝐵) ∈ 𝑋)
30	6, 28, 9, 29	mp3an 1463	. . . . 5 ⊢ (-1𝑆𝐵) ∈ 𝑋
31	10, 11	nvgcl 30556	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
32	6, 8, 30, 31	mp3an 1463	. . . 4 ⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
33	10, 15	nvscl 30562	. . . 4 ⊢ ((𝑈 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋) → ((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))) ∈ 𝑋)
34	6, 7, 32, 33	mp3an 1463	. . 3 ⊢ ((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))) ∈ 𝑋
35	10, 11, 15, 22, 5, 24, 34, 25	ip1i 30763	. 2 ⊢ (((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
36		eqid 2730	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑈) = (1^st ‘𝑈)
37	36	nvvc 30551	. . . . . . . . . . 11 ⊢ (𝑈 ∈ NrmCVec → (1^st ‘𝑈) ∈ CVec_OLD)
38	6, 37	ax-mp 5	. . . . . . . . . 10 ⊢ (1^st ‘𝑈) ∈ CVec_OLD
39	11	vafval 30539	. . . . . . . . . . 11 ⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))
40	39	vcablo 30505	. . . . . . . . . 10 ⊢ ((1^st ‘𝑈) ∈ CVec_OLD → 𝐺 ∈ AbelOp)
41	38, 40	ax-mp 5	. . . . . . . . 9 ⊢ 𝐺 ∈ AbelOp
42	8, 9	pm3.2i 470	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)
43	8, 30	pm3.2i 470	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)
44	10, 11	bafval 30540	. . . . . . . . . 10 ⊢ 𝑋 = ran 𝐺
45	44	ablo4 30486	. . . . . . . . 9 ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))))
46	41, 42, 43, 45	mp3an 1463	. . . . . . . 8 ⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵)))
47	15	smfval 30541	. . . . . . . . . . 11 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))
48	39, 47, 44	vc2OLD 30504	. . . . . . . . . 10 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴))
49	38, 8, 48	mp2an 692	. . . . . . . . 9 ⊢ (𝐴𝐺𝐴) = (2𝑆𝐴)
50		eqid 2730	. . . . . . . . . . 11 ⊢ (0_vec‘𝑈) = (0_vec‘𝑈)
51	10, 11, 15, 50	nvrinv 30587	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺(-1𝑆𝐵)) = (0_vec‘𝑈))
52	6, 9, 51	mp2an 692	. . . . . . . . 9 ⊢ (𝐵𝐺(-1𝑆𝐵)) = (0_vec‘𝑈)
53	49, 52	oveq12i 7402	. . . . . . . 8 ⊢ ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))) = ((2𝑆𝐴)𝐺(0_vec‘𝑈))
54	10, 15	nvscl 30562	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (2𝑆𝐴) ∈ 𝑋)
55	6, 1, 8, 54	mp3an 1463	. . . . . . . . 9 ⊢ (2𝑆𝐴) ∈ 𝑋
56	10, 11, 50	nv0rid 30571	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (2𝑆𝐴) ∈ 𝑋) → ((2𝑆𝐴)𝐺(0_vec‘𝑈)) = (2𝑆𝐴))
57	6, 55, 56	mp2an 692	. . . . . . . 8 ⊢ ((2𝑆𝐴)𝐺(0_vec‘𝑈)) = (2𝑆𝐴)
58	46, 53, 57	3eqtri 2757	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = (2𝑆𝐴)
59	58	oveq2i 7401	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆(2𝑆𝐴))
60	7, 1, 8	3pm3.2i 1340	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋)
61	10, 15	nvsass 30564	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋)) → (((1 / 2) · 2)𝑆𝐴) = ((1 / 2)𝑆(2𝑆𝐴)))
62	6, 60, 61	mp2an 692	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐴) = ((1 / 2)𝑆(2𝑆𝐴))
63	59, 62	eqtr4i 2756	. . . . 5 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2) · 2)𝑆𝐴)
64	7, 13, 32	3pm3.2i 1340	. . . . . 6 ⊢ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
65	10, 11, 15	nvdi 30566	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))
66	6, 64, 65	mp2an 692	. . . . 5 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))
67		ax-1cn 11133	. . . . . . . 8 ⊢ 1 ∈ ℂ
68	67, 1, 2	divcan1i 11933	. . . . . . 7 ⊢ ((1 / 2) · 2) = 1
69	68	oveq1i 7400	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐴) = (1𝑆𝐴)
70	10, 15	nvsid 30563	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
71	6, 8, 70	mp2an 692	. . . . . 6 ⊢ (1𝑆𝐴) = 𝐴
72	69, 71	eqtri 2753	. . . . 5 ⊢ (((1 / 2) · 2)𝑆𝐴) = 𝐴
73	63, 66, 72	3eqtr3i 2761	. . . 4 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) = 𝐴
74	73	oveq1i 7400	. . 3 ⊢ ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) = (𝐴𝑃𝐶)
75	28, 7	mulcomi 11189	. . . . . . . . 9 ⊢ (-1 · (1 / 2)) = ((1 / 2) · -1)
76	75	oveq1i 7400	. . . . . . . 8 ⊢ ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵)))
77	28, 7, 32	3pm3.2i 1340	. . . . . . . . 9 ⊢ (-1 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
78	10, 15	nvsass 30564	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))
79	6, 77, 78	mp2an 692	. . . . . . . 8 ⊢ ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))
80	7, 28, 32	3pm3.2i 1340	. . . . . . . . . 10 ⊢ ((1 / 2) ∈ ℂ ∧ -1 ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
81	10, 15	nvsass 30564	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ -1 ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵)))))
82	6, 80, 81	mp2an 692	. . . . . . . . 9 ⊢ (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵))))
83	28, 8, 30	3pm3.2i 1340	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)
84	10, 11, 15	nvdi 30566	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))))
85	6, 83, 84	mp2an 692	. . . . . . . . . . 11 ⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵)))
86		neg1mulneg1e1 12401	. . . . . . . . . . . . . 14 ⊢ (-1 · -1) = 1
87	86	oveq1i 7400	. . . . . . . . . . . . 13 ⊢ ((-1 · -1)𝑆𝐵) = (1𝑆𝐵)
88	28, 28, 9	3pm3.2i 1340	. . . . . . . . . . . . . 14 ⊢ (-1 ∈ ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋)
89	10, 15	nvsass 30564	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → ((-1 · -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵)))
90	6, 88, 89	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((-1 · -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵))
91	10, 15	nvsid 30563	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵)
92	6, 9, 91	mp2an 692	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐵) = 𝐵
93	87, 90, 92	3eqtr3i 2761	. . . . . . . . . . . 12 ⊢ (-1𝑆(-1𝑆𝐵)) = 𝐵
94	93	oveq2i 7401	. . . . . . . . . . 11 ⊢ ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵)
95	85, 94	eqtri 2753	. . . . . . . . . 10 ⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵)
96	95	oveq2i 7401	. . . . . . . . 9 ⊢ ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))
97	82, 96	eqtri 2753	. . . . . . . 8 ⊢ (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))
98	76, 79, 97	3eqtr3i 2761	. . . . . . 7 ⊢ (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))
99	98	oveq2i 7401	. . . . . 6 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)))
100	10, 15	nvscl 30562	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (-1𝑆𝐴) ∈ 𝑋)
101	6, 28, 8, 100	mp3an 1463	. . . . . . . . 9 ⊢ (-1𝑆𝐴) ∈ 𝑋
102	10, 11	nvgcl 30556	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)
103	6, 101, 9, 102	mp3an 1463	. . . . . . . 8 ⊢ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋
104	7, 13, 103	3pm3.2i 1340	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)
105	10, 11, 15	nvdi 30566	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)) → ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))))
106	6, 104, 105	mp2an 692	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)))
107	99, 106	eqtr4i 2756	. . . . 5 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)))
108	101, 9	pm3.2i 470	. . . . . . . . 9 ⊢ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)
109	44	ablo4 30486	. . . . . . . . 9 ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)))
110	41, 42, 108, 109	mp3an 1463	. . . . . . . 8 ⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵))
111	10, 11, 15, 50	nvrinv 30587	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐴)) = (0_vec‘𝑈))
112	6, 8, 111	mp2an 692	. . . . . . . . . 10 ⊢ (𝐴𝐺(-1𝑆𝐴)) = (0_vec‘𝑈)
113	112	oveq1i 7400	. . . . . . . . 9 ⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = ((0_vec‘𝑈)𝐺(𝐵𝐺𝐵))
114	10, 11	nvgcl 30556	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) ∈ 𝑋)
115	6, 9, 9, 114	mp3an 1463	. . . . . . . . . 10 ⊢ (𝐵𝐺𝐵) ∈ 𝑋
116	10, 11, 50	nv0lid 30572	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐵𝐺𝐵) ∈ 𝑋) → ((0_vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵))
117	6, 115, 116	mp2an 692	. . . . . . . . 9 ⊢ ((0_vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵)
118	113, 117	eqtri 2753	. . . . . . . 8 ⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵)
119	39, 47, 44	vc2OLD 30504	. . . . . . . . 9 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) = (2𝑆𝐵))
120	38, 9, 119	mp2an 692	. . . . . . . 8 ⊢ (𝐵𝐺𝐵) = (2𝑆𝐵)
121	110, 118, 120	3eqtri 2757	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = (2𝑆𝐵)
122	121	oveq2i 7401	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = ((1 / 2)𝑆(2𝑆𝐵))
123	7, 1, 9	3pm3.2i 1340	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋)
124	10, 15	nvsass 30564	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → (((1 / 2) · 2)𝑆𝐵) = ((1 / 2)𝑆(2𝑆𝐵)))
125	6, 123, 124	mp2an 692	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐵) = ((1 / 2)𝑆(2𝑆𝐵))
126	68	oveq1i 7400	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐵) = (1𝑆𝐵)
127	122, 125, 126	3eqtr2i 2759	. . . . 5 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (1𝑆𝐵)
128	107, 127, 92	3eqtri 2757	. . . 4 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = 𝐵
129	128	oveq1i 7400	. . 3 ⊢ ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶) = (𝐵𝑃𝐶)
130	74, 129	oveq12i 7402	. 2 ⊢ (((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))
131	27, 35, 130	3eqtr2i 2759	1 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))

Colors of variables: wff setvar class

Syntax hints: ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ‘cfv 6514 (class class class)co 7390 1^st c1st 7969 ℂcc 11073 1c1 11076 + caddc 11078 · cmul 11080 -cneg 11413 / cdiv 11842 2c2 12248 AbelOpcablo 30480 CVec_OLDcvc 30494 NrmCVeccnv 30520 +_𝑣 cpv 30521 BaseSetcba 30522 ·_𝑠OLD cns 30523 0_veccn0v 30524 ·_𝑖OLDcdip 30636 CPreHil_OLDccphlo 30748

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9400 df-oi 9470 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-n0 12450 df-z 12537 df-uz 12801 df-rp 12959 df-fz 13476 df-fzo 13623 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-sum 15660 df-grpo 30429 df-gid 30430 df-ginv 30431 df-ablo 30481 df-vc 30495 df-nv 30528 df-va 30531 df-ba 30532 df-sm 30533 df-0v 30534 df-nmcv 30536 df-dip 30637 df-ph 30749

This theorem is referenced by: ipdiri 30766

W3C validator