Theorem dipdir

Description: Distributive law for inner product. Equation I3 of Ponnusamy p. 362. (Contributed by NM, 25-Aug-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dipdir.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	dipdir.2	$$⊢G={+}_v\left(U\right)$$
	dipdir.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
Assertion	dipdir	$$⊢\left(U\in {CPreHil}_{\mathrm{OLD}}\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(AGB\right)PC=\left(APC\right)+\left(BPC\right)$$

Proof

Step	Hyp	Ref	Expression
1		dipdir.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		dipdir.2	$$⊢G={+}_v\left(U\right)$$
3		dipdir.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
4		fveq2	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
5	1 4	syl5eq	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to X=\mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
6	5	eleq2d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(A\in X\leftrightarrow A\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)$$
7	5	eleq2d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(B\in X\leftrightarrow B\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)$$
8	5	eleq2d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(C\in X\leftrightarrow C\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)$$
9	6 7 8	3anbi123d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(A\in X\wedge B\in X\wedge C\in X\right)\leftrightarrow \left(A\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge B\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge C\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)\right)$$
10		fveq2	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to {+}_v\left(U\right)={+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
11	2 10	syl5eq	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to G={+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
12	11	oveqd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to AGB=A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B$$
13	12	oveq1d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(AGB\right)PC=\left(A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right)PC$$
14		fveq2	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to {\cdot }_{\mathrm{𝑖OLD}}\left(U\right)={\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
15	3 14	syl5eq	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to P={\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
16	15	oveqd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right)PC=\left(A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C$$
17	13 16	eqtrd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(AGB\right)PC=\left(A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C$$
18	15	oveqd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to APC=A{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C$$
19	15	oveqd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to BPC=B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C$$
20	18 19	oveq12d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(APC\right)+\left(BPC\right)=\left(A{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)+\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)$$
21	17 20	eqeq12d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(AGB\right)PC=\left(APC\right)+\left(BPC\right)\leftrightarrow \left(A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C=\left(A{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)+\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)\right)$$
22	9 21	imbi12d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(\left(A\in X\wedge B\in X\wedge C\in X\right)\to \left(AGB\right)PC=\left(APC\right)+\left(BPC\right)\right)\leftrightarrow \left(\left(A\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge B\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge C\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)\to \left(A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C=\left(A{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)+\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)\right)\right)$$
23		eqid	$$⊢\mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)=\mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
24		eqid	$$⊢{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)={+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
25		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)={\cdot }_{\mathrm{𝑠OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
26		eqid	$$⊢{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)={\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
27		elimphu	$$⊢if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\in {CPreHil}_{\mathrm{OLD}}$$
28	23 24 25 26 27	ipdiri	$$⊢\left(A\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge B\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\wedge C\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)\to \left(A{+}_v\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right){\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C=\left(A{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)+\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)$$
29	22 28	dedth	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to \left(\left(A\in X\wedge B\in X\wedge C\in X\right)\to \left(AGB\right)PC=\left(APC\right)+\left(BPC\right)\right)$$
30	29	imp	$$⊢\left(U\in {CPreHil}_{\mathrm{OLD}}\wedge \left(A\in X\wedge B\in X\wedge C\in X\right)\right)\to \left(AGB\right)PC=\left(APC\right)+\left(BPC\right)$$