Metamath Proof Explorer


Theorem asclmul2

Description: Right multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses asclmul1.a A=algScW
asclmul1.f F=ScalarW
asclmul1.k K=BaseF
asclmul1.v V=BaseW
asclmul1.t ×˙=W
asclmul1.s ·˙=W
Assertion asclmul2 WAssAlgRKXVX×˙AR=R·˙X

Proof

Step Hyp Ref Expression
1 asclmul1.a A=algScW
2 asclmul1.f F=ScalarW
3 asclmul1.k K=BaseF
4 asclmul1.v V=BaseW
5 asclmul1.t ×˙=W
6 asclmul1.s ·˙=W
7 eqid 1W=1W
8 1 2 3 6 7 asclval RKAR=R·˙1W
9 8 3ad2ant2 WAssAlgRKXVAR=R·˙1W
10 9 oveq2d WAssAlgRKXVX×˙AR=X×˙R·˙1W
11 simp1 WAssAlgRKXVWAssAlg
12 simp2 WAssAlgRKXVRK
13 simp3 WAssAlgRKXVXV
14 assaring WAssAlgWRing
15 14 3ad2ant1 WAssAlgRKXVWRing
16 4 7 ringidcl WRing1WV
17 15 16 syl WAssAlgRKXV1WV
18 4 2 3 6 5 assaassr WAssAlgRKXV1WVX×˙R·˙1W=R·˙X×˙1W
19 11 12 13 17 18 syl13anc WAssAlgRKXVX×˙R·˙1W=R·˙X×˙1W
20 4 5 7 ringridm WRingXVX×˙1W=X
21 15 13 20 syl2anc WAssAlgRKXVX×˙1W=X
22 21 oveq2d WAssAlgRKXVR·˙X×˙1W=R·˙X
23 10 19 22 3eqtrd WAssAlgRKXVX×˙AR=R·˙X