This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )