This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )