Metamath Proof Explorer

Theorem cphassir

Description: "Associative" law for the second 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 cphassir 
|- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., ( _i .x. B ) ) = ( -u _i x. ( A ., B ) ) )

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 simp2 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> A e. X )
9 simp3 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> B e. X )
10 3 1 4 5 2 cphassr 
 |-  ( ( W e. CPreHil /\ ( _i e. K /\ A e. X /\ B e. X ) ) -> ( A ., ( _i .x. B ) ) = ( ( * ` _i ) x. ( A ., B ) ) )
11 6 7 8 9 10 syl13anc 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., ( _i .x. B ) ) = ( ( * ` _i ) x. ( A ., B ) ) )
12 cji 
 |-  ( * ` _i ) = -u _i
13 12 oveq1i 
 |-  ( ( * ` _i ) x. ( A ., B ) ) = ( -u _i x. ( A ., B ) )
14 11 13 eqtrdi 
 |-  ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., ( _i .x. B ) ) = ( -u _i x. ( A ., B ) ) )