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 ) |