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 28910

Description: Lemma for ipdiri 28911. (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 11905	. . . . . . 7 ⊢ 2 ∈ ℂ
2		2ne0 11934	. . . . . . 7 ⊢ 2 ≠ 0
3	1, 2	recidi 11563	. . . . . 6 ⊢ (2 · (1 / 2)) = 1
4	3	oveq1i 7223	. . . . 5 ⊢ ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (1𝑆(𝐴𝐺𝐵))
5		ip1i.9	. . . . . . 7 ⊢ 𝑈 ∈ CPreHil_OLD
6	5	phnvi 28897	. . . . . 6 ⊢ 𝑈 ∈ NrmCVec
7		halfcn 12045	. . . . . . 7 ⊢ (1 / 2) ∈ ℂ
8		ipdiri.8	. . . . . . . 8 ⊢ 𝐴 ∈ 𝑋
9		ipdiri.9	. . . . . . . 8 ⊢ 𝐵 ∈ 𝑋
10		ip1i.1	. . . . . . . . 9 ⊢ 𝑋 = (BaseSet‘𝑈)
11		ip1i.2	. . . . . . . . 9 ⊢ 𝐺 = ( +_𝑣 ‘𝑈)
12	10, 11	nvgcl 28701	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
13	6, 8, 9, 12	mp3an 1463	. . . . . . 7 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
14	1, 7, 13	3pm3.2i 1341	. . . . . 6 ⊢ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋)
15		ip1i.4	. . . . . . 7 ⊢ 𝑆 = ( ·_𝑠OLD ‘𝑈)
16	10, 15	nvsass 28709	. . . . . 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 28708	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋) → (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵))
19	6, 13, 18	mp2an 692	. . . . 5 ⊢ (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵)
20	4, 17, 19	3eqtr3i 2773	. . . 4 ⊢ (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵))) = (𝐴𝐺𝐵)
21	20	oveq1i 7223	. . 3 ⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = ((𝐴𝐺𝐵)𝑃𝐶)
22		ip1i.7	. . . 4 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
23	10, 15	nvscl 28707	. . . . 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 28909	. . 3 ⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
27	21, 26	eqtr3i 2767	. 2 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
28		neg1cn 11944	. . . . . 6 ⊢ -1 ∈ ℂ
29	10, 15	nvscl 28707	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (-1𝑆𝐵) ∈ 𝑋)
30	6, 28, 9, 29	mp3an 1463	. . . . 5 ⊢ (-1𝑆𝐵) ∈ 𝑋
31	10, 11	nvgcl 28701	. . . . 5 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
32	6, 8, 30, 31	mp3an 1463	. . . 4 ⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
33	10, 15	nvscl 28707	. . . 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 28908	. 2 ⊢ (((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶))
36		eqid 2737	. . . . . . . . . . . 12 ⊢ (1^st ‘𝑈) = (1^st ‘𝑈)
37	36	nvvc 28696	. . . . . . . . . . 11 ⊢ (𝑈 ∈ NrmCVec → (1^st ‘𝑈) ∈ CVec_OLD)
38	6, 37	ax-mp 5	. . . . . . . . . 10 ⊢ (1^st ‘𝑈) ∈ CVec_OLD
39	11	vafval 28684	. . . . . . . . . . 11 ⊢ 𝐺 = (1^st ‘(1^st ‘𝑈))
40	39	vcablo 28650	. . . . . . . . . 10 ⊢ ((1^st ‘𝑈) ∈ CVec_OLD → 𝐺 ∈ AbelOp)
41	38, 40	ax-mp 5	. . . . . . . . 9 ⊢ 𝐺 ∈ AbelOp
42	8, 9	pm3.2i 474	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)
43	8, 30	pm3.2i 474	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)
44	10, 11	bafval 28685	. . . . . . . . . 10 ⊢ 𝑋 = ran 𝐺
45	44	ablo4 28631	. . . . . . . . 9 ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))))
46	41, 42, 43, 45	mp3an 1463	. . . . . . . 8 ⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵)))
47	15	smfval 28686	. . . . . . . . . . 11 ⊢ 𝑆 = (2^nd ‘(1^st ‘𝑈))
48	39, 47, 44	vc2OLD 28649	. . . . . . . . . 10 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴))
49	38, 8, 48	mp2an 692	. . . . . . . . 9 ⊢ (𝐴𝐺𝐴) = (2𝑆𝐴)
50		eqid 2737	. . . . . . . . . . 11 ⊢ (0_vec‘𝑈) = (0_vec‘𝑈)
51	10, 11, 15, 50	nvrinv 28732	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺(-1𝑆𝐵)) = (0_vec‘𝑈))
52	6, 9, 51	mp2an 692	. . . . . . . . 9 ⊢ (𝐵𝐺(-1𝑆𝐵)) = (0_vec‘𝑈)
53	49, 52	oveq12i 7225	. . . . . . . 8 ⊢ ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))) = ((2𝑆𝐴)𝐺(0_vec‘𝑈))
54	10, 15	nvscl 28707	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (2𝑆𝐴) ∈ 𝑋)
55	6, 1, 8, 54	mp3an 1463	. . . . . . . . 9 ⊢ (2𝑆𝐴) ∈ 𝑋
56	10, 11, 50	nv0rid 28716	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (2𝑆𝐴) ∈ 𝑋) → ((2𝑆𝐴)𝐺(0_vec‘𝑈)) = (2𝑆𝐴))
57	6, 55, 56	mp2an 692	. . . . . . . 8 ⊢ ((2𝑆𝐴)𝐺(0_vec‘𝑈)) = (2𝑆𝐴)
58	46, 53, 57	3eqtri 2769	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = (2𝑆𝐴)
59	58	oveq2i 7224	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆(2𝑆𝐴))
60	7, 1, 8	3pm3.2i 1341	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋)
61	10, 15	nvsass 28709	. . . . . . 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 2768	. . . . 5 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2) · 2)𝑆𝐴)
64	7, 13, 32	3pm3.2i 1341	. . . . . 6 ⊢ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
65	10, 11, 15	nvdi 28711	. . . . . 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 10787	. . . . . . . 8 ⊢ 1 ∈ ℂ
68	67, 1, 2	divcan1i 11576	. . . . . . 7 ⊢ ((1 / 2) · 2) = 1
69	68	oveq1i 7223	. . . . . 6 ⊢ (((1 / 2) · 2)𝑆𝐴) = (1𝑆𝐴)
70	10, 15	nvsid 28708	. . . . . . 7 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴)
71	6, 8, 70	mp2an 692	. . . . . 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 7223	. . 3 ⊢ ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) = (𝐴𝑃𝐶)
75	28, 7	mulcomi 10841	. . . . . . . . 9 ⊢ (-1 · (1 / 2)) = ((1 / 2) · -1)
76	75	oveq1i 7223	. . . . . . . 8 ⊢ ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵)))
77	28, 7, 32	3pm3.2i 1341	. . . . . . . . 9 ⊢ (-1 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
78	10, 15	nvsass 28709	. . . . . . . . 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 1341	. . . . . . . . . 10 ⊢ ((1 / 2) ∈ ℂ ∧ -1 ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
81	10, 15	nvsass 28709	. . . . . . . . . 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 1341	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)
84	10, 11, 15	nvdi 28711	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))))
85	6, 83, 84	mp2an 692	. . . . . . . . . . 11 ⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵)))
86		neg1mulneg1e1 12043	. . . . . . . . . . . . . 14 ⊢ (-1 · -1) = 1
87	86	oveq1i 7223	. . . . . . . . . . . . 13 ⊢ ((-1 · -1)𝑆𝐵) = (1𝑆𝐵)
88	28, 28, 9	3pm3.2i 1341	. . . . . . . . . . . . . 14 ⊢ (-1 ∈ ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋)
89	10, 15	nvsass 28709	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈ ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → ((-1 · -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵)))
90	6, 88, 89	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((-1 · -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵))
91	10, 15	nvsid 28708	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵)
92	6, 9, 91	mp2an 692	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐵) = 𝐵
93	87, 90, 92	3eqtr3i 2773	. . . . . . . . . . . 12 ⊢ (-1𝑆(-1𝑆𝐵)) = 𝐵
94	93	oveq2i 7224	. . . . . . . . . . 11 ⊢ ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵)
95	85, 94	eqtri 2765	. . . . . . . . . 10 ⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵)
96	95	oveq2i 7224	. . . . . . . . 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 7224	. . . . . 6 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)))
100	10, 15	nvscl 28707	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (-1𝑆𝐴) ∈ 𝑋)
101	6, 28, 8, 100	mp3an 1463	. . . . . . . . 9 ⊢ (-1𝑆𝐴) ∈ 𝑋
102	10, 11	nvgcl 28701	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)
103	6, 101, 9, 102	mp3an 1463	. . . . . . . 8 ⊢ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋
104	7, 13, 103	3pm3.2i 1341	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)
105	10, 11, 15	nvdi 28711	. . . . . . 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 2768	. . . . 5 ⊢ (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)))
108	101, 9	pm3.2i 474	. . . . . . . . 9 ⊢ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)
109	44	ablo4 28631	. . . . . . . . 9 ⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)))
110	41, 42, 108, 109	mp3an 1463	. . . . . . . 8 ⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵))
111	10, 11, 15, 50	nvrinv 28732	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐴)) = (0_vec‘𝑈))
112	6, 8, 111	mp2an 692	. . . . . . . . . 10 ⊢ (𝐴𝐺(-1𝑆𝐴)) = (0_vec‘𝑈)
113	112	oveq1i 7223	. . . . . . . . 9 ⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = ((0_vec‘𝑈)𝐺(𝐵𝐺𝐵))
114	10, 11	nvgcl 28701	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) ∈ 𝑋)
115	6, 9, 9, 114	mp3an 1463	. . . . . . . . . 10 ⊢ (𝐵𝐺𝐵) ∈ 𝑋
116	10, 11, 50	nv0lid 28717	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐵𝐺𝐵) ∈ 𝑋) → ((0_vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵))
117	6, 115, 116	mp2an 692	. . . . . . . . 9 ⊢ ((0_vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵)
118	113, 117	eqtri 2765	. . . . . . . 8 ⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵)
119	39, 47, 44	vc2OLD 28649	. . . . . . . . 9 ⊢ (((1^st ‘𝑈) ∈ CVec_OLD ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) = (2𝑆𝐵))
120	38, 9, 119	mp2an 692	. . . . . . . 8 ⊢ (𝐵𝐺𝐵) = (2𝑆𝐵)
121	110, 118, 120	3eqtri 2769	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = (2𝑆𝐵)
122	121	oveq2i 7224	. . . . . 6 ⊢ ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = ((1 / 2)𝑆(2𝑆𝐵))
123	7, 1, 9	3pm3.2i 1341	. . . . . . 7 ⊢ ((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋)
124	10, 15	nvsass 28709	. . . . . . 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 7223	. . . . . 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 7223	. . 3 ⊢ ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶) = (𝐵𝑃𝐶)
130	74, 129	oveq12i 7225	. 2 ⊢ (((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))
131	27, 35, 130	3eqtr2i 2771	1 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))

Colors of variables: wff setvar class

Syntax hints: ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 ‘cfv 6380 (class class class)co 7213 1^st c1st 7759 ℂcc 10727 1c1 10730 + caddc 10732 · cmul 10734 -cneg 11063 / cdiv 11489 2c2 11885 AbelOpcablo 28625 CVec_OLDcvc 28639 NrmCVeccnv 28665 +_𝑣 cpv 28666 BaseSetcba 28667 ·_𝑠OLD cns 28668 0_veccn0v 28669 ·_𝑖OLDcdip 28781 CPreHil_OLDccphlo 28893

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-rep 5179 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-inf2 9256 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806 ax-pre-sup 10807

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-int 4860 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-se 5510 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-isom 6389 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-1st 7761 df-2nd 7762 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-1o 8202 df-er 8391 df-en 8627 df-dom 8628 df-sdom 8629 df-fin 8630 df-sup 9058 df-oi 9126 df-card 9555 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-div 11490 df-nn 11831 df-2 11893 df-3 11894 df-4 11895 df-n0 12091 df-z 12177 df-uz 12439 df-rp 12587 df-fz 13096 df-fzo 13239 df-seq 13575 df-exp 13636 df-hash 13897 df-cj 14662 df-re 14663 df-im 14664 df-sqrt 14798 df-abs 14799 df-clim 15049 df-sum 15250 df-grpo 28574 df-gid 28575 df-ginv 28576 df-ablo 28626 df-vc 28640 df-nv 28673 df-va 28676 df-ba 28677 df-sm 28678 df-0v 28679 df-nmcv 28681 df-dip 28782 df-ph 28894

This theorem is referenced by: ipdiri 28911

W3C validator