Metamath Proof Explorer


Theorem dipassr2

Description: "Associative" law for inner product. Conjugate version of dipassr . (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipass.1 X = BaseSet U
ipass.4 S = 𝑠OLD U
ipass.7 P = 𝑖OLD U
Assertion dipassr2 U CPreHil OLD A X B C X A P B S C = B A P C

Proof

Step Hyp Ref Expression
1 ipass.1 X = BaseSet U
2 ipass.4 S = 𝑠OLD U
3 ipass.7 P = 𝑖OLD U
4 cjcl B B
5 1 2 3 dipassr U CPreHil OLD A X B C X A P B S C = B A P C
6 4 5 syl3anr2 U CPreHil OLD A X B C X A P B S C = B A P C
7 cjcj B B = B
8 7 3ad2ant2 A X B C X B = B
9 8 adantl U CPreHil OLD A X B C X B = B
10 9 oveq1d U CPreHil OLD A X B C X B A P C = B A P C
11 6 10 eqtrd U CPreHil OLD A X B C X A P B S C = B A P C