Metamath Proof Explorer


Theorem dipassr

Description: "Associative" law for second argument of inner product (compare dipass ). (Contributed by NM, 22-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ipass.1
|- X = ( BaseSet ` U )
ipass.4
|- S = ( .sOLD ` U )
ipass.7
|- P = ( .iOLD ` U )
Assertion dipassr
|- ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( A P ( B S C ) ) = ( ( * ` B ) x. ( A P C ) ) )

Proof

Step Hyp Ref Expression
1 ipass.1
 |-  X = ( BaseSet ` U )
2 ipass.4
 |-  S = ( .sOLD ` U )
3 ipass.7
 |-  P = ( .iOLD ` U )
4 3anrot
 |-  ( ( A e. X /\ B e. CC /\ C e. X ) <-> ( B e. CC /\ C e. X /\ A e. X ) )
5 1 2 3 dipass
 |-  ( ( U e. CPreHilOLD /\ ( B e. CC /\ C e. X /\ A e. X ) ) -> ( ( B S C ) P A ) = ( B x. ( C P A ) ) )
6 4 5 sylan2b
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( ( B S C ) P A ) = ( B x. ( C P A ) ) )
7 6 fveq2d
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( ( B S C ) P A ) ) = ( * ` ( B x. ( C P A ) ) ) )
8 phnv
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
9 simpl
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> U e. NrmCVec )
10 1 2 nvscl
 |-  ( ( U e. NrmCVec /\ B e. CC /\ C e. X ) -> ( B S C ) e. X )
11 10 3adant3r1
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( B S C ) e. X )
12 simpr1
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> A e. X )
13 1 3 dipcj
 |-  ( ( U e. NrmCVec /\ ( B S C ) e. X /\ A e. X ) -> ( * ` ( ( B S C ) P A ) ) = ( A P ( B S C ) ) )
14 9 11 12 13 syl3anc
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( ( B S C ) P A ) ) = ( A P ( B S C ) ) )
15 8 14 sylan
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( ( B S C ) P A ) ) = ( A P ( B S C ) ) )
16 simpr2
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> B e. CC )
17 1 3 dipcl
 |-  ( ( U e. NrmCVec /\ C e. X /\ A e. X ) -> ( C P A ) e. CC )
18 17 3com23
 |-  ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( C P A ) e. CC )
19 18 3adant3r2
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( C P A ) e. CC )
20 16 19 cjmuld
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( B x. ( C P A ) ) ) = ( ( * ` B ) x. ( * ` ( C P A ) ) ) )
21 1 3 dipcj
 |-  ( ( U e. NrmCVec /\ C e. X /\ A e. X ) -> ( * ` ( C P A ) ) = ( A P C ) )
22 21 3com23
 |-  ( ( U e. NrmCVec /\ A e. X /\ C e. X ) -> ( * ` ( C P A ) ) = ( A P C ) )
23 22 3adant3r2
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( C P A ) ) = ( A P C ) )
24 23 oveq2d
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( ( * ` B ) x. ( * ` ( C P A ) ) ) = ( ( * ` B ) x. ( A P C ) ) )
25 20 24 eqtrd
 |-  ( ( U e. NrmCVec /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( B x. ( C P A ) ) ) = ( ( * ` B ) x. ( A P C ) ) )
26 8 25 sylan
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( B x. ( C P A ) ) ) = ( ( * ` B ) x. ( A P C ) ) )
27 7 15 26 3eqtr3d
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( A P ( B S C ) ) = ( ( * ` B ) x. ( A P C ) ) )