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 ) ) ) )