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 ( 𝜑 → ( 𝑍 = ( ( 𝐴 𝑋 ) ( 𝐶 𝑌 ) ) ↔ ∀ 𝑖𝐼 ( 𝑍𝑖 ) = ( ( 𝐴 · ( 𝑋𝑖 ) ) + ( 𝐶 · ( 𝑌𝑖 ) ) ) ) )