| Step | Hyp | Ref
| Expression |
| 1 | | islss3.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
| 2 | | islss3.s |
. . . . 5
⊢ 𝑆 = (LSubSp‘𝑊) |
| 3 | 1, 2 | lssss 20934 |
. . . 4
⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) |
| 4 | 3 | adantl 481 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ⊆ 𝑉) |
| 5 | | islss3.x |
. . . . . . 7
⊢ 𝑋 = (𝑊 ↾s 𝑈) |
| 6 | 5, 1 | ressbas2 17283 |
. . . . . 6
⊢ (𝑈 ⊆ 𝑉 → 𝑈 = (Base‘𝑋)) |
| 7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉) → 𝑈 = (Base‘𝑋)) |
| 8 | 3, 7 | sylan2 593 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = (Base‘𝑋)) |
| 9 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 10 | 5, 9 | ressplusg 17334 |
. . . . 5
⊢ (𝑈 ∈ 𝑆 → (+g‘𝑊) = (+g‘𝑋)) |
| 11 | 10 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (+g‘𝑊) = (+g‘𝑋)) |
| 12 | | eqid 2737 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 13 | 5, 12 | resssca 17387 |
. . . . 5
⊢ (𝑈 ∈ 𝑆 → (Scalar‘𝑊) = (Scalar‘𝑋)) |
| 14 | 13 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑊) = (Scalar‘𝑋)) |
| 15 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 16 | 5, 15 | ressvsca 17388 |
. . . . 5
⊢ (𝑈 ∈ 𝑆 → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
| 17 | 16 | adantl 481 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
| 18 | | eqidd 2738 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (Base‘(Scalar‘𝑊)) =
(Base‘(Scalar‘𝑊))) |
| 19 | | eqidd 2738 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) →
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊))) |
| 20 | | eqidd 2738 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) →
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊))) |
| 21 | | eqidd 2738 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) →
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊))) |
| 22 | 12 | lmodring 20866 |
. . . . 5
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
| 23 | 22 | adantr 480 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (Scalar‘𝑊) ∈ Ring) |
| 24 | 2 | lsssubg 20955 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ∈ (SubGrp‘𝑊)) |
| 25 | 5 | subggrp 19147 |
. . . . 5
⊢ (𝑈 ∈ (SubGrp‘𝑊) → 𝑋 ∈ Grp) |
| 26 | 24, 25 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ Grp) |
| 27 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 28 | 12, 15, 27, 2 | lssvscl 20953 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝑊)𝑎) ∈ 𝑈) |
| 29 | 28 | 3impb 1115 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈) → (𝑥( ·𝑠
‘𝑊)𝑎) ∈ 𝑈) |
| 30 | | simpll 767 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑊 ∈ LMod) |
| 31 | | simpr1 1195 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
| 32 | 3 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑈 ⊆ 𝑉) |
| 33 | | simpr2 1196 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑎 ∈ 𝑈) |
| 34 | 32, 33 | sseldd 3984 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑎 ∈ 𝑉) |
| 35 | | simpr3 1197 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑏 ∈ 𝑈) |
| 36 | 32, 35 | sseldd 3984 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → 𝑏 ∈ 𝑉) |
| 37 | 1, 9, 12, 15, 27 | lmodvsdi 20883 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑥( ·𝑠
‘𝑊)(𝑎(+g‘𝑊)𝑏)) = ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑏))) |
| 38 | 30, 31, 34, 36, 37 | syl13anc 1374 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑥( ·𝑠
‘𝑊)(𝑎(+g‘𝑊)𝑏)) = ((𝑥( ·𝑠
‘𝑊)𝑎)(+g‘𝑊)(𝑥( ·𝑠
‘𝑊)𝑏))) |
| 39 | | simpll 767 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → 𝑊 ∈ LMod) |
| 40 | | simpr1 1195 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → 𝑥 ∈ (Base‘(Scalar‘𝑊))) |
| 41 | | simpr2 1196 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → 𝑎 ∈ (Base‘(Scalar‘𝑊))) |
| 42 | 3 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → 𝑈 ⊆ 𝑉) |
| 43 | | simpr3 1197 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → 𝑏 ∈ 𝑈) |
| 44 | 42, 43 | sseldd 3984 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → 𝑏 ∈ 𝑉) |
| 45 | | eqid 2737 |
. . . . . 6
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
| 46 | 1, 9, 12, 15, 27, 45 | lmodvsdir 20884 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑉)) → ((𝑥(+g‘(Scalar‘𝑊))𝑎)( ·𝑠
‘𝑊)𝑏) = ((𝑥( ·𝑠
‘𝑊)𝑏)(+g‘𝑊)(𝑎( ·𝑠
‘𝑊)𝑏))) |
| 47 | 39, 40, 41, 44, 46 | syl13anc 1374 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → ((𝑥(+g‘(Scalar‘𝑊))𝑎)( ·𝑠
‘𝑊)𝑏) = ((𝑥( ·𝑠
‘𝑊)𝑏)(+g‘𝑊)(𝑎( ·𝑠
‘𝑊)𝑏))) |
| 48 | | eqid 2737 |
. . . . . 6
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
| 49 | 1, 12, 15, 27, 48 | lmodvsass 20885 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑥 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑉)) → ((𝑥(.r‘(Scalar‘𝑊))𝑎)( ·𝑠
‘𝑊)𝑏) = (𝑥( ·𝑠
‘𝑊)(𝑎(
·𝑠 ‘𝑊)𝑏))) |
| 50 | 39, 40, 41, 44, 49 | syl13anc 1374 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑏 ∈ 𝑈)) → ((𝑥(.r‘(Scalar‘𝑊))𝑎)( ·𝑠
‘𝑊)𝑏) = (𝑥( ·𝑠
‘𝑊)(𝑎(
·𝑠 ‘𝑊)𝑏))) |
| 51 | 4 | sselda 3983 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑉) |
| 52 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
| 53 | 1, 12, 15, 52 | lmodvs1 20888 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑉) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑥) = 𝑥) |
| 54 | 53 | adantlr 715 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑥 ∈ 𝑉) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑥) = 𝑥) |
| 55 | 51, 54 | syldan 591 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑥 ∈ 𝑈) →
((1r‘(Scalar‘𝑊))( ·𝑠
‘𝑊)𝑥) = 𝑥) |
| 56 | 8, 11, 14, 17, 18, 19, 20, 21, 23, 26, 29, 38, 47, 50, 55 | islmodd 20864 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ LMod) |
| 57 | 4, 56 | jca 511 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) |
| 58 | | simprl 771 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → 𝑈 ⊆ 𝑉) |
| 59 | 58, 6 | syl 17 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → 𝑈 = (Base‘𝑋)) |
| 60 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝑋)
∈ V |
| 61 | 59, 60 | eqeltrdi 2849 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → 𝑈 ∈ V) |
| 62 | 5, 12 | resssca 17387 |
. . . . . 6
⊢ (𝑈 ∈ V →
(Scalar‘𝑊) =
(Scalar‘𝑋)) |
| 63 | 61, 62 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (Scalar‘𝑊) = (Scalar‘𝑋)) |
| 64 | 63 | eqcomd 2743 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (Scalar‘𝑋) = (Scalar‘𝑊)) |
| 65 | | eqidd 2738 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) →
(Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑋))) |
| 66 | 1 | a1i 11 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → 𝑉 = (Base‘𝑊)) |
| 67 | 5, 9 | ressplusg 17334 |
. . . . . 6
⊢ (𝑈 ∈ V →
(+g‘𝑊) =
(+g‘𝑋)) |
| 68 | 61, 67 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) →
(+g‘𝑊) =
(+g‘𝑋)) |
| 69 | 68 | eqcomd 2743 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) →
(+g‘𝑋) =
(+g‘𝑊)) |
| 70 | 5, 15 | ressvsca 17388 |
. . . . . 6
⊢ (𝑈 ∈ V → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
| 71 | 61, 70 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑋)) |
| 72 | 71 | eqcomd 2743 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (
·𝑠 ‘𝑋) = ( ·𝑠
‘𝑊)) |
| 73 | 2 | a1i 11 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → 𝑆 = (LSubSp‘𝑊)) |
| 74 | 59, 58 | eqsstrrd 4019 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (Base‘𝑋) ⊆ 𝑉) |
| 75 | | lmodgrp 20865 |
. . . . . 6
⊢ (𝑋 ∈ LMod → 𝑋 ∈ Grp) |
| 76 | 75 | ad2antll 729 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → 𝑋 ∈ Grp) |
| 77 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑋) =
(Base‘𝑋) |
| 78 | 77 | grpbn0 18984 |
. . . . 5
⊢ (𝑋 ∈ Grp →
(Base‘𝑋) ≠
∅) |
| 79 | 76, 78 | syl 17 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (Base‘𝑋) ≠ ∅) |
| 80 | | eqid 2737 |
. . . . . . 7
⊢
(LSubSp‘𝑋) =
(LSubSp‘𝑋) |
| 81 | 77, 80 | lss1 20936 |
. . . . . 6
⊢ (𝑋 ∈ LMod →
(Base‘𝑋) ∈
(LSubSp‘𝑋)) |
| 82 | 81 | ad2antll 729 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (Base‘𝑋) ∈ (LSubSp‘𝑋)) |
| 83 | | eqid 2737 |
. . . . . 6
⊢
(Scalar‘𝑋) =
(Scalar‘𝑋) |
| 84 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑋)) = (Base‘(Scalar‘𝑋)) |
| 85 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑋) = (+g‘𝑋) |
| 86 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑋) = ( ·𝑠
‘𝑋) |
| 87 | 83, 84, 85, 86, 80 | lsscl 20940 |
. . . . 5
⊢
(((Base‘𝑋)
∈ (LSubSp‘𝑋)
∧ (𝑥 ∈
(Base‘(Scalar‘𝑋)) ∧ 𝑎 ∈ (Base‘𝑋) ∧ 𝑏 ∈ (Base‘𝑋))) → ((𝑥( ·𝑠
‘𝑋)𝑎)(+g‘𝑋)𝑏) ∈ (Base‘𝑋)) |
| 88 | 82, 87 | sylan 580 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) ∧ (𝑥 ∈ (Base‘(Scalar‘𝑋)) ∧ 𝑎 ∈ (Base‘𝑋) ∧ 𝑏 ∈ (Base‘𝑋))) → ((𝑥( ·𝑠
‘𝑋)𝑎)(+g‘𝑋)𝑏) ∈ (Base‘𝑋)) |
| 89 | 64, 65, 66, 69, 72, 73, 74, 79, 88 | islssd 20933 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → (Base‘𝑋) ∈ 𝑆) |
| 90 | 59, 89 | eqeltrd 2841 |
. 2
⊢ ((𝑊 ∈ LMod ∧ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod)) → 𝑈 ∈ 𝑆) |
| 91 | 57, 90 | impbida 801 |
1
⊢ (𝑊 ∈ LMod → (𝑈 ∈ 𝑆 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod))) |