Step |
Hyp |
Ref |
Expression |
1 |
|
scmsuppfi.s |
⊢ 𝑆 = ( Scalar ‘ 𝑀 ) |
2 |
|
scmsuppfi.r |
⊢ 𝑅 = ( Base ‘ 𝑆 ) |
3 |
|
simp3 |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ∈ Fin ) → ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ∈ Fin ) |
4 |
|
simpll |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑀 ∈ LMod ) |
5 |
|
simplr |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) |
6 |
|
simpr |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) |
7 |
4 5 6
|
3jca |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ) |
8 |
7
|
3adant3 |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ∈ Fin ) → ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ) |
9 |
1 2
|
scmsuppss |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ) |
10 |
8 9
|
syl |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ∈ Fin ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ) |
11 |
|
ssfi |
⊢ ( ( ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ∈ Fin ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) |
12 |
3 10 11
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) ∈ Fin ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) |