Metamath Proof Explorer

Theorem lmodslmd

Description: Left semimodules generalize the notion of left modules. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion lmodslmd ( 𝑊 ∈ LMod → 𝑊 ∈ SLMod )

Proof

Step Hyp Ref Expression
1 lmodcmn ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ CMnd )
2 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
3 2 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
4 ringsrg ⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( Scalar ‘ 𝑊 ) ∈ SRing )
5 3 4 syl ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ SRing )
6 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
8 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
9 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
10 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
11 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
12 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
13 6 7 8 2 9 10 11 12 islmod ⊢ ( 𝑊 ∈ LMod ↔ ( 𝑊 ∈ Grp ∧ ( Scalar ‘ 𝑊 ) ∈ Ring ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ) ) ) )
14 13 simp3bi ⊢ ( 𝑊 ∈ LMod → ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ) ) )
15 14 r19.21bi ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ) ) )
16 15 r19.21bi ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ) ) )
17 16 r19.21bi ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ) ) )
18 17 r19.21bi ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ) ) )
19 18 simpld ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) )
20 18 simprd ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ) )
21 20 simpld ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) )
22 20 simprd ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 )
23 simp-4l ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ LMod )
24 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
25 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
26 6 2 8 24 25 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) )
27 23 26 sylancom ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) )
28 21 22 27 3jca ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) ) )
29 19 28 jca ⊢ ( ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) ) ) )
30 29 ralrimiva ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) ) ) )
31 30 ralrimiva ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) ) ) )
32 31 ralrimiva ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) ) ) )
33 32 ralrimiva ⊢ ( 𝑊 ∈ LMod → ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) ) ) )
34 6 7 8 25 2 9 10 11 12 24 isslmd ⊢ ( 𝑊 ∈ SLMod ↔ ( 𝑊 ∈ CMnd ∧ ( Scalar ‘ 𝑊 ) ∈ SRing ∧ ∀ 𝑞 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) ( 𝑤 ( +g ‘ 𝑊 ) 𝑥 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∧ ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ) ∧ ( ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 𝑞 ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑤 ) ) ∧ ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = 𝑤 ∧ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑤 ) = ( 0g ‘ 𝑊 ) ) ) ) )
35 1 5 33 34 syl3anbrc ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ SLMod )