Metamath Proof Explorer


Theorem frlmvscavalb

Description: Scalar multiplication in a free module at the coordinates. (Contributed by AV, 16-Jan-2023)

Ref Expression
Hypotheses frlmplusgvalb.f F=RfreeLModI
frlmplusgvalb.b B=BaseF
frlmplusgvalb.i φIW
frlmplusgvalb.x φXB
frlmplusgvalb.z φZB
frlmplusgvalb.r φRRing
frlmvscavalb.k K=BaseR
frlmvscavalb.a φAK
frlmvscavalb.v ˙=F
frlmvscavalb.t ·˙=R
Assertion frlmvscavalb φZ=A˙XiIZi=A·˙Xi

Proof

Step Hyp Ref Expression
1 frlmplusgvalb.f F=RfreeLModI
2 frlmplusgvalb.b B=BaseF
3 frlmplusgvalb.i φIW
4 frlmplusgvalb.x φXB
5 frlmplusgvalb.z φZB
6 frlmplusgvalb.r φRRing
7 frlmvscavalb.k K=BaseR
8 frlmvscavalb.a φAK
9 frlmvscavalb.v ˙=F
10 frlmvscavalb.t ·˙=R
11 1 7 2 frlmbasmap IWZBZKI
12 3 5 11 syl2anc φZKI
13 7 fvexi KV
14 13 a1i φKV
15 14 3 elmapd φZKIZ:IK
16 12 15 mpbid φZ:IK
17 16 ffnd φZFnI
18 1 frlmlmod RRingIWFLMod
19 6 3 18 syl2anc φFLMod
20 8 7 eleqtrdi φABaseR
21 1 frlmsca RRingIWR=ScalarF
22 6 3 21 syl2anc φR=ScalarF
23 22 fveq2d φBaseR=BaseScalarF
24 20 23 eleqtrd φABaseScalarF
25 eqid ScalarF=ScalarF
26 eqid BaseScalarF=BaseScalarF
27 2 25 9 26 lmodvscl FLModABaseScalarFXBA˙XB
28 19 24 4 27 syl3anc φA˙XB
29 1 7 2 frlmbasmap IWA˙XBA˙XKI
30 3 28 29 syl2anc φA˙XKI
31 14 3 elmapd φA˙XKIA˙X:IK
32 30 31 mpbid φA˙X:IK
33 32 ffnd φA˙XFnI
34 eqfnfv ZFnIA˙XFnIZ=A˙XiIZi=A˙Xi
35 17 33 34 syl2anc φZ=A˙XiIZi=A˙Xi
36 3 adantr φiIIW
37 8 adantr φiIAK
38 4 adantr φiIXB
39 simpr φiIiI
40 1 2 7 36 37 38 39 9 10 frlmvscaval φiIA˙Xi=A·˙Xi
41 40 eqeq2d φiIZi=A˙XiZi=A·˙Xi
42 41 ralbidva φiIZi=A˙XiiIZi=A·˙Xi
43 35 42 bitrd φZ=A˙XiIZi=A·˙Xi