Step |
Hyp |
Ref |
Expression |
1 |
|
eqidd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) ) |
2 |
|
eqidd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) |
3 |
|
eqidd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) ) |
4 |
|
eqidd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) ) |
5 |
|
eqidd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 ) ) |
6 |
|
eqidd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 ) ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
8 |
|
eqid |
⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) |
9 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) |
10 |
7 8 9
|
lcoval |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) ) |
11 |
|
simpl |
⊢ ( ( 𝑣 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑣 ∈ ( Base ‘ 𝑀 ) ) |
12 |
10 11
|
syl6bi |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) → 𝑣 ∈ ( Base ‘ 𝑀 ) ) ) |
13 |
12
|
ssrdv |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ⊆ ( Base ‘ 𝑀 ) ) |
14 |
|
lcoel0 |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) ) |
15 |
14
|
ne0d |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ≠ ∅ ) |
16 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 ) |
17 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
18 |
16 9 17
|
lincsumscmcl |
⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝑏 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑎 ) ( +g ‘ 𝑀 ) 𝑏 ) ∈ ( 𝑀 LinCo 𝑉 ) ) |
19 |
1 2 3 4 5 6 13 15 18
|
islssd |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ∈ ( LSubSp ‘ 𝑀 ) ) |