Metamath Proof Explorer


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 )