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 โŠข ๐ด = ( ๐‘ Mat ๐‘… )
mavmulcl.m โŠข ร— = ( ๐‘… maVecMul โŸจ ๐‘ , ๐‘ โŸฉ )
mavmulcl.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
mavmulcl.t โŠข ยท = ( .r โ€˜ ๐‘… )
mavmulcl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
mavmulcl.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ Fin )
mavmulcl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ๐ด ) )
mavmulcl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ( ๐ต โ†‘m ๐‘ ) )
Assertion mavmulcl ( ๐œ‘ โ†’ ( ๐‘‹ ร— ๐‘Œ ) โˆˆ ( ๐ต โ†‘m ๐‘ ) )

Proof

Step Hyp Ref Expression
1 mavmulcl.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 mavmulcl.m โŠข ร— = ( ๐‘… maVecMul โŸจ ๐‘ , ๐‘ โŸฉ )
3 mavmulcl.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
4 mavmulcl.t โŠข ยท = ( .r โ€˜ ๐‘… )
5 mavmulcl.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
6 mavmulcl.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ Fin )
7 mavmulcl.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ๐ด ) )
8 mavmulcl.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ( ๐ต โ†‘m ๐‘ ) )
9 1 2 3 4 5 6 7 8 mavmulval โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ร— ๐‘Œ ) = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) )
10 ringcmn โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘… โˆˆ CMnd )
11 5 10 syl โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ CMnd )
12 11 adantr โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โ†’ ๐‘… โˆˆ CMnd )
13 6 adantr โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โ†’ ๐‘ โˆˆ Fin )
14 5 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ๐‘… โˆˆ Ring )
15 1 3 matbas2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ( ๐ต โ†‘m ( ๐‘ ร— ๐‘ ) ) = ( Base โ€˜ ๐ด ) )
16 6 5 15 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐ต โ†‘m ( ๐‘ ร— ๐‘ ) ) = ( Base โ€˜ ๐ด ) )
17 7 16 eleqtrrd โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ๐ต โ†‘m ( ๐‘ ร— ๐‘ ) ) )
18 elmapi โŠข ( ๐‘‹ โˆˆ ( ๐ต โ†‘m ( ๐‘ ร— ๐‘ ) ) โ†’ ๐‘‹ : ( ๐‘ ร— ๐‘ ) โŸถ ๐ต )
19 17 18 syl โŠข ( ๐œ‘ โ†’ ๐‘‹ : ( ๐‘ ร— ๐‘ ) โŸถ ๐ต )
20 19 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ๐‘‹ : ( ๐‘ ร— ๐‘ ) โŸถ ๐ต )
21 simpr โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โ†’ ๐‘– โˆˆ ๐‘ )
22 21 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ๐‘– โˆˆ ๐‘ )
23 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ๐‘— โˆˆ ๐‘ )
24 20 22 23 fovcdmd โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ( ๐‘– ๐‘‹ ๐‘— ) โˆˆ ๐ต )
25 elmapi โŠข ( ๐‘Œ โˆˆ ( ๐ต โ†‘m ๐‘ ) โ†’ ๐‘Œ : ๐‘ โŸถ ๐ต )
26 8 25 syl โŠข ( ๐œ‘ โ†’ ๐‘Œ : ๐‘ โŸถ ๐ต )
27 26 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ๐‘Œ : ๐‘ โŸถ ๐ต )
28 27 23 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ( ๐‘Œ โ€˜ ๐‘— ) โˆˆ ๐ต )
29 3 4 ringcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘– ๐‘‹ ๐‘— ) โˆˆ ๐ต โˆง ( ๐‘Œ โ€˜ ๐‘— ) โˆˆ ๐ต ) โ†’ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) โˆˆ ๐ต )
30 14 24 28 29 syl3anc โŠข ( ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โˆง ๐‘— โˆˆ ๐‘ ) โ†’ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) โˆˆ ๐ต )
31 30 ralrimiva โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โ†’ โˆ€ ๐‘— โˆˆ ๐‘ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) โˆˆ ๐ต )
32 3 12 13 31 gsummptcl โŠข ( ( ๐œ‘ โˆง ๐‘– โˆˆ ๐‘ ) โ†’ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) โˆˆ ๐ต )
33 32 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘– โˆˆ ๐‘ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) โˆˆ ๐ต )
34 eqid โŠข ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) = ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) )
35 34 fmpt โŠข ( โˆ€ ๐‘– โˆˆ ๐‘ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) โˆˆ ๐ต โ†” ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) : ๐‘ โŸถ ๐ต )
36 3 fvexi โŠข ๐ต โˆˆ V
37 elmapg โŠข ( ( ๐ต โˆˆ V โˆง ๐‘ โˆˆ Fin ) โ†’ ( ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) โˆˆ ( ๐ต โ†‘m ๐‘ ) โ†” ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) : ๐‘ โŸถ ๐ต ) )
38 36 6 37 sylancr โŠข ( ๐œ‘ โ†’ ( ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) โˆˆ ( ๐ต โ†‘m ๐‘ ) โ†” ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) : ๐‘ โŸถ ๐ต ) )
39 35 38 bitr4id โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘– โˆˆ ๐‘ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) โˆˆ ๐ต โ†” ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) โˆˆ ( ๐ต โ†‘m ๐‘ ) ) )
40 33 39 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘– โˆˆ ๐‘ โ†ฆ ( ๐‘… ฮฃg ( ๐‘— โˆˆ ๐‘ โ†ฆ ( ( ๐‘– ๐‘‹ ๐‘— ) ยท ( ๐‘Œ โ€˜ ๐‘— ) ) ) ) ) โˆˆ ( ๐ต โ†‘m ๐‘ ) )
41 9 40 eqeltrd โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ร— ๐‘Œ ) โˆˆ ( ๐ต โ†‘m ๐‘ ) )