Theorem ip1i

Description: Equation 6.47 of Ponnusamy p. 362. (Contributed by NM, 27-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip1i.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	ip1i.2	$$⊢G={+}_v\left(U\right)$$
	ip1i.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	ip1i.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	ip1i.9	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
	ip1i.a	$$⊢A\in X$$
	ip1i.b	$$⊢B\in X$$
	ip1i.c	$$⊢C\in X$$
Assertion	ip1i	$$⊢\left(\left(AGB\right)PC\right)+\left(\left(AG\left(-1SB\right)\right)PC\right)=2\left(APC\right)$$

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ip1i.2	$$⊢G={+}_v\left(U\right)$$
3		ip1i.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
4		ip1i.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
5		ip1i.9	$$⊢U\in {CPreHil}_{\mathrm{OLD}}$$
6		ip1i.a	$$⊢A\in X$$
7		ip1i.b	$$⊢B\in X$$
8		ip1i.c	$$⊢C\in X$$
9		eqid	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(U\right)$$
10		ax-1cn	$$⊢1\in ℂ$$
11	1 2 3 4 5 6 7 8 9 10	ip1ilem	$$⊢\left(\left(AGB\right)PC\right)+\left(\left(AG\left(-1SB\right)\right)PC\right)=2\left(APC\right)$$