Metamath Proof Explorer

Theorem clmvscom

Description: Commutative law for the scalar product. (Contributed by NM, 14-Feb-2008) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses clmvscl.v 
|- V = ( Base ` W )
clmvscl.f 
|- F = ( Scalar ` W )
clmvscl.s 
|- .x. = ( .s ` W )
clmvscl.k 
|- K = ( Base ` F )
Assertion clmvscom 
|- ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( Q .x. ( R .x. X ) ) = ( R .x. ( Q .x. X ) ) )

Proof

Step Hyp Ref Expression
1 clmvscl.v 
 |-  V = ( Base ` W )
2 clmvscl.f 
 |-  F = ( Scalar ` W )
3 clmvscl.s 
 |-  .x. = ( .s ` W )
4 clmvscl.k 
 |-  K = ( Base ` F )
5 ssel 
 |-  ( K C_ CC -> ( Q e. K -> Q e. CC ) )
6 ssel 
 |-  ( K C_ CC -> ( R e. K -> R e. CC ) )
7 5 6 anim12d 
 |-  ( K C_ CC -> ( ( Q e. K /\ R e. K ) -> ( Q e. CC /\ R e. CC ) ) )
8 2 4 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
9 7 8 syl11 
 |-  ( ( Q e. K /\ R e. K ) -> ( W e. CMod -> ( Q e. CC /\ R e. CC ) ) )
10 9 3adant3 
 |-  ( ( Q e. K /\ R e. K /\ X e. V ) -> ( W e. CMod -> ( Q e. CC /\ R e. CC ) ) )
11 10 impcom 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( Q e. CC /\ R e. CC ) )
12 mulcom 
 |-  ( ( Q e. CC /\ R e. CC ) -> ( Q x. R ) = ( R x. Q ) )
13 11 12 syl 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( Q x. R ) = ( R x. Q ) )
14 13 oveq1d 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q x. R ) .x. X ) = ( ( R x. Q ) .x. X ) )
15 1 2 3 4 clmvsass 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q x. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
16 3ancoma 
 |-  ( ( Q e. K /\ R e. K /\ X e. V ) <-> ( R e. K /\ Q e. K /\ X e. V ) )
17 1 2 3 4 clmvsass 
 |-  ( ( W e. CMod /\ ( R e. K /\ Q e. K /\ X e. V ) ) -> ( ( R x. Q ) .x. X ) = ( R .x. ( Q .x. X ) ) )
18 16 17 sylan2b 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( R x. Q ) .x. X ) = ( R .x. ( Q .x. X ) ) )
19 14 15 18 3eqtr3d 
 |-  ( ( W e. CMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( Q .x. ( R .x. X ) ) = ( R .x. ( Q .x. X ) ) )