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 = ( .sOLD ` U )
ipass.7 
|- P = ( .iOLD ` U )
Assertion dipassr2 
|- ( ( 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 cjcl 
 |-  ( B e. CC -> ( * ` B ) e. CC )
5 1 2 3 dipassr 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ ( * ` B ) e. CC /\ C e. X ) ) -> ( A P ( ( * ` B ) S C ) ) = ( ( * ` ( * ` B ) ) x. ( A P C ) ) )
6 4 5 syl3anr2 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( A P ( ( * ` B ) S C ) ) = ( ( * ` ( * ` B ) ) x. ( A P C ) ) )
7 cjcj 
 |-  ( B e. CC -> ( * ` ( * ` B ) ) = B )
8 7 3ad2ant2 
 |-  ( ( A e. X /\ B e. CC /\ C e. X ) -> ( * ` ( * ` B ) ) = B )
9 8 adantl 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( * ` ( * ` B ) ) = B )
10 9 oveq1d 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( ( * ` ( * ` B ) ) x. ( A P C ) ) = ( B x. ( A P C ) ) )
11 6 10 eqtrd 
 |-  ( ( U e. CPreHilOLD /\ ( A e. X /\ B e. CC /\ C e. X ) ) -> ( A P ( ( * ` B ) S C ) ) = ( B x. ( A P C ) ) )