Metamath Proof Explorer

Theorem frlmvplusgvalc

Description: Coordinates of a sum with respect to a basis in a free module. (Contributed by AV, 16-Jan-2023)

Ref Expression
Hypotheses frlmvplusgvalc.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmvplusgvalc.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
frlmvplusgvalc.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
frlmvplusgvalc.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
frlmvplusgvalc.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
frlmvplusgvalc.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
frlmvplusgvalc.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
frlmvplusgvalc.a ⊢ + = ( +g ‘ 𝑅 )
frlmvplusgvalc.p ⊢ ✚ = ( +g ‘ 𝐹 )
Assertion frlmvplusgvalc ( 𝜑 → ( ( 𝑋 ✚ 𝑌 ) ‘ 𝐽 ) = ( ( 𝑋 ‘ 𝐽 ) + ( 𝑌 ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 frlmvplusgvalc.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmvplusgvalc.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 frlmvplusgvalc.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4 frlmvplusgvalc.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5 frlmvplusgvalc.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 frlmvplusgvalc.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 frlmvplusgvalc.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
8 frlmvplusgvalc.a ⊢ + = ( +g ‘ 𝑅 )
9 frlmvplusgvalc.p ⊢ ✚ = ( +g ‘ 𝐹 )
10 1 2 3 4 5 6 8 9 frlmplusgval ⊢ ( 𝜑 → ( 𝑋 ✚ 𝑌 ) = ( 𝑋 ∘f + 𝑌 ) )
11 10 fveq1d ⊢ ( 𝜑 → ( ( 𝑋 ✚ 𝑌 ) ‘ 𝐽 ) = ( ( 𝑋 ∘f + 𝑌 ) ‘ 𝐽 ) )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 1 12 2 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
14 4 5 13 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
15 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
16 15 4 elmapd ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) )
17 14 16 mpbid ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
18 17 ffnd ⊢ ( 𝜑 → 𝑋 Fn 𝐼 )
19 1 12 2 frlmbasmap ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
20 4 6 19 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) )
21 15 4 elmapd ⊢ ( 𝜑 → ( 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐼 ) ↔ 𝑌 : 𝐼 ⟶ ( Base ‘ 𝑅 ) ) )
22 20 21 mpbid ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
23 22 ffnd ⊢ ( 𝜑 → 𝑌 Fn 𝐼 )
24 fnfvof ⊢ ( ( ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) ∧ ( 𝐼 ∈ 𝑊 ∧ 𝐽 ∈ 𝐼 ) ) → ( ( 𝑋 ∘f + 𝑌 ) ‘ 𝐽 ) = ( ( 𝑋 ‘ 𝐽 ) + ( 𝑌 ‘ 𝐽 ) ) )
25 18 23 4 7 24 syl22anc ⊢ ( 𝜑 → ( ( 𝑋 ∘f + 𝑌 ) ‘ 𝐽 ) = ( ( 𝑋 ‘ 𝐽 ) + ( 𝑌 ‘ 𝐽 ) ) )
26 11 25 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ✚ 𝑌 ) ‘ 𝐽 ) = ( ( 𝑋 ‘ 𝐽 ) + ( 𝑌 ‘ 𝐽 ) ) )