Metamath Proof Explorer

Theorem frlmvplusgscavalb

Description: Addition combined with 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 ‘ 𝑅 )
frlmvplusgscavalb.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
frlmvplusgscavalb.a ⊢ + = ( +g ‘ 𝑅 )
frlmvplusgscavalb.p ⊢ ✚ = ( +g ‘ 𝐹 )
frlmvplusgscavalb.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion frlmvplusgscavalb ( 𝜑 → ( 𝑍 = ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )

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 frlmvplusgscavalb.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12 frlmvplusgscavalb.a ⊢ + = ( +g ‘ 𝑅 )
13 frlmvplusgscavalb.p ⊢ ✚ = ( +g ‘ 𝐹 )
14 frlmvplusgscavalb.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
15 1 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ LMod )
16 6 3 15 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ LMod )
17 8 7 eleqtrdi ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝑅 ) )
18 1 frlmsca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
19 6 3 18 syl2anc ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )
20 19 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
21 17 20 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
22 eqid ⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
23 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
24 2 22 9 23 lmodvscl ⊢ ( ( 𝐹 ∈ LMod ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ∙ 𝑋 ) ∈ 𝐵 )
25 16 21 4 24 syl3anc ⊢ ( 𝜑 → ( 𝐴 ∙ 𝑋 ) ∈ 𝐵 )
26 14 7 eleqtrdi ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝑅 ) )
27 26 20 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
28 2 22 9 23 lmodvscl ⊢ ( ( 𝐹 ∈ LMod ∧ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐶 ∙ 𝑌 ) ∈ 𝐵 )
29 16 27 11 28 syl3anc ⊢ ( 𝜑 → ( 𝐶 ∙ 𝑌 ) ∈ 𝐵 )
30 1 2 3 25 5 6 29 12 13 frlmplusgvalb ⊢ ( 𝜑 → ( 𝑍 = ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) + ( ( 𝐶 ∙ 𝑌 ) ‘ 𝑖 ) ) ) )
31 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
32 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐴 ∈ 𝐾 )
33 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑋 ∈ 𝐵 )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
35 1 2 7 31 32 33 34 9 10 frlmvscaval ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) = ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) )
36 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐶 ∈ 𝐾 )
37 11 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝑌 ∈ 𝐵 )
38 1 2 7 31 36 37 34 9 10 frlmvscaval ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝐶 ∙ 𝑌 ) ‘ 𝑖 ) = ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) )
39 35 38 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) + ( ( 𝐶 ∙ 𝑌 ) ‘ 𝑖 ) ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) )
40 39 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑍 ‘ 𝑖 ) = ( ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) + ( ( 𝐶 ∙ 𝑌 ) ‘ 𝑖 ) ) ↔ ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )
41 40 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( ( 𝐴 ∙ 𝑋 ) ‘ 𝑖 ) + ( ( 𝐶 ∙ 𝑌 ) ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )
42 30 41 bitrd ⊢ ( 𝜑 → ( 𝑍 = ( ( 𝐴 ∙ 𝑋 ) ✚ ( 𝐶 ∙ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑍 ‘ 𝑖 ) = ( ( 𝐴 · ( 𝑋 ‘ 𝑖 ) ) + ( 𝐶 · ( 𝑌 ‘ 𝑖 ) ) ) ) )