Theorem frlm0vald

Description: All coordinates of the zero vector are zero. (Contributed by SN, 14-Aug-2024)

	Ref	Expression
Hypotheses	frlm0vald.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
	frlm0vald.0	⊢ 0 = ( 0g ‘ 𝑅 )
	frlm0vald.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	frlm0vald.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	frlm0vald.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
Assertion	frlm0vald	⊢ ( 𝜑 → ( ( 0g ‘ 𝐹 ) ‘ 𝐽 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		frlm0vald.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		frlm0vald.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		frlm0vald.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		frlm0vald.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		frlm0vald.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐼 )
6	1 2	frlm0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( 𝐼 × { 0 } ) = ( 0g ‘ 𝐹 ) )
7	3 4 6	syl2anc	⊢ ( 𝜑 → ( 𝐼 × { 0 } ) = ( 0g ‘ 𝐹 ) )
8	7	fveq1d	⊢ ( 𝜑 → ( ( 𝐼 × { 0 } ) ‘ 𝐽 ) = ( ( 0g ‘ 𝐹 ) ‘ 𝐽 ) )
9	2	fvexi	⊢ 0 ∈ V
10	9	fvconst2	⊢ ( 𝐽 ∈ 𝐼 → ( ( 𝐼 × { 0 } ) ‘ 𝐽 ) = 0 )
11	5 10	syl	⊢ ( 𝜑 → ( ( 𝐼 × { 0 } ) ‘ 𝐽 ) = 0 )
12	8 11	eqtr3d	⊢ ( 𝜑 → ( ( 0g ‘ 𝐹 ) ‘ 𝐽 ) = 0 )