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 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmplusgvalb.b 𝐵 = ( Base ‘ 𝐹 )
frlmplusgvalb.i ( 𝜑𝐼𝑊 )
frlmplusgvalb.x ( 𝜑𝑋𝐵 )
frlmplusgvalb.z ( 𝜑𝑍𝐵 )
frlmplusgvalb.r ( 𝜑𝑅 ∈ Ring )
frlmvscavalb.k 𝐾 = ( Base ‘ 𝑅 )
frlmvscavalb.a ( 𝜑𝐴𝐾 )
frlmvscavalb.v = ( ·𝑠𝐹 )
frlmvscavalb.t · = ( .r𝑅 )
Assertion frlmvscavalb ( 𝜑 → ( 𝑍 = ( 𝐴 𝑋 ) ↔ ∀ 𝑖𝐼 ( 𝑍𝑖 ) = ( 𝐴 · ( 𝑋𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 frlmplusgvalb.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmplusgvalb.b 𝐵 = ( Base ‘ 𝐹 )
3 frlmplusgvalb.i ( 𝜑𝐼𝑊 )
4 frlmplusgvalb.x ( 𝜑𝑋𝐵 )
5 frlmplusgvalb.z ( 𝜑𝑍𝐵 )
6 frlmplusgvalb.r ( 𝜑𝑅 ∈ Ring )
7 frlmvscavalb.k 𝐾 = ( Base ‘ 𝑅 )
8 frlmvscavalb.a ( 𝜑𝐴𝐾 )
9 frlmvscavalb.v = ( ·𝑠𝐹 )
10 frlmvscavalb.t · = ( .r𝑅 )
11 1 7 2 frlmbasmap ( ( 𝐼𝑊𝑍𝐵 ) → 𝑍 ∈ ( 𝐾m 𝐼 ) )
12 3 5 11 syl2anc ( 𝜑𝑍 ∈ ( 𝐾m 𝐼 ) )
13 7 fvexi 𝐾 ∈ V
14 13 a1i ( 𝜑𝐾 ∈ V )
15 14 3 elmapd ( 𝜑 → ( 𝑍 ∈ ( 𝐾m 𝐼 ) ↔ 𝑍 : 𝐼𝐾 ) )
16 12 15 mpbid ( 𝜑𝑍 : 𝐼𝐾 )
17 16 ffnd ( 𝜑𝑍 Fn 𝐼 )
18 1 frlmlmod ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐹 ∈ LMod )
19 6 3 18 syl2anc ( 𝜑𝐹 ∈ LMod )
20 8 7 eleqtrdi ( 𝜑𝐴 ∈ ( Base ‘ 𝑅 ) )
21 1 frlmsca ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
22 6 3 21 syl2anc ( 𝜑𝑅 = ( Scalar ‘ 𝐹 ) )
23 22 fveq2d ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
24 20 23 eleqtrd ( 𝜑𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
25 eqid ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
26 eqid ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
27 2 25 9 26 lmodvscl ( ( 𝐹 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑋𝐵 ) → ( 𝐴 𝑋 ) ∈ 𝐵 )
28 19 24 4 27 syl3anc ( 𝜑 → ( 𝐴 𝑋 ) ∈ 𝐵 )
29 1 7 2 frlmbasmap ( ( 𝐼𝑊 ∧ ( 𝐴 𝑋 ) ∈ 𝐵 ) → ( 𝐴 𝑋 ) ∈ ( 𝐾m 𝐼 ) )
30 3 28 29 syl2anc ( 𝜑 → ( 𝐴 𝑋 ) ∈ ( 𝐾m 𝐼 ) )
31 14 3 elmapd ( 𝜑 → ( ( 𝐴 𝑋 ) ∈ ( 𝐾m 𝐼 ) ↔ ( 𝐴 𝑋 ) : 𝐼𝐾 ) )
32 30 31 mpbid ( 𝜑 → ( 𝐴 𝑋 ) : 𝐼𝐾 )
33 32 ffnd ( 𝜑 → ( 𝐴 𝑋 ) Fn 𝐼 )
34 eqfnfv ( ( 𝑍 Fn 𝐼 ∧ ( 𝐴 𝑋 ) Fn 𝐼 ) → ( 𝑍 = ( 𝐴 𝑋 ) ↔ ∀ 𝑖𝐼 ( 𝑍𝑖 ) = ( ( 𝐴 𝑋 ) ‘ 𝑖 ) ) )
35 17 33 34 syl2anc ( 𝜑 → ( 𝑍 = ( 𝐴 𝑋 ) ↔ ∀ 𝑖𝐼 ( 𝑍𝑖 ) = ( ( 𝐴 𝑋 ) ‘ 𝑖 ) ) )
36 3 adantr ( ( 𝜑𝑖𝐼 ) → 𝐼𝑊 )
37 8 adantr ( ( 𝜑𝑖𝐼 ) → 𝐴𝐾 )
38 4 adantr ( ( 𝜑𝑖𝐼 ) → 𝑋𝐵 )
39 simpr ( ( 𝜑𝑖𝐼 ) → 𝑖𝐼 )
40 1 2 7 36 37 38 39 9 10 frlmvscaval ( ( 𝜑𝑖𝐼 ) → ( ( 𝐴 𝑋 ) ‘ 𝑖 ) = ( 𝐴 · ( 𝑋𝑖 ) ) )
41 40 eqeq2d ( ( 𝜑𝑖𝐼 ) → ( ( 𝑍𝑖 ) = ( ( 𝐴 𝑋 ) ‘ 𝑖 ) ↔ ( 𝑍𝑖 ) = ( 𝐴 · ( 𝑋𝑖 ) ) ) )
42 41 ralbidva ( 𝜑 → ( ∀ 𝑖𝐼 ( 𝑍𝑖 ) = ( ( 𝐴 𝑋 ) ‘ 𝑖 ) ↔ ∀ 𝑖𝐼 ( 𝑍𝑖 ) = ( 𝐴 · ( 𝑋𝑖 ) ) ) )
43 35 42 bitrd ( 𝜑 → ( 𝑍 = ( 𝐴 𝑋 ) ↔ ∀ 𝑖𝐼 ( 𝑍𝑖 ) = ( 𝐴 · ( 𝑋𝑖 ) ) ) )