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	⊢ ( 𝜑 → ( ( 𝑋 ✚ 𝑌 ) ‘ 𝐽 ) = ( ( 𝑋 ‘ 𝐽 ) + ( 𝑌 ‘ 𝐽 ) ) )

Metamath Proof Explorer

Theorem frlmvplusgvalc

Proof