Metamath Proof Explorer

Theorem rmodislmodlem

Description: Lemma for rmodislmod . This is the part of the proof of rmodislmod which requires the scalar ring to be commutative. (Contributed by AV, 3-Dec-2021)

Ref Expression
Hypotheses rmodislmod.v 
|- V = ( Base ` R )
rmodislmod.a 
|- .+ = ( +g ` R )
rmodislmod.s 
|- .x. = ( .s ` R )
rmodislmod.f 
|- F = ( Scalar ` R )
rmodislmod.k 
|- K = ( Base ` F )
rmodislmod.p 
|- .+^ = ( +g ` F )
rmodislmod.t 
|- .X. = ( .r ` F )
rmodislmod.u 
|- .1. = ( 1r ` F )
rmodislmod.r 
|- ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) )
rmodislmod.m 
|- .* = ( s e. K , v e. V |-> ( v .x. s ) )
rmodislmod.l 
|- L = ( R sSet <. ( .s ` ndx ) , .* >. )
Assertion rmodislmodlem 
|- ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .X. b ) .* c ) = ( a .* ( b .* c ) ) )

Proof

Step Hyp Ref Expression
1 rmodislmod.v 
 |-  V = ( Base ` R )
2 rmodislmod.a 
 |-  .+ = ( +g ` R )
3 rmodislmod.s 
 |-  .x. = ( .s ` R )
4 rmodislmod.f 
 |-  F = ( Scalar ` R )
5 rmodislmod.k 
 |-  K = ( Base ` F )
6 rmodislmod.p 
 |-  .+^ = ( +g ` F )
7 rmodislmod.t 
 |-  .X. = ( .r ` F )
8 rmodislmod.u 
 |-  .1. = ( 1r ` F )
9 rmodislmod.r 
 |-  ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) )
10 rmodislmod.m 
 |-  .* = ( s e. K , v e. V |-> ( v .x. s ) )
11 rmodislmod.l 
 |-  L = ( R sSet <. ( .s ` ndx ) , .* >. )
12 simprl 
 |-  ( ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) )
13 12 2ralimi 
 |-  ( A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. x e. V A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) )
14 13 2ralimi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) )
15 ralrot3 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) <-> A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) )
16 1 grpbn0 
 |-  ( R e. Grp -> V =/= (/) )
17 16 3ad2ant1 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> V =/= (/) )
18 9 17 ax-mp 
 |-  V =/= (/)
19 rspn0 
 |-  ( V =/= (/) -> ( A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) -> A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) ) )
20 18 19 ax-mp 
 |-  ( A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) -> A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) )
21 oveq1 
 |-  ( q = b -> ( q .X. r ) = ( b .X. r ) )
22 21 oveq2d 
 |-  ( q = b -> ( w .x. ( q .X. r ) ) = ( w .x. ( b .X. r ) ) )
23 oveq2 
 |-  ( q = b -> ( w .x. q ) = ( w .x. b ) )
24 23 oveq1d 
 |-  ( q = b -> ( ( w .x. q ) .x. r ) = ( ( w .x. b ) .x. r ) )
25 22 24 eqeq12d 
 |-  ( q = b -> ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) <-> ( w .x. ( b .X. r ) ) = ( ( w .x. b ) .x. r ) ) )
26 oveq2 
 |-  ( r = a -> ( b .X. r ) = ( b .X. a ) )
27 26 oveq2d 
 |-  ( r = a -> ( w .x. ( b .X. r ) ) = ( w .x. ( b .X. a ) ) )
28 oveq2 
 |-  ( r = a -> ( ( w .x. b ) .x. r ) = ( ( w .x. b ) .x. a ) )
29 27 28 eqeq12d 
 |-  ( r = a -> ( ( w .x. ( b .X. r ) ) = ( ( w .x. b ) .x. r ) <-> ( w .x. ( b .X. a ) ) = ( ( w .x. b ) .x. a ) ) )
30 oveq1 
 |-  ( w = c -> ( w .x. ( b .X. a ) ) = ( c .x. ( b .X. a ) ) )
31 oveq1 
 |-  ( w = c -> ( w .x. b ) = ( c .x. b ) )
32 31 oveq1d 
 |-  ( w = c -> ( ( w .x. b ) .x. a ) = ( ( c .x. b ) .x. a ) )
33 30 32 eqeq12d 
 |-  ( w = c -> ( ( w .x. ( b .X. a ) ) = ( ( w .x. b ) .x. a ) <-> ( c .x. ( b .X. a ) ) = ( ( c .x. b ) .x. a ) ) )
34 25 29 33 rspc3v 
 |-  ( ( b e. K /\ a e. K /\ c e. V ) -> ( A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) -> ( c .x. ( b .X. a ) ) = ( ( c .x. b ) .x. a ) ) )
35 34 3com12 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) -> ( c .x. ( b .X. a ) ) = ( ( c .x. b ) .x. a ) ) )
36 20 35 syl5com 
 |-  ( A. x e. V A. q e. K A. r e. K A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( b .X. a ) ) = ( ( c .x. b ) .x. a ) ) )
37 15 36 sylbi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( b .X. a ) ) = ( ( c .x. b ) .x. a ) ) )
38 eqcom 
 |-  ( ( ( c .x. b ) .x. a ) = ( c .x. ( b .X. a ) ) <-> ( c .x. ( b .X. a ) ) = ( ( c .x. b ) .x. a ) )
39 37 38 imbitrrdi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( c .x. b ) .x. a ) = ( c .x. ( b .X. a ) ) ) )
40 14 39 syl 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( c .x. b ) .x. a ) = ( c .x. ( b .X. a ) ) ) )
41 40 3ad2ant3 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( c .x. b ) .x. a ) = ( c .x. ( b .X. a ) ) ) )
42 9 41 ax-mp 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( c .x. b ) .x. a ) = ( c .x. ( b .X. a ) ) )
43 42 adantl 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( c .x. b ) .x. a ) = ( c .x. ( b .X. a ) ) )
44 5 7 crngcom 
 |-  ( ( F e. CRing /\ b e. K /\ a e. K ) -> ( b .X. a ) = ( a .X. b ) )
45 44 3expb 
 |-  ( ( F e. CRing /\ ( b e. K /\ a e. K ) ) -> ( b .X. a ) = ( a .X. b ) )
46 45 expcom 
 |-  ( ( b e. K /\ a e. K ) -> ( F e. CRing -> ( b .X. a ) = ( a .X. b ) ) )
47 46 ancoms 
 |-  ( ( a e. K /\ b e. K ) -> ( F e. CRing -> ( b .X. a ) = ( a .X. b ) ) )
48 47 3adant3 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( F e. CRing -> ( b .X. a ) = ( a .X. b ) ) )
49 48 impcom 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( b .X. a ) = ( a .X. b ) )
50 49 oveq2d 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( c .x. ( b .X. a ) ) = ( c .x. ( a .X. b ) ) )
51 43 50 eqtrd 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( c .x. b ) .x. a ) = ( c .x. ( a .X. b ) ) )
52 10 a1i 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> .* = ( s e. K , v e. V |-> ( v .x. s ) ) )
53 oveq12 
 |-  ( ( v = c /\ s = b ) -> ( v .x. s ) = ( c .x. b ) )
54 53 ancoms 
 |-  ( ( s = b /\ v = c ) -> ( v .x. s ) = ( c .x. b ) )
55 54 adantl 
 |-  ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = b /\ v = c ) ) -> ( v .x. s ) = ( c .x. b ) )
56 simp2 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> b e. K )
57 simp3 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> c e. V )
58 ovexd 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. b ) e. _V )
59 52 55 56 57 58 ovmpod 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( b .* c ) = ( c .x. b ) )
60 59 oveq2d 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* ( b .* c ) ) = ( a .* ( c .x. b ) ) )
61 oveq12 
 |-  ( ( v = ( c .x. b ) /\ s = a ) -> ( v .x. s ) = ( ( c .x. b ) .x. a ) )
62 61 ancoms 
 |-  ( ( s = a /\ v = ( c .x. b ) ) -> ( v .x. s ) = ( ( c .x. b ) .x. a ) )
63 62 adantl 
 |-  ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = a /\ v = ( c .x. b ) ) ) -> ( v .x. s ) = ( ( c .x. b ) .x. a ) )
64 simp1 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> a e. K )
65 simpl1 
 |-  ( ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( w .x. r ) e. V )
66 65 2ralimi 
 |-  ( A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. x e. V A. w e. V ( w .x. r ) e. V )
67 66 2ralimi 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V )
68 ringgrp 
 |-  ( F e. Ring -> F e. Grp )
69 5 grpbn0 
 |-  ( F e. Grp -> K =/= (/) )
70 68 69 syl 
 |-  ( F e. Ring -> K =/= (/) )
71 70 3ad2ant2 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> K =/= (/) )
72 9 71 ax-mp 
 |-  K =/= (/)
73 rspn0 
 |-  ( K =/= (/) -> ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V -> A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V ) )
74 72 73 ax-mp 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V -> A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V )
75 ralcom 
 |-  ( A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V <-> A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V )
76 rspn0 
 |-  ( V =/= (/) -> ( A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V -> A. r e. K A. w e. V ( w .x. r ) e. V ) )
77 18 76 ax-mp 
 |-  ( A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V -> A. r e. K A. w e. V ( w .x. r ) e. V )
78 oveq2 
 |-  ( r = b -> ( w .x. r ) = ( w .x. b ) )
79 78 eleq1d 
 |-  ( r = b -> ( ( w .x. r ) e. V <-> ( w .x. b ) e. V ) )
80 31 eleq1d 
 |-  ( w = c -> ( ( w .x. b ) e. V <-> ( c .x. b ) e. V ) )
81 79 80 rspc2v 
 |-  ( ( b e. K /\ c e. V ) -> ( A. r e. K A. w e. V ( w .x. r ) e. V -> ( c .x. b ) e. V ) )
82 77 81 syl5com 
 |-  ( A. x e. V A. r e. K A. w e. V ( w .x. r ) e. V -> ( ( b e. K /\ c e. V ) -> ( c .x. b ) e. V ) )
83 75 82 sylbi 
 |-  ( A. r e. K A. x e. V A. w e. V ( w .x. r ) e. V -> ( ( b e. K /\ c e. V ) -> ( c .x. b ) e. V ) )
84 67 74 83 3syl 
 |-  ( A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) -> ( ( b e. K /\ c e. V ) -> ( c .x. b ) e. V ) )
85 84 3ad2ant3 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( b e. K /\ c e. V ) -> ( c .x. b ) e. V ) )
86 9 85 ax-mp 
 |-  ( ( b e. K /\ c e. V ) -> ( c .x. b ) e. V )
87 86 3adant1 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. b ) e. V )
88 ovexd 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( c .x. b ) .x. a ) e. _V )
89 52 63 64 87 88 ovmpod 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* ( c .x. b ) ) = ( ( c .x. b ) .x. a ) )
90 60 89 eqtrd 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .* ( b .* c ) ) = ( ( c .x. b ) .x. a ) )
91 90 adantl 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( a .* ( b .* c ) ) = ( ( c .x. b ) .x. a ) )
92 oveq12 
 |-  ( ( v = c /\ s = ( a .X. b ) ) -> ( v .x. s ) = ( c .x. ( a .X. b ) ) )
93 92 ancoms 
 |-  ( ( s = ( a .X. b ) /\ v = c ) -> ( v .x. s ) = ( c .x. ( a .X. b ) ) )
94 93 adantl 
 |-  ( ( ( a e. K /\ b e. K /\ c e. V ) /\ ( s = ( a .X. b ) /\ v = c ) ) -> ( v .x. s ) = ( c .x. ( a .X. b ) ) )
95 5 7 ringcl 
 |-  ( ( F e. Ring /\ a e. K /\ b e. K ) -> ( a .X. b ) e. K )
96 95 3expib 
 |-  ( F e. Ring -> ( ( a e. K /\ b e. K ) -> ( a .X. b ) e. K ) )
97 96 3ad2ant2 
 |-  ( ( R e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( w .x. r ) e. V /\ ( ( w .+ x ) .x. r ) = ( ( w .x. r ) .+ ( x .x. r ) ) /\ ( w .x. ( q .+^ r ) ) = ( ( w .x. q ) .+ ( w .x. r ) ) ) /\ ( ( w .x. ( q .X. r ) ) = ( ( w .x. q ) .x. r ) /\ ( w .x. .1. ) = w ) ) ) -> ( ( a e. K /\ b e. K ) -> ( a .X. b ) e. K ) )
98 9 97 ax-mp 
 |-  ( ( a e. K /\ b e. K ) -> ( a .X. b ) e. K )
99 98 3adant3 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( a .X. b ) e. K )
100 ovexd 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( c .x. ( a .X. b ) ) e. _V )
101 52 94 99 57 100 ovmpod 
 |-  ( ( a e. K /\ b e. K /\ c e. V ) -> ( ( a .X. b ) .* c ) = ( c .x. ( a .X. b ) ) )
102 101 adantl 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .X. b ) .* c ) = ( c .x. ( a .X. b ) ) )
103 51 91 102 3eqtr4rd 
 |-  ( ( F e. CRing /\ ( a e. K /\ b e. K /\ c e. V ) ) -> ( ( a .X. b ) .* c ) = ( a .* ( b .* c ) ) )