Step | Hyp | Ref
| Expression |
1 | | 1mavmul.a |
. . . 4
โข ๐ด = (๐ Mat ๐
) |
2 | | 1mavmul.t |
. . . 4
โข ยท =
(๐
maVecMul โจ๐, ๐โฉ) |
3 | | 1mavmul.b |
. . . 4
โข ๐ต = (Baseโ๐
) |
4 | | eqid 2732 |
. . . 4
โข
(.rโ๐
) = (.rโ๐
) |
5 | | 1mavmul.r |
. . . 4
โข (๐ โ ๐
โ Ring) |
6 | | 1mavmul.n |
. . . 4
โข (๐ โ ๐ โ Fin) |
7 | | mavmulass.m |
. . . . . 6
โข ร =
(๐
maMul โจ๐, ๐, ๐โฉ) |
8 | | mavmulass.x |
. . . . . . 7
โข (๐ โ ๐ โ (Baseโ๐ด)) |
9 | 1, 3 | matbas2 21914 |
. . . . . . . 8
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ต โm (๐ ร ๐)) = (Baseโ๐ด)) |
10 | 6, 5, 9 | syl2anc 584 |
. . . . . . 7
โข (๐ โ (๐ต โm (๐ ร ๐)) = (Baseโ๐ด)) |
11 | 8, 10 | eleqtrrd 2836 |
. . . . . 6
โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) |
12 | | mavmulass.z |
. . . . . . 7
โข (๐ โ ๐ โ (Baseโ๐ด)) |
13 | 12, 10 | eleqtrrd 2836 |
. . . . . 6
โข (๐ โ ๐ โ (๐ต โm (๐ ร ๐))) |
14 | 3, 5, 7, 6, 6, 6, 11, 13 | mamucl 21892 |
. . . . 5
โข (๐ โ (๐ ร ๐) โ (๐ต โm (๐ ร ๐))) |
15 | 14, 10 | eleqtrd 2835 |
. . . 4
โข (๐ โ (๐ ร ๐) โ (Baseโ๐ด)) |
16 | | 1mavmul.y |
. . . 4
โข (๐ โ ๐ โ (๐ต โm ๐)) |
17 | 1, 2, 3, 4, 5, 6, 15, 16 | mavmulcl 22040 |
. . 3
โข (๐ โ ((๐ ร ๐) ยท ๐) โ (๐ต โm ๐)) |
18 | | elmapi 8839 |
. . 3
โข (((๐ ร ๐) ยท ๐) โ (๐ต โm ๐) โ ((๐ ร ๐) ยท ๐):๐โถ๐ต) |
19 | | ffn 6714 |
. . 3
โข (((๐ ร ๐) ยท ๐):๐โถ๐ต โ ((๐ ร ๐) ยท ๐) Fn ๐) |
20 | 17, 18, 19 | 3syl 18 |
. 2
โข (๐ โ ((๐ ร ๐) ยท ๐) Fn ๐) |
21 | 1, 2, 3, 4, 5, 6, 12, 16 | mavmulcl 22040 |
. . . 4
โข (๐ โ (๐ ยท ๐) โ (๐ต โm ๐)) |
22 | 1, 2, 3, 4, 5, 6, 8, 21 | mavmulcl 22040 |
. . 3
โข (๐ โ (๐ ยท (๐ ยท ๐)) โ (๐ต โm ๐)) |
23 | | elmapi 8839 |
. . 3
โข ((๐ ยท (๐ ยท ๐)) โ (๐ต โm ๐) โ (๐ ยท (๐ ยท ๐)):๐โถ๐ต) |
24 | | ffn 6714 |
. . 3
โข ((๐ ยท (๐ ยท ๐)):๐โถ๐ต โ (๐ ยท (๐ ยท ๐)) Fn ๐) |
25 | 22, 23, 24 | 3syl 18 |
. 2
โข (๐ โ (๐ ยท (๐ ยท ๐)) Fn ๐) |
26 | 5 | ringcmnd 20094 |
. . . . . 6
โข (๐ โ ๐
โ CMnd) |
27 | 26 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐
โ CMnd) |
28 | 6 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ๐ โ Fin) |
29 | 5 | ad2antrr 724 |
. . . . . 6
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐
โ Ring) |
30 | | elmapi 8839 |
. . . . . . . . 9
โข (๐ โ (๐ต โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ๐ต) |
31 | 11, 30 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐:(๐ ร ๐)โถ๐ต) |
32 | 31 | ad2antrr 724 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐:(๐ ร ๐)โถ๐ต) |
33 | | simplr 767 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
34 | | simprr 771 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
35 | 32, 33, 34 | fovcdmd 7575 |
. . . . . 6
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐) โ ๐ต) |
36 | | elmapi 8839 |
. . . . . . . . . 10
โข (๐ โ (๐ต โm (๐ ร ๐)) โ ๐:(๐ ร ๐)โถ๐ต) |
37 | 13, 36 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐:(๐ ร ๐)โถ๐ต) |
38 | 37 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐:(๐ ร ๐)โถ๐ต) |
39 | | simprl 769 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
40 | 38, 34, 39 | fovcdmd 7575 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐) โ ๐ต) |
41 | | elmapi 8839 |
. . . . . . . . . 10
โข (๐ โ (๐ต โm ๐) โ ๐:๐โถ๐ต) |
42 | | ffvelcdm 7080 |
. . . . . . . . . . 11
โข ((๐:๐โถ๐ต โง ๐ โ ๐) โ (๐โ๐) โ ๐ต) |
43 | 42 | ex 413 |
. . . . . . . . . 10
โข (๐:๐โถ๐ต โ (๐ โ ๐ โ (๐โ๐) โ ๐ต)) |
44 | 16, 41, 43 | 3syl 18 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐ โ (๐โ๐) โ ๐ต)) |
45 | 44 | imp 407 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐) โ (๐โ๐) โ ๐ต) |
46 | 45 | ad2ant2r 745 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐โ๐) โ ๐ต) |
47 | 3, 4, 29, 40, 46 | ringcld 20073 |
. . . . . 6
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐๐๐)(.rโ๐
)(๐โ๐)) โ ๐ต) |
48 | 3, 4, 29, 35, 47 | ringcld 20073 |
. . . . 5
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐))) โ ๐ต) |
49 | 3, 27, 28, 28, 48 | gsumcom3fi 19841 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐))))))) = (๐
ฮฃg (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))))))) |
50 | 5 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐
โ Ring) |
51 | 6 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ Fin) |
52 | 11 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ (๐ต โm (๐ ร ๐))) |
53 | 13 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ (๐ต โm (๐ ร ๐))) |
54 | | simplr 767 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
55 | | simpr 485 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
56 | 7, 3, 4, 50, 51, 51, 51, 52, 53, 54, 55 | mamufv 21880 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐(๐ ร ๐)๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐๐๐))))) |
57 | 56 | oveq1d 7420 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐(๐ ร ๐)๐)(.rโ๐
)(๐โ๐)) = ((๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐๐๐))))(.rโ๐
)(๐โ๐))) |
58 | | eqid 2732 |
. . . . . . . 8
โข
(0gโ๐
) = (0gโ๐
) |
59 | 45 | adantlr 713 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ๐) โ ๐ต) |
60 | 5 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐) โ ๐
โ Ring) |
61 | 60 | ad2antrr 724 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐
โ Ring) |
62 | 31 | ad2antrr 724 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ๐ต) |
63 | | simplr 767 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
64 | | simpr 485 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
65 | 62, 63, 64 | fovcdmd 7575 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐๐๐) โ ๐ต) |
66 | 65 | adantlr 713 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ (๐๐๐) โ ๐ต) |
67 | 37 | adantr 481 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ๐ต) |
68 | 67 | ad2antrr 724 |
. . . . . . . . . 10
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ๐ต) |
69 | | simpr 485 |
. . . . . . . . . 10
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
70 | | simplr 767 |
. . . . . . . . . 10
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
71 | 68, 69, 70 | fovcdmd 7575 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ (๐๐๐) โ ๐ต) |
72 | 3, 4, 61, 66, 71 | ringcld 20073 |
. . . . . . . 8
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐)(.rโ๐
)(๐๐๐)) โ ๐ต) |
73 | | eqid 2732 |
. . . . . . . . 9
โข (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐๐๐))) = (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐๐๐))) |
74 | | ovexd 7440 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐)(.rโ๐
)(๐๐๐)) โ V) |
75 | | fvexd 6903 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (0gโ๐
) โ V) |
76 | 73, 51, 74, 75 | fsuppmptdm 9370 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐๐๐))) finSupp (0gโ๐
)) |
77 | 3, 58, 4, 50, 51, 59, 72, 76 | gsummulc1 20121 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ (((๐๐๐)(.rโ๐
)(๐๐๐))(.rโ๐
)(๐โ๐)))) = ((๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐๐๐))))(.rโ๐
)(๐โ๐))) |
78 | 3, 4 | ringass 20069 |
. . . . . . . . . . 11
โข ((๐
โ Ring โง ((๐๐๐) โ ๐ต โง (๐๐๐) โ ๐ต โง (๐โ๐) โ ๐ต)) โ (((๐๐๐)(.rโ๐
)(๐๐๐))(.rโ๐
)(๐โ๐)) = ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))) |
79 | 29, 35, 40, 46, 78 | syl13anc 1372 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐๐๐)(.rโ๐
)(๐๐๐))(.rโ๐
)(๐โ๐)) = ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))) |
80 | 79 | anassrs 468 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ (((๐๐๐)(.rโ๐
)(๐๐๐))(.rโ๐
)(๐โ๐)) = ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))) |
81 | 80 | mpteq2dva 5247 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ โ ๐ โฆ (((๐๐๐)(.rโ๐
)(๐๐๐))(.rโ๐
)(๐โ๐))) = (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐))))) |
82 | 81 | oveq2d 7421 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ (((๐๐๐)(.rโ๐
)(๐๐๐))(.rโ๐
)(๐โ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))))) |
83 | 57, 77, 82 | 3eqtr2d 2778 |
. . . . . 6
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐(๐ ร ๐)๐)(.rโ๐
)(๐โ๐)) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))))) |
84 | 83 | mpteq2dva 5247 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โฆ ((๐(๐ ร ๐)๐)(.rโ๐
)(๐โ๐))) = (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐))))))) |
85 | 84 | oveq2d 7421 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐(๐ ร ๐)๐)(.rโ๐
)(๐โ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))))))) |
86 | 5 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐
โ Ring) |
87 | 6 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ Fin) |
88 | 12 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ (Baseโ๐ด)) |
89 | 16 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ (๐ต โm ๐)) |
90 | 1, 2, 3, 4, 86, 87, 88, 89, 64 | mavmulfv 22039 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐ ยท ๐)โ๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))))) |
91 | 90 | oveq2d 7421 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐)(.rโ๐
)((๐ ยท ๐)โ๐)) = ((๐๐๐)(.rโ๐
)(๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐)))))) |
92 | 60 | ad2antrr 724 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐
โ Ring) |
93 | 67 | ad2antrr 724 |
. . . . . . . . . 10
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐:(๐ ร ๐)โถ๐ต) |
94 | | simplr 767 |
. . . . . . . . . 10
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
95 | | simpr 485 |
. . . . . . . . . 10
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ๐ โ ๐) |
96 | 93, 94, 95 | fovcdmd 7575 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ (๐๐๐) โ ๐ต) |
97 | 44 | ad2antrr 724 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ โ ๐ โ (๐โ๐) โ ๐ต)) |
98 | 97 | imp 407 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ (๐โ๐) โ ๐ต) |
99 | 3, 4, 92, 96, 98 | ringcld 20073 |
. . . . . . . 8
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐)(.rโ๐
)(๐โ๐)) โ ๐ต) |
100 | | eqid 2732 |
. . . . . . . . 9
โข (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))) = (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))) |
101 | | ovexd 7440 |
. . . . . . . . 9
โข ((((๐ โง ๐ โ ๐) โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐)(.rโ๐
)(๐โ๐)) โ V) |
102 | | fvexd 6903 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (0gโ๐
) โ V) |
103 | 100, 87, 101, 102 | fsuppmptdm 9370 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐))) finSupp (0gโ๐
)) |
104 | 3, 58, 4, 86, 87, 65, 99, 103 | gsummulc2 20122 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐))))) = ((๐๐๐)(.rโ๐
)(๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)(๐โ๐)))))) |
105 | 91, 104 | eqtr4d 2775 |
. . . . . 6
โข (((๐ โง ๐ โ ๐) โง ๐ โ ๐) โ ((๐๐๐)(.rโ๐
)((๐ ยท ๐)โ๐)) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))))) |
106 | 105 | mpteq2dva 5247 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐ ยท ๐)โ๐))) = (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐))))))) |
107 | 106 | oveq2d 7421 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐ ยท ๐)โ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐๐๐)(.rโ๐
)(๐โ๐)))))))) |
108 | 49, 85, 107 | 3eqtr4d 2782 |
. . 3
โข ((๐ โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐(๐ ร ๐)๐)(.rโ๐
)(๐โ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐ ยท ๐)โ๐))))) |
109 | 15 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ ร ๐) โ (Baseโ๐ด)) |
110 | 16 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ๐ โ (๐ต โm ๐)) |
111 | | simpr 485 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐) |
112 | 1, 2, 3, 4, 60, 28, 109, 110, 111 | mavmulfv 22039 |
. . 3
โข ((๐ โง ๐ โ ๐) โ (((๐ ร ๐) ยท ๐)โ๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐(๐ ร ๐)๐)(.rโ๐
)(๐โ๐))))) |
113 | 8 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ ๐ โ (Baseโ๐ด)) |
114 | 21 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ ยท ๐) โ (๐ต โm ๐)) |
115 | 1, 2, 3, 4, 60, 28, 113, 114, 111 | mavmulfv 22039 |
. . 3
โข ((๐ โง ๐ โ ๐) โ ((๐ ยท (๐ ยท ๐))โ๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐๐)(.rโ๐
)((๐ ยท ๐)โ๐))))) |
116 | 108, 112,
115 | 3eqtr4d 2782 |
. 2
โข ((๐ โง ๐ โ ๐) โ (((๐ ร ๐) ยท ๐)โ๐) = ((๐ ยท (๐ ยท ๐))โ๐)) |
117 | 20, 25, 116 | eqfnfvd 7032 |
1
โข (๐ โ ((๐ ร ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |