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 ⊢ ( 𝜑 → ( 𝑍 = ( 𝐴 ∙ 𝑋 ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) ) )