Step | Hyp | Ref
| Expression |
1 | | mavmulcl.a |
. . 3
โข ๐ด = (๐ Mat ๐
) |
2 | | mavmulcl.m |
. . 3
โข ร =
(๐
maVecMul โจ๐, ๐โฉ) |
3 | | mavmulcl.b |
. . 3
โข ๐ต = (Baseโ๐
) |
4 | | mavmulcl.t |
. . 3
โข ยท =
(.rโ๐
) |
5 | | mavmulcl.r |
. . 3
โข (๐ โ ๐
โ Ring) |
6 | | mavmulcl.n |
. . 3
โข (๐ โ ๐ โ Fin) |
7 | | mavmulcl.x |
. . 3
โข (๐ โ ๐ โ (Baseโ๐ด)) |
8 | | mavmulcl.y |
. . 3
โข (๐ โ ๐ โ (๐ต โm ๐)) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | mavmulval 21917 |
. 2
โข (๐ โ (๐ ร ๐) = (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐)))))) |
10 | | ringcmn 20011 |
. . . . . . 7
โข (๐
โ Ring โ ๐
โ CMnd) |
11 | 5, 10 | syl 17 |
. . . . . 6
โข (๐ โ ๐
โ CMnd) |
12 | 11 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐
โ CMnd) |
13 | 6 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐ โ Fin) |
14 | 5 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐
โ Ring) |
15 | 1, 3 | matbas2 21793 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ต โm (๐ ร ๐)) = (Baseโ๐ด)) |
16 | 6, 5, 15 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐ต โm (๐ ร ๐)) = (Baseโ๐ด)) |
17 | 7, 16 | eleqtrrd 2837 |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) |
18 | | elmapi 8793 |
. . . . . . . . . 10
โข (๐ โ (๐ต โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ๐ต) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐:(๐ ร ๐)โถ๐ต) |
20 | 19 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ๐ต) |
21 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐) |
22 | 21 | adantr 482 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
23 | | simpr 486 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
24 | 20, 22, 23 | fovcdmd 7530 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐๐๐) โ ๐ต) |
25 | | elmapi 8793 |
. . . . . . . . . 10
โข (๐ โ (๐ต โm ๐) โ ๐:๐โถ๐ต) |
26 | 8, 25 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐:๐โถ๐ต) |
27 | 26 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐:๐โถ๐ต) |
28 | 27, 23 | ffvelcdmd 7040 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ๐) โ ๐ต) |
29 | 3, 4 | ringcl 19989 |
. . . . . . 7
โข ((๐
โ Ring โง (๐๐๐) โ ๐ต โง (๐โ๐) โ ๐ต) โ ((๐๐๐) ยท (๐โ๐)) โ ๐ต) |
30 | 14, 24, 28, 29 | syl3anc 1372 |
. . . . . 6
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐) ยท (๐โ๐)) โ ๐ต) |
31 | 30 | ralrimiva 3140 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ โ๐ โ ๐ ((๐๐๐) ยท (๐โ๐)) โ ๐ต) |
32 | 3, 12, 13, 31 | gsummptcl 19752 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐)))) โ ๐ต) |
33 | 32 | ralrimiva 3140 |
. . 3
โข (๐ โ โ๐ โ ๐ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐)))) โ ๐ต) |
34 | | eqid 2733 |
. . . . 5
โข (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))) = (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))) |
35 | 34 | fmpt 7062 |
. . . 4
โข
(โ๐ โ
๐ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐)))) โ ๐ต โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))):๐โถ๐ต) |
36 | 3 | fvexi 6860 |
. . . . 5
โข ๐ต โ V |
37 | | elmapg 8784 |
. . . . 5
โข ((๐ต โ V โง ๐ โ Fin) โ ((๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))) โ (๐ต โm ๐) โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))):๐โถ๐ต)) |
38 | 36, 6, 37 | sylancr 588 |
. . . 4
โข (๐ โ ((๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))) โ (๐ต โm ๐) โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))):๐โถ๐ต)) |
39 | 35, 38 | bitr4id 290 |
. . 3
โข (๐ โ (โ๐ โ ๐ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐)))) โ ๐ต โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))) โ (๐ต โm ๐))) |
40 | 33, 39 | mpbid 231 |
. 2
โข (๐ โ (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐) ยท (๐โ๐))))) โ (๐ต โm ๐)) |
41 | 9, 40 | eqeltrd 2834 |
1
โข (๐ โ (๐ ร ๐) โ (๐ต โm ๐)) |