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 = ( R freeLMod I )
frlmplusgvalb.b
|- B = ( Base ` F )
frlmplusgvalb.i
|- ( ph -> I e. W )
frlmplusgvalb.x
|- ( ph -> X e. B )
frlmplusgvalb.z
|- ( ph -> Z e. B )
frlmplusgvalb.r
|- ( ph -> R e. Ring )
frlmvscavalb.k
|- K = ( Base ` R )
frlmvscavalb.a
|- ( ph -> A e. K )
frlmvscavalb.v
|- .xb = ( .s ` F )
frlmvscavalb.t
|- .x. = ( .r ` R )
Assertion frlmvscavalb
|- ( ph -> ( Z = ( A .xb X ) <-> A. i e. I ( Z ` i ) = ( A .x. ( X ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 frlmplusgvalb.f
 |-  F = ( R freeLMod I )
2 frlmplusgvalb.b
 |-  B = ( Base ` F )
3 frlmplusgvalb.i
 |-  ( ph -> I e. W )
4 frlmplusgvalb.x
 |-  ( ph -> X e. B )
5 frlmplusgvalb.z
 |-  ( ph -> Z e. B )
6 frlmplusgvalb.r
 |-  ( ph -> R e. Ring )
7 frlmvscavalb.k
 |-  K = ( Base ` R )
8 frlmvscavalb.a
 |-  ( ph -> A e. K )
9 frlmvscavalb.v
 |-  .xb = ( .s ` F )
10 frlmvscavalb.t
 |-  .x. = ( .r ` R )
11 1 7 2 frlmbasmap
 |-  ( ( I e. W /\ Z e. B ) -> Z e. ( K ^m I ) )
12 3 5 11 syl2anc
 |-  ( ph -> Z e. ( K ^m I ) )
13 7 fvexi
 |-  K e. _V
14 13 a1i
 |-  ( ph -> K e. _V )
15 14 3 elmapd
 |-  ( ph -> ( Z e. ( K ^m I ) <-> Z : I --> K ) )
16 12 15 mpbid
 |-  ( ph -> Z : I --> K )
17 16 ffnd
 |-  ( ph -> Z Fn I )
18 1 frlmlmod
 |-  ( ( R e. Ring /\ I e. W ) -> F e. LMod )
19 6 3 18 syl2anc
 |-  ( ph -> F e. LMod )
20 8 7 eleqtrdi
 |-  ( ph -> A e. ( Base ` R ) )
21 1 frlmsca
 |-  ( ( R e. Ring /\ I e. W ) -> R = ( Scalar ` F ) )
22 6 3 21 syl2anc
 |-  ( ph -> R = ( Scalar ` F ) )
23 22 fveq2d
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )
24 20 23 eleqtrd
 |-  ( ph -> A e. ( Base ` ( Scalar ` F ) ) )
25 eqid
 |-  ( Scalar ` F ) = ( Scalar ` F )
26 eqid
 |-  ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )
27 2 25 9 26 lmodvscl
 |-  ( ( F e. LMod /\ A e. ( Base ` ( Scalar ` F ) ) /\ X e. B ) -> ( A .xb X ) e. B )
28 19 24 4 27 syl3anc
 |-  ( ph -> ( A .xb X ) e. B )
29 1 7 2 frlmbasmap
 |-  ( ( I e. W /\ ( A .xb X ) e. B ) -> ( A .xb X ) e. ( K ^m I ) )
30 3 28 29 syl2anc
 |-  ( ph -> ( A .xb X ) e. ( K ^m I ) )
31 14 3 elmapd
 |-  ( ph -> ( ( A .xb X ) e. ( K ^m I ) <-> ( A .xb X ) : I --> K ) )
32 30 31 mpbid
 |-  ( ph -> ( A .xb X ) : I --> K )
33 32 ffnd
 |-  ( ph -> ( A .xb X ) Fn I )
34 eqfnfv
 |-  ( ( Z Fn I /\ ( A .xb X ) Fn I ) -> ( Z = ( A .xb X ) <-> A. i e. I ( Z ` i ) = ( ( A .xb X ) ` i ) ) )
35 17 33 34 syl2anc
 |-  ( ph -> ( Z = ( A .xb X ) <-> A. i e. I ( Z ` i ) = ( ( A .xb X ) ` i ) ) )
36 3 adantr
 |-  ( ( ph /\ i e. I ) -> I e. W )
37 8 adantr
 |-  ( ( ph /\ i e. I ) -> A e. K )
38 4 adantr
 |-  ( ( ph /\ i e. I ) -> X e. B )
39 simpr
 |-  ( ( ph /\ i e. I ) -> i e. I )
40 1 2 7 36 37 38 39 9 10 frlmvscaval
 |-  ( ( ph /\ i e. I ) -> ( ( A .xb X ) ` i ) = ( A .x. ( X ` i ) ) )
41 40 eqeq2d
 |-  ( ( ph /\ i e. I ) -> ( ( Z ` i ) = ( ( A .xb X ) ` i ) <-> ( Z ` i ) = ( A .x. ( X ` i ) ) ) )
42 41 ralbidva
 |-  ( ph -> ( A. i e. I ( Z ` i ) = ( ( A .xb X ) ` i ) <-> A. i e. I ( Z ` i ) = ( A .x. ( X ` i ) ) ) )
43 35 42 bitrd
 |-  ( ph -> ( Z = ( A .xb X ) <-> A. i e. I ( Z ` i ) = ( A .x. ( X ` i ) ) ) )