Step |
Hyp |
Ref |
Expression |
1 |
|
frlmvscaval.y |
โข ๐ = ( ๐
freeLMod ๐ผ ) |
2 |
|
frlmvscaval.b |
โข ๐ต = ( Base โ ๐ ) |
3 |
|
frlmvscaval.k |
โข ๐พ = ( Base โ ๐
) |
4 |
|
frlmvscaval.i |
โข ( ๐ โ ๐ผ โ ๐ ) |
5 |
|
frlmvscaval.a |
โข ( ๐ โ ๐ด โ ๐พ ) |
6 |
|
frlmvscaval.x |
โข ( ๐ โ ๐ โ ๐ต ) |
7 |
|
frlmvscaval.j |
โข ( ๐ โ ๐ฝ โ ๐ผ ) |
8 |
|
frlmvscaval.v |
โข โ = ( ยท๐ โ ๐ ) |
9 |
|
frlmvscaval.t |
โข ยท = ( .r โ ๐
) |
10 |
1 2 3 4 5 6 8 9
|
frlmvscafval |
โข ( ๐ โ ( ๐ด โ ๐ ) = ( ( ๐ผ ร { ๐ด } ) โf ยท ๐ ) ) |
11 |
10
|
fveq1d |
โข ( ๐ โ ( ( ๐ด โ ๐ ) โ ๐ฝ ) = ( ( ( ๐ผ ร { ๐ด } ) โf ยท ๐ ) โ ๐ฝ ) ) |
12 |
|
fnconstg |
โข ( ๐ด โ ๐พ โ ( ๐ผ ร { ๐ด } ) Fn ๐ผ ) |
13 |
5 12
|
syl |
โข ( ๐ โ ( ๐ผ ร { ๐ด } ) Fn ๐ผ ) |
14 |
1 3 2
|
frlmbasf |
โข ( ( ๐ผ โ ๐ โง ๐ โ ๐ต ) โ ๐ : ๐ผ โถ ๐พ ) |
15 |
4 6 14
|
syl2anc |
โข ( ๐ โ ๐ : ๐ผ โถ ๐พ ) |
16 |
15
|
ffnd |
โข ( ๐ โ ๐ Fn ๐ผ ) |
17 |
|
fnfvof |
โข ( ( ( ( ๐ผ ร { ๐ด } ) Fn ๐ผ โง ๐ Fn ๐ผ ) โง ( ๐ผ โ ๐ โง ๐ฝ โ ๐ผ ) ) โ ( ( ( ๐ผ ร { ๐ด } ) โf ยท ๐ ) โ ๐ฝ ) = ( ( ( ๐ผ ร { ๐ด } ) โ ๐ฝ ) ยท ( ๐ โ ๐ฝ ) ) ) |
18 |
13 16 4 7 17
|
syl22anc |
โข ( ๐ โ ( ( ( ๐ผ ร { ๐ด } ) โf ยท ๐ ) โ ๐ฝ ) = ( ( ( ๐ผ ร { ๐ด } ) โ ๐ฝ ) ยท ( ๐ โ ๐ฝ ) ) ) |
19 |
|
fvconst2g |
โข ( ( ๐ด โ ๐พ โง ๐ฝ โ ๐ผ ) โ ( ( ๐ผ ร { ๐ด } ) โ ๐ฝ ) = ๐ด ) |
20 |
5 7 19
|
syl2anc |
โข ( ๐ โ ( ( ๐ผ ร { ๐ด } ) โ ๐ฝ ) = ๐ด ) |
21 |
20
|
oveq1d |
โข ( ๐ โ ( ( ( ๐ผ ร { ๐ด } ) โ ๐ฝ ) ยท ( ๐ โ ๐ฝ ) ) = ( ๐ด ยท ( ๐ โ ๐ฝ ) ) ) |
22 |
11 18 21
|
3eqtrd |
โข ( ๐ โ ( ( ๐ด โ ๐ ) โ ๐ฝ ) = ( ๐ด ยท ( ๐ โ ๐ฝ ) ) ) |