Metamath Proof Explorer

Theorem cphassi

Description: Associative law for the first argument of an inner product with scalar _ i . (Contributed by AV, 17-Oct-2021)

Ref Expression
Hypotheses cphassi.x 
|- X = ( Base ` W )
cphassi.s 
|- .x. = ( .s ` W )
cphassi.i 
|- ., = ( .i ` W )
cphassi.f 
|- F = ( Scalar ` W )
cphassi.k 
|- K = ( Base ` F )
Assertion cphassi 
|- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i .x. B ) ., A ) = ( _i x. ( B ., A ) ) )

Proof

Step Hyp Ref Expression
1 cphassi.x 
 |-  X = ( Base ` W )
2 cphassi.s 
 |-  .x. = ( .s ` W )
3 cphassi.i 
 |-  ., = ( .i ` W )
4 cphassi.f 
 |-  F = ( Scalar ` W )
5 cphassi.k 
 |-  K = ( Base ` F )
6 simp1l 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> W e. CPreHil )
7 simp1r 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> _i e. K )
8 simp3 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> B e. X )
9 simp2 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> A e. X )
10 3 1 4 5 2 cphass 
 |-  ( ( W e. CPreHil /\ ( _i e. K /\ B e. X /\ A e. X ) ) -> ( ( _i .x. B ) ., A ) = ( _i x. ( B ., A ) ) )
11 6 7 8 9 10 syl13anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i .x. B ) ., A ) = ( _i x. ( B ., A ) ) )