Metamath Proof Explorer

Theorem mavmulcl

Description: Multiplication of an NxN matrix with an N-dimensional vector results in an N-dimensional vector. (Contributed by AV, 6-Dec-2018) (Revised by AV, 23-Feb-2019) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mavmulcl.a 
|- A = ( N Mat R )
mavmulcl.m 
|- .X. = ( R maVecMul <. N , N >. )
mavmulcl.b 
|- B = ( Base ` R )
mavmulcl.t 
|- .x. = ( .r ` R )
mavmulcl.r 
|- ( ph -> R e. Ring )
mavmulcl.n 
|- ( ph -> N e. Fin )
mavmulcl.x 
|- ( ph -> X e. ( Base ` A ) )
mavmulcl.y 
|- ( ph -> Y e. ( B ^m N ) )
Assertion mavmulcl 
|- ( ph -> ( X .X. Y ) e. ( B ^m N ) )

Proof

Step Hyp Ref Expression
1 mavmulcl.a 
 |-  A = ( N Mat R )
2 mavmulcl.m 
 |-  .X. = ( R maVecMul <. N , N >. )
3 mavmulcl.b 
 |-  B = ( Base ` R )
4 mavmulcl.t 
 |-  .x. = ( .r ` R )
5 mavmulcl.r 
 |-  ( ph -> R e. Ring )
6 mavmulcl.n 
 |-  ( ph -> N e. Fin )
7 mavmulcl.x 
 |-  ( ph -> X e. ( Base ` A ) )
8 mavmulcl.y 
 |-  ( ph -> Y e. ( B ^m N ) )
9 1 2 3 4 5 6 7 8 mavmulval 
 |-  ( ph -> ( X .X. Y ) = ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) )
10 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
11 5 10 syl 
 |-  ( ph -> R e. CMnd )
12 11 adantr 
 |-  ( ( ph /\ i e. N ) -> R e. CMnd )
13 6 adantr 
 |-  ( ( ph /\ i e. N ) -> N e. Fin )
14 5 ad2antrr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> R e. Ring )
15 1 3 matbas2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
16 6 5 15 syl2anc 
 |-  ( ph -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
17 7 16 eleqtrrd 
 |-  ( ph -> X e. ( B ^m ( N X. N ) ) )
18 elmapi 
 |-  ( X e. ( B ^m ( N X. N ) ) -> X : ( N X. N ) --> B )
19 17 18 syl 
 |-  ( ph -> X : ( N X. N ) --> B )
20 19 ad2antrr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> X : ( N X. N ) --> B )
21 simpr 
 |-  ( ( ph /\ i e. N ) -> i e. N )
22 21 adantr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> i e. N )
23 simpr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> j e. N )
24 20 22 23 fovrnd 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( i X j ) e. B )
25 elmapi 
 |-  ( Y e. ( B ^m N ) -> Y : N --> B )
26 8 25 syl 
 |-  ( ph -> Y : N --> B )
27 26 ad2antrr 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> Y : N --> B )
28 27 23 ffvelrnd 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( Y ` j ) e. B )
29 3 4 ringcl 
 |-  ( ( R e. Ring /\ ( i X j ) e. B /\ ( Y ` j ) e. B ) -> ( ( i X j ) .x. ( Y ` j ) ) e. B )
30 14 24 28 29 syl3anc 
 |-  ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( i X j ) .x. ( Y ` j ) ) e. B )
31 30 ralrimiva 
 |-  ( ( ph /\ i e. N ) -> A. j e. N ( ( i X j ) .x. ( Y ` j ) ) e. B )
32 3 12 13 31 gsummptcl 
 |-  ( ( ph /\ i e. N ) -> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) e. B )
33 32 ralrimiva 
 |-  ( ph -> A. i e. N ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) e. B )
34 eqid 
 |-  ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) = ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) )
35 34 fmpt 
 |-  ( A. i e. N ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) e. B <-> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) : N --> B )
36 3 fvexi 
 |-  B e. _V
37 elmapg 
 |-  ( ( B e. _V /\ N e. Fin ) -> ( ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) e. ( B ^m N ) <-> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) : N --> B ) )
38 36 6 37 sylancr 
 |-  ( ph -> ( ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) e. ( B ^m N ) <-> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) : N --> B ) )
39 35 38 bitr4id 
 |-  ( ph -> ( A. i e. N ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) e. B <-> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) e. ( B ^m N ) ) )
40 33 39 mpbid 
 |-  ( ph -> ( i e. N |-> ( R gsum ( j e. N |-> ( ( i X j ) .x. ( Y ` j ) ) ) ) ) e. ( B ^m N ) )
41 9 40 eqeltrd 
 |-  ( ph -> ( X .X. Y ) e. ( B ^m N ) )