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 )