ip1ilem

Description: Lemma for ip1i . (Contributed by NM, 21-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip1i.1	$⊢ X = BaseSet (U)$
	ip1i.2	$⊢ G = +_{v} (U)$
	ip1i.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
	ip1i.a	$⊢ A \in X$
	ip1i.b	$⊢ B \in X$
	ip1i.c	$⊢ C \in X$
	ip1i.6	$⊢ N = {norm}_{CV} (U)$
	ip0i.j	$⊢ J \in ℂ$
Assertion	ip1ilem	$⊢ ((A G B) P C) + ((A G (-1 S B)) P C) = 2 (A P C)$

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	$⊢ X = BaseSet (U)$
2		ip1i.2	$⊢ G = +_{v} (U)$
3		ip1i.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
5		ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
6		ip1i.a	$⊢ A \in X$
7		ip1i.b	$⊢ B \in X$
8		ip1i.c	$⊢ C \in X$
9		ip1i.6	$⊢ N = {norm}_{CV} (U)$
10		ip0i.j	$⊢ J \in ℂ$
11	5	phnvi	$⊢ U \in NrmCVec$
12	1 2 3 9 4	4ipval2	$⊢ (U \in NrmCVec \land A \in X \land C \in X) \to 4 (A P C) = {N (A G C)}^{2} - {N (A G (-1 S C))}^{2} + i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
13	11 6 8 12	mp3an	$⊢ 4 (A P C) = {N (A G C)}^{2} - {N (A G (-1 S C))}^{2} + i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
14	13	oveq2i	$⊢ 2 4 (A P C) = 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2} + i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2}))$
15		2cn	$⊢ 2 \in ℂ$
16		4cn	$⊢ 4 \in ℂ$
17	1 4	dipcl	$⊢ (U \in NrmCVec \land A \in X \land C \in X) \to A P C \in ℂ$
18	11 6 8 17	mp3an	$⊢ A P C \in ℂ$
19	15 16 18	mul12i	$⊢ 2 4 (A P C) = 4 2 (A P C)$
20	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land C \in X) \to A G C \in X$
21	11 6 8 20	mp3an	$⊢ A G C \in X$
22	1 9 11 21	nvcli	$⊢ N (A G C) \in ℝ$
23	22	resqcli	$⊢ {N (A G C)}^{2} \in ℝ$
24	23	recni	$⊢ {N (A G C)}^{2} \in ℂ$
25		ax-1cn	$⊢ 1 \in ℂ$
26	25	negcli	$⊢ - 1 \in ℂ$
27	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land C \in X) \to -1 S C \in X$
28	11 26 8 27	mp3an	$⊢ -1 S C \in X$
29	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land -1 S C \in X) \to A G (-1 S C) \in X$
30	11 6 28 29	mp3an	$⊢ A G (-1 S C) \in X$
31	1 9 11 30	nvcli	$⊢ N (A G (-1 S C)) \in ℝ$
32	31	resqcli	$⊢ {N (A G (-1 S C))}^{2} \in ℝ$
33	32	recni	$⊢ {N (A G (-1 S C))}^{2} \in ℂ$
34	24 33	subcli	$⊢ {N (A G C)}^{2} - {N (A G (-1 S C))}^{2} \in ℂ$
35		ax-icn	$⊢ i \in ℂ$
36	1 3	nvscl	$⊢ (U \in NrmCVec \land i \in ℂ \land C \in X) \to i S C \in X$
37	11 35 8 36	mp3an	$⊢ i S C \in X$
38	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land i S C \in X) \to A G (i S C) \in X$
39	11 6 37 38	mp3an	$⊢ A G (i S C) \in X$
40	1 9 11 39	nvcli	$⊢ N (A G (i S C)) \in ℝ$
41	40	resqcli	$⊢ {N (A G (i S C))}^{2} \in ℝ$
42	41	recni	$⊢ {N (A G (i S C))}^{2} \in ℂ$
43	35	negcli	$⊢ - i \in ℂ$
44	1 3	nvscl	$⊢ (U \in NrmCVec \land - i \in ℂ \land C \in X) \to (- i) S C \in X$
45	11 43 8 44	mp3an	$⊢ (- i) S C \in X$
46	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land (- i) S C \in X) \to A G ((- i) S C) \in X$
47	11 6 45 46	mp3an	$⊢ A G ((- i) S C) \in X$
48	1 9 11 47	nvcli	$⊢ N (A G ((- i) S C)) \in ℝ$
49	48	resqcli	$⊢ {N (A G ((- i) S C))}^{2} \in ℝ$
50	49	recni	$⊢ {N (A G ((- i) S C))}^{2} \in ℂ$
51	42 50	subcli	$⊢ {N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2} \in ℂ$
52	35 51	mulcli	$⊢ i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2}) \in ℂ$
53	15 34 52	adddii	$⊢ 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2} + i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})) = 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2}) + 2 i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
54	1 2 3 4 5 6 7 8 9 25	ip0i	$⊢ ({N ((A G B) G (1 S C))}^{2} - {N ((A G B) G (-1 S C))}^{2}) + {N ((A G (-1 S B)) G (1 S C))}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2} = 2 ({N (A G (1 S C))}^{2} - {N (A G (-1 S C))}^{2})$
55	1 3	nvsid	$⊢ (U \in NrmCVec \land C \in X) \to 1 S C = C$
56	11 8 55	mp2an	$⊢ 1 S C = C$
57	56	oveq2i	$⊢ (A G B) G (1 S C) = (A G B) G C$
58	57	fveq2i	$⊢ N ((A G B) G (1 S C)) = N ((A G B) G C)$
59	58	oveq1i	$⊢ {N ((A G B) G (1 S C))}^{2} = {N ((A G B) G C)}^{2}$
60	59	oveq1i	$⊢ {N ((A G B) G (1 S C))}^{2} - {N ((A G B) G (-1 S C))}^{2} = {N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}$
61	56	oveq2i	$⊢ (A G (-1 S B)) G (1 S C) = (A G (-1 S B)) G C$
62	61	fveq2i	$⊢ N ((A G (-1 S B)) G (1 S C)) = N ((A G (-1 S B)) G C)$
63	62	oveq1i	$⊢ {N ((A G (-1 S B)) G (1 S C))}^{2} = {N ((A G (-1 S B)) G C)}^{2}$
64	63	oveq1i	$⊢ {N ((A G (-1 S B)) G (1 S C))}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2} = {N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}$
65	60 64	oveq12i	$⊢ ({N ((A G B) G (1 S C))}^{2} - {N ((A G B) G (-1 S C))}^{2}) + {N ((A G (-1 S B)) G (1 S C))}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2} = ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + {N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}$
66	56	oveq2i	$⊢ A G (1 S C) = A G C$
67	66	fveq2i	$⊢ N (A G (1 S C)) = N (A G C)$
68	67	oveq1i	$⊢ {N (A G (1 S C))}^{2} = {N (A G C)}^{2}$
69	68	oveq1i	$⊢ {N (A G (1 S C))}^{2} - {N (A G (-1 S C))}^{2} = {N (A G C)}^{2} - {N (A G (-1 S C))}^{2}$
70	69	oveq2i	$⊢ 2 ({N (A G (1 S C))}^{2} - {N (A G (-1 S C))}^{2}) = 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2})$
71	54 65 70	3eqtr3i	$⊢ ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + {N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2} = 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2})$
72	1 2 3 4 5 6 7 8 9 35	ip0i	$⊢ ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + {N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2} = 2 ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
73	72	oveq2i	$⊢ i (({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + {N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2}) = i 2 ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
74	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G B \in X$
75	11 6 7 74	mp3an	$⊢ A G B \in X$
76	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G B \in X \land i S C \in X) \to (A G B) G (i S C) \in X$
77	11 75 37 76	mp3an	$⊢ (A G B) G (i S C) \in X$
78	1 9 11 77	nvcli	$⊢ N ((A G B) G (i S C)) \in ℝ$
79	78	resqcli	$⊢ {N ((A G B) G (i S C))}^{2} \in ℝ$
80	79	recni	$⊢ {N ((A G B) G (i S C))}^{2} \in ℂ$
81	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G B \in X \land (- i) S C \in X) \to (A G B) G ((- i) S C) \in X$
82	11 75 45 81	mp3an	$⊢ (A G B) G ((- i) S C) \in X$
83	1 9 11 82	nvcli	$⊢ N ((A G B) G ((- i) S C)) \in ℝ$
84	83	resqcli	$⊢ {N ((A G B) G ((- i) S C))}^{2} \in ℝ$
85	84	recni	$⊢ {N ((A G B) G ((- i) S C))}^{2} \in ℂ$
86	80 85	subcli	$⊢ {N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2} \in ℂ$
87	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land B \in X) \to -1 S B \in X$
88	11 26 7 87	mp3an	$⊢ -1 S B \in X$
89	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land -1 S B \in X) \to A G (-1 S B) \in X$
90	11 6 88 89	mp3an	$⊢ A G (-1 S B) \in X$
91	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land i S C \in X) \to (A G (-1 S B)) G (i S C) \in X$
92	11 90 37 91	mp3an	$⊢ (A G (-1 S B)) G (i S C) \in X$
93	1 9 11 92	nvcli	$⊢ N ((A G (-1 S B)) G (i S C)) \in ℝ$
94	93	resqcli	$⊢ {N ((A G (-1 S B)) G (i S C))}^{2} \in ℝ$
95	94	recni	$⊢ {N ((A G (-1 S B)) G (i S C))}^{2} \in ℂ$
96	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land (- i) S C \in X) \to (A G (-1 S B)) G ((- i) S C) \in X$
97	11 90 45 96	mp3an	$⊢ (A G (-1 S B)) G ((- i) S C) \in X$
98	1 9 11 97	nvcli	$⊢ N ((A G (-1 S B)) G ((- i) S C)) \in ℝ$
99	98	resqcli	$⊢ {N ((A G (-1 S B)) G ((- i) S C))}^{2} \in ℝ$
100	99	recni	$⊢ {N ((A G (-1 S B)) G ((- i) S C))}^{2} \in ℂ$
101	95 100	subcli	$⊢ {N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2} \in ℂ$
102	35 86 101	adddii	$⊢ i (({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + {N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2}) = i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2})$
103	35 15 51	mul12i	$⊢ i 2 ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2}) = 2 i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
104	73 102 103	3eqtr3i	$⊢ i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2}) = 2 i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
105	71 104	oveq12i	$⊢ ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + ({N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}) + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2}) = 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2}) + 2 i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})$
106	53 105	eqtr4i	$⊢ 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2} + i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})) = ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + ({N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}) + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2})$
107	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G B \in X \land C \in X) \to (A G B) G C \in X$
108	11 75 8 107	mp3an	$⊢ (A G B) G C \in X$
109	1 9 11 108	nvcli	$⊢ N ((A G B) G C) \in ℝ$
110	109	resqcli	$⊢ {N ((A G B) G C)}^{2} \in ℝ$
111	110	recni	$⊢ {N ((A G B) G C)}^{2} \in ℂ$
112	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G B \in X \land -1 S C \in X) \to (A G B) G (-1 S C) \in X$
113	11 75 28 112	mp3an	$⊢ (A G B) G (-1 S C) \in X$
114	1 9 11 113	nvcli	$⊢ N ((A G B) G (-1 S C)) \in ℝ$
115	114	resqcli	$⊢ {N ((A G B) G (-1 S C))}^{2} \in ℝ$
116	115	recni	$⊢ {N ((A G B) G (-1 S C))}^{2} \in ℂ$
117	111 116	subcli	$⊢ {N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2} \in ℂ$
118	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land C \in X) \to (A G (-1 S B)) G C \in X$
119	11 90 8 118	mp3an	$⊢ (A G (-1 S B)) G C \in X$
120	1 9 11 119	nvcli	$⊢ N ((A G (-1 S B)) G C) \in ℝ$
121	120	resqcli	$⊢ {N ((A G (-1 S B)) G C)}^{2} \in ℝ$
122	121	recni	$⊢ {N ((A G (-1 S B)) G C)}^{2} \in ℂ$
123	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land -1 S C \in X) \to (A G (-1 S B)) G (-1 S C) \in X$
124	11 90 28 123	mp3an	$⊢ (A G (-1 S B)) G (-1 S C) \in X$
125	1 9 11 124	nvcli	$⊢ N ((A G (-1 S B)) G (-1 S C)) \in ℝ$
126	125	resqcli	$⊢ {N ((A G (-1 S B)) G (-1 S C))}^{2} \in ℝ$
127	126	recni	$⊢ {N ((A G (-1 S B)) G (-1 S C))}^{2} \in ℂ$
128	122 127	subcli	$⊢ {N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2} \in ℂ$
129	35 86	mulcli	$⊢ i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) \in ℂ$
130	35 101	mulcli	$⊢ i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2}) \in ℂ$
131	117 128 129 130	add4i	$⊢ ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + ({N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}) + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2}) = ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + ({N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2})$
132	1 4	dipcl	$⊢ (U \in NrmCVec \land A G B \in X \land C \in X) \to (A G B) P C \in ℂ$
133	11 75 8 132	mp3an	$⊢ (A G B) P C \in ℂ$
134	1 4	dipcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land C \in X) \to (A G (-1 S B)) P C \in ℂ$
135	11 90 8 134	mp3an	$⊢ (A G (-1 S B)) P C \in ℂ$
136	16 133 135	adddii	$⊢ 4 (((A G B) P C) + ((A G (-1 S B)) P C)) = 4 ((A G B) P C) + 4 ((A G (-1 S B)) P C)$
137	1 2 3 9 4	4ipval2	$⊢ (U \in NrmCVec \land A G B \in X \land C \in X) \to 4 ((A G B) P C) = {N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2} + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2})$
138	11 75 8 137	mp3an	$⊢ 4 ((A G B) P C) = {N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2} + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2})$
139	1 2 3 9 4	4ipval2	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land C \in X) \to 4 ((A G (-1 S B)) P C) = {N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2} + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2})$
140	11 90 8 139	mp3an	$⊢ 4 ((A G (-1 S B)) P C) = {N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2} + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2})$
141	138 140	oveq12i	$⊢ 4 ((A G B) P C) + 4 ((A G (-1 S B)) P C) = ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + ({N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2})$
142	136 141	eqtr2i	$⊢ ({N ((A G B) G C)}^{2} - {N ((A G B) G (-1 S C))}^{2}) + i ({N ((A G B) G (i S C))}^{2} - {N ((A G B) G ((- i) S C))}^{2}) + ({N ((A G (-1 S B)) G C)}^{2} - {N ((A G (-1 S B)) G (-1 S C))}^{2}) + i ({N ((A G (-1 S B)) G (i S C))}^{2} - {N ((A G (-1 S B)) G ((- i) S C))}^{2}) = 4 (((A G B) P C) + ((A G (-1 S B)) P C))$
143	106 131 142	3eqtri	$⊢ 2 ({N (A G C)}^{2} - {N (A G (-1 S C))}^{2} + i ({N (A G (i S C))}^{2} - {N (A G ((- i) S C))}^{2})) = 4 (((A G B) P C) + ((A G (-1 S B)) P C))$
144	14 19 143	3eqtr3ri	$⊢ 4 (((A G B) P C) + ((A G (-1 S B)) P C)) = 4 2 (A P C)$
145	144	oveq1i	$⊢ \frac{4 (((A G B) P C) + ((A G (-1 S B)) P C))}{4} = \frac{4 2 (A P C)}{4}$
146	133 135	addcli	$⊢ ((A G B) P C) + ((A G (-1 S B)) P C) \in ℂ$
147		4ne0	$⊢ 4 \neq 0$
148	146 16 147	divcan3i	$⊢ \frac{4 (((A G B) P C) + ((A G (-1 S B)) P C))}{4} = ((A G B) P C) + ((A G (-1 S B)) P C)$
149	15 18	mulcli	$⊢ 2 (A P C) \in ℂ$
150	149 16 147	divcan3i	$⊢ \frac{4 2 (A P C)}{4} = 2 (A P C)$
151	145 148 150	3eqtr3i	$⊢ ((A G B) P C) + ((A G (-1 S B)) P C) = 2 (A P C)$

Metamath Proof Explorer

Theorem ip1ilem

Proof