Theorem frlm0vald

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

	Ref	Expression
Hypotheses	frlm0vald.f	|- F = ( R freeLMod I )
	frlm0vald.0	|- .0. = ( 0g ` R )
	frlm0vald.r	|- ( ph -> R e. Ring )
	frlm0vald.i	|- ( ph -> I e. W )
	frlm0vald.j	|- ( ph -> J e. I )
Assertion	frlm0vald	|- ( ph -> ( ( 0g ` F ) ` J ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		frlm0vald.f	|- F = ( R freeLMod I )
2		frlm0vald.0	|- .0. = ( 0g ` R )
3		frlm0vald.r	|- ( ph -> R e. Ring )
4		frlm0vald.i	|- ( ph -> I e. W )
5		frlm0vald.j	|- ( ph -> J e. I )
6	1 2	frlm0	|- ( ( R e. Ring /\ I e. W ) -> ( I X. { .0. } ) = ( 0g ` F ) )
7	3 4 6	syl2anc	|- ( ph -> ( I X. { .0. } ) = ( 0g ` F ) )
8	7	fveq1d	|- ( ph -> ( ( I X. { .0. } ) ` J ) = ( ( 0g ` F ) ` J ) )
9	2	fvexi	|- .0. e. _V
10	9	fvconst2	|- ( J e. I -> ( ( I X. { .0. } ) ` J ) = .0. )
11	5 10	syl	|- ( ph -> ( ( I X. { .0. } ) ` J ) = .0. )
12	8 11	eqtr3d	|- ( ph -> ( ( 0g ` F ) ` J ) = .0. )