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 ๐ ) ) |