Theorem dipass

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

	Ref	Expression
Hypotheses	ipass.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	ipass.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	ipass.7	$$⊢P={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
Assertion	dipass	$$⊢\left(U\in {CPreHil}_{\mathrm{OLD}}\wedge \left(A\in ℂ\wedge B\in X\wedge C\in X\right)\right)\to \left(ASB\right)PC=A\left(BPC\right)$$

Proof

Step	Hyp	Ref	Expression
1		ipass.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ipass.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
3		ipass.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(B\in X\leftrightarrow B\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(C\in X\leftrightarrow C\in \mathrm{BaseSet}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)\right)$$
8	6 7	3anbi23d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(A\in ℂ\wedge B\in X\wedge C\in X\right)\leftrightarrow \left(A\in ℂ\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)$$
9		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)$$
10	2 9	syl5eq	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to S={\cdot }_{\mathrm{𝑠OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)$$
11	10	oveqd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to ASB=A{\cdot }_{\mathrm{𝑠OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B$$
12	11	oveq1d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(ASB\right)PC=\left(A{\cdot }_{\mathrm{𝑠OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right)PC$$
13		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)$$
14	3 13	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)$$
15	14	oveqd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(A{\cdot }_{\mathrm{𝑠OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)B\right)PC=\left(A{\cdot }_{\mathrm{𝑠OLD}}\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$$
16	12 15	eqtrd	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(ASB\right)PC=\left(A{\cdot }_{\mathrm{𝑠OLD}}\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	14	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$$
18	17	oveq2d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to A\left(BPC\right)=A\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)$$
19	16 18	eqeq12d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(ASB\right)PC=A\left(BPC\right)\leftrightarrow \left(A{\cdot }_{\mathrm{𝑠OLD}}\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=A\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)\right)$$
20	8 19	imbi12d	$$⊢U=if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\to \left(\left(\left(A\in ℂ\wedge B\in X\wedge C\in X\right)\to \left(ASB\right)PC=A\left(BPC\right)\right)\leftrightarrow \left(\left(A\in ℂ\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{\cdot }_{\mathrm{𝑠OLD}}\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=A\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)\right)\right)$$
21		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)$$
22		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)$$
23		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)$$
24		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)$$
25		elimphu	$$⊢if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\in {CPreHil}_{\mathrm{OLD}}$$
26	21 22 23 24 25	ipassi	$$⊢\left(A\in ℂ\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{\cdot }_{\mathrm{𝑠OLD}}\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=A\left(B{\cdot }_{\mathrm{𝑖OLD}}\left(if\left(U\in {CPreHil}_{\mathrm{OLD}},U,⟨⟨+,\times ⟩,\mathrm{abs}⟩\right)\right)C\right)$$
27	20 26	dedth	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to \left(\left(A\in ℂ\wedge B\in X\wedge C\in X\right)\to \left(ASB\right)PC=A\left(BPC\right)\right)$$
28	27	imp	$$⊢\left(U\in {CPreHil}_{\mathrm{OLD}}\wedge \left(A\in ℂ\wedge B\in X\wedge C\in X\right)\right)\to \left(ASB\right)PC=A\left(BPC\right)$$