Step | Hyp | Ref
| Expression |
1 | | lmodcmn 20171 |
. 2
⊢ (𝑊 ∈ LMod → 𝑊 ∈ CMnd) |
2 | | eqid 2738 |
. . . 4
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
3 | 2 | lmodring 20131 |
. . 3
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
4 | | ringsrg 19828 |
. . 3
⊢
((Scalar‘𝑊)
∈ Ring → (Scalar‘𝑊) ∈ SRing) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
SRing) |
6 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑊) =
(Base‘𝑊) |
7 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑊) = (+g‘𝑊) |
8 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
9 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
10 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
11 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
12 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
13 | 6, 7, 8, 2, 9, 10,
11, 12 | islmod 20127 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧
(Scalar‘𝑊) ∈
Ring ∧ ∀𝑞 ∈
(Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤)))) |
14 | 13 | simp3bi 1146 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ LMod →
∀𝑞 ∈
(Base‘(Scalar‘𝑊))∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤))) |
15 | 14 | r19.21bi 3134 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤))) |
16 | 15 | r19.21bi 3134 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ LMod ∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → ∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤))) |
17 | 16 | r19.21bi 3134 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤))) |
18 | 17 | r19.21bi 3134 |
. . . . . . . 8
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) → (((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤))) |
19 | 18 | simpld 495 |
. . . . . . 7
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) → ((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤)))) |
20 | 18 | simprd 496 |
. . . . . . . . 9
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) → (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤)) |
21 | 20 | simpld 495 |
. . . . . . . 8
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) → ((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤))) |
22 | 20 | simprd 496 |
. . . . . . . 8
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤) |
23 | | simp-4l 780 |
. . . . . . . . 9
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod) |
24 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
25 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘𝑊) = (0g‘𝑊) |
26 | 6, 2, 8, 24, 25 | lmod0vs 20156 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑤 ∈ (Base‘𝑊)) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = (0g‘𝑊)) |
27 | 23, 26 | sylancom 588 |
. . . . . . . 8
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = (0g‘𝑊)) |
28 | 21, 22, 27 | 3jca 1127 |
. . . . . . 7
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) → (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤 ∧
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = (0g‘𝑊))) |
29 | 19, 28 | jca 512 |
. . . . . 6
⊢
(((((𝑊 ∈ LMod
∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) ∧ 𝑤 ∈ (Base‘𝑊)) → (((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤 ∧
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = (0g‘𝑊)))) |
30 | 29 | ralrimiva 3103 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤 ∧
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = (0g‘𝑊)))) |
31 | 30 | ralrimiva 3103 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) ∧ 𝑟 ∈ (Base‘(Scalar‘𝑊))) → ∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤 ∧
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = (0g‘𝑊)))) |
32 | 31 | ralrimiva 3103 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑞 ∈
(Base‘(Scalar‘𝑊))) → ∀𝑟 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠
‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠
‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑥)) ∧ ((𝑞(+g‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = ((𝑞( ·𝑠
‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠
‘𝑊)𝑤))) ∧ (((𝑞(.r‘(Scalar‘𝑊))𝑟)( ·𝑠
‘𝑊)𝑤) = (𝑞( ·𝑠
‘𝑊)(𝑟(
·𝑠 ‘𝑊)𝑤)) ∧
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = 𝑤 ∧
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑤) = (0g‘𝑊)))) |
33 | 32 | ralrimiva 3103 |
. 2
⊢ (𝑊 ∈ 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 31455 |
. 2
⊢ (𝑊 ∈ 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 1342 |
1
⊢ (𝑊 ∈ LMod → 𝑊 ∈ SLMod) |