Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
2 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
3 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
4 |
|
eqid |
⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) |
5 |
|
eqid |
⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) |
6 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) |
7 |
|
eqid |
⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) ) |
8 |
|
eqid |
⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) |
9 |
|
eqid |
⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) |
10 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) |
11 |
1 2 3 4 5 6 7 8 9 10
|
isslmd |
⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ ( Scalar ‘ 𝑊 ) ∈ SRing ∧ ∀ 𝑤 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑧 ( ·𝑠 ‘ 𝑊 ) ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑤 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( ( 𝑤 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ( +g ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) ) ∧ ( ( ( 𝑤 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑧 ) ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( 𝑤 ( ·𝑠 ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = 𝑦 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ 𝑊 ) ) ) ) ) |
12 |
11
|
simp1bi |
⊢ ( 𝑊 ∈ SLMod → 𝑊 ∈ CMnd ) |