Step | Hyp | Ref
| Expression |
1 | | mvmumamul1.t |
. . . . . 6
โข ยท =
(๐
maVecMul โจ๐, ๐โฉ) |
2 | | mvmumamul1.b |
. . . . . 6
โข ๐ต = (Baseโ๐
) |
3 | | eqid 2733 |
. . . . . 6
โข
(.rโ๐
) = (.rโ๐
) |
4 | | mvmumamul1.r |
. . . . . . 7
โข (๐ โ ๐
โ Ring) |
5 | 4 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐
โ Ring) |
6 | | mvmumamul1.m |
. . . . . . 7
โข (๐ โ ๐ โ Fin) |
7 | 6 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ โ Fin) |
8 | | mvmumamul1.n |
. . . . . . 7
โข (๐ โ ๐ โ Fin) |
9 | 8 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ โ Fin) |
10 | | mvmumamul1.a |
. . . . . . 7
โข (๐ โ ๐ด โ (๐ต โm (๐ ร ๐))) |
11 | 10 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ด โ (๐ต โm (๐ ร ๐))) |
12 | | mvmumamul1.y |
. . . . . . 7
โข (๐ โ ๐ โ (๐ต โm ๐)) |
13 | 12 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ โ (๐ต โm ๐)) |
14 | | simpr 486 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ โ ๐) |
15 | 1, 2, 3, 5, 7, 9, 11, 13, 14 | mvmulfv 21916 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ ((๐ด ยท ๐)โ๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐โ๐))))) |
16 | 15 | adantlr 714 |
. . . 4
โข (((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โง ๐ โ ๐) โ ((๐ด ยท ๐)โ๐) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐โ๐))))) |
17 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
18 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐๐โ
) = (๐๐โ
)) |
19 | 17, 18 | eqeq12d 2749 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐โ๐) = (๐๐โ
) โ (๐โ๐) = (๐๐โ
))) |
20 | 19 | rspccv 3580 |
. . . . . . . . . 10
โข
(โ๐ โ
๐ (๐โ๐) = (๐๐โ
) โ (๐ โ ๐ โ (๐โ๐) = (๐๐โ
))) |
21 | 20 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โ (๐ โ ๐ โ (๐โ๐) = (๐๐โ
))) |
22 | 21 | imp 408 |
. . . . . . . 8
โข (((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โง ๐ โ ๐) โ (๐โ๐) = (๐๐โ
)) |
23 | 22 | oveq2d 7377 |
. . . . . . 7
โข (((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โง ๐ โ ๐) โ ((๐๐ด๐)(.rโ๐
)(๐โ๐)) = ((๐๐ด๐)(.rโ๐
)(๐๐โ
))) |
24 | 23 | mpteq2dva 5209 |
. . . . . 6
โข ((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โ (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐โ๐))) = (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐๐โ
)))) |
25 | 24 | oveq2d 7377 |
. . . . 5
โข ((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐โ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐๐โ
))))) |
26 | 25 | adantr 482 |
. . . 4
โข (((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐โ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐๐โ
))))) |
27 | | mvmumamul1.x |
. . . . . . 7
โข ร =
(๐
maMul โจ๐, ๐, {โ
}โฉ) |
28 | | snfi 8994 |
. . . . . . . 8
โข {โ
}
โ Fin |
29 | 28 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ {โ
} โ
Fin) |
30 | | mvmumamul1.z |
. . . . . . . 8
โข (๐ โ ๐ โ (๐ต โm (๐ ร {โ
}))) |
31 | 30 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ๐ โ (๐ต โm (๐ ร {โ
}))) |
32 | | 0ex 5268 |
. . . . . . . . 9
โข โ
โ V |
33 | 32 | snid 4626 |
. . . . . . . 8
โข โ
โ {โ
} |
34 | 33 | a1i 11 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ โ
โ
{โ
}) |
35 | 27, 2, 3, 5, 7, 9, 29, 11, 31, 14, 34 | mamufv 21759 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ (๐(๐ด ร ๐)โ
) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐๐โ
))))) |
36 | 35 | eqcomd 2739 |
. . . . 5
โข ((๐ โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐๐โ
)))) = (๐(๐ด ร ๐)โ
)) |
37 | 36 | adantlr 714 |
. . . 4
โข (((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โง ๐ โ ๐) โ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ด๐)(.rโ๐
)(๐๐โ
)))) = (๐(๐ด ร ๐)โ
)) |
38 | 16, 26, 37 | 3eqtrd 2777 |
. . 3
โข (((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โง ๐ โ ๐) โ ((๐ด ยท ๐)โ๐) = (๐(๐ด ร ๐)โ
)) |
39 | 38 | ralrimiva 3140 |
. 2
โข ((๐ โง โ๐ โ ๐ (๐โ๐) = (๐๐โ
)) โ โ๐ โ ๐ ((๐ด ยท ๐)โ๐) = (๐(๐ด ร ๐)โ
)) |
40 | 39 | ex 414 |
1
โข (๐ โ (โ๐ โ ๐ (๐โ๐) = (๐๐โ
) โ โ๐ โ ๐ ((๐ด ยท ๐)โ๐) = (๐(๐ด ร ๐)โ
))) |