Theorem ipdiri

Description: Distributive law for inner product. Equation I3 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}}$$
Assertion	ipdiri	$$⊢\left(A\in X\wedge B\in X\wedge C\in X\right)\to \left(AGB\right)PC=\left(APC\right)+\left(BPC\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		oveq1	$$⊢A=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)\to AGB=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)GB$$
7	6	oveq1d	$$⊢A=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)\to \left(AGB\right)PC=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)GB\right)PC$$
8		oveq1	$$⊢A=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)\to APC=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC$$
9	8	oveq1d	$$⊢A=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)\to \left(APC\right)+\left(BPC\right)=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(BPC\right)$$
10	7 9	eqeq12d	$$⊢A=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)\to \left(\left(AGB\right)PC=\left(APC\right)+\left(BPC\right)\leftrightarrow \left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)GB\right)PC=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(BPC\right)\right)$$
11		oveq2	$$⊢B=if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\to if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)GB=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)$$
12	11	oveq1d	$$⊢B=if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\to \left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)GB\right)PC=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\right)PC$$
13		oveq1	$$⊢B=if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\to BPC=if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)PC$$
14	13	oveq2d	$$⊢B=if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\to \left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(BPC\right)=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)PC\right)$$
15	12 14	eqeq12d	$$⊢B=if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\to \left(\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)GB\right)PC=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(BPC\right)\leftrightarrow \left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\right)PC=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)PC\right)\right)$$
16		oveq2	$$⊢C=if\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\to \left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\right)PC=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)$$
17		oveq2	$$⊢C=if\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\to if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC=if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)$$
18		oveq2	$$⊢C=if\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\to if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)PC=if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)$$
19	17 18	oveq12d	$$⊢C=if\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\to \left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)PC\right)=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\right)+\left(if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\right)$$
20	16 19	eqeq12d	$$⊢C=if\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\to \left(\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\right)PC=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)PC\right)+\left(if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)PC\right)\leftrightarrow \left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\right)+\left(if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\right)\right)$$
21		eqid	$$⊢0_{\mathrm{vec}}\left(U\right)=0_{\mathrm{vec}}\left(U\right)$$
22	1 21 5	elimph	$$⊢if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)\in X$$
23	1 21 5	elimph	$$⊢if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\in X$$
24	1 21 5	elimph	$$⊢if\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\in X$$
25	1 2 3 4 5 22 23 24	ipdirilem	$$⊢\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Gif\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)=\left(if\left(A\in X,A,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\right)+\left(if\left(B\in X,B,0_{\mathrm{vec}}\left(U\right)\right)Pif\left(C\in X,C,0_{\mathrm{vec}}\left(U\right)\right)\right)$$
26	10 15 20 25	dedth3h	$$⊢\left(A\in X\wedge B\in X\wedge C\in X\right)\to \left(AGB\right)PC=\left(APC\right)+\left(BPC\right)$$