Metamath Proof Explorer

Theorem islss3

Description: A linear subspace of a module is a subset which is a module in its own right. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses islss3.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
islss3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
islss3.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion islss3 ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) )

Proof

Step Hyp Ref Expression
1 islss3.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 islss3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 islss3.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
4 2 3 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
5 4 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ⊆ 𝑉 )
6 1 2 ressbas2 ⊢ ( 𝑈 ⊆ 𝑉 → 𝑈 = ( Base ‘ 𝑋 ) )
7 6 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ⊆ 𝑉 ) → 𝑈 = ( Base ‘ 𝑋 ) )
8 4 7 sylan2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( Base ‘ 𝑋 ) )
9 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
10 1 9 ressplusg ⊢ ( 𝑈 ∈ 𝑆 → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑋 ) )
11 10 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑋 ) )
12 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13 1 12 resssca ⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
14 13 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
15 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
16 1 15 ressvsca ⊢ ( 𝑈 ∈ 𝑆 → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
17 16 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
18 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) ) )
20 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
21 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
22 12 lmodring ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring )
23 22 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ Ring )
24 3 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
25 1 subggrp ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) → 𝑋 ∈ Grp )
26 24 25 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ Grp )
27 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
28 12 15 27 3 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ∈ 𝑈 )
29 28 3impb ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ∈ 𝑈 )
30 simpll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
31 simpr1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32 4 ad2antlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑈 ⊆ 𝑉 )
33 simpr2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ 𝑈 )
34 32 33 sseldd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ 𝑉 )
35 simpr3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑈 )
36 32 35 sseldd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑉 )
37 2 9 12 15 27 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑎 ( +g ‘ 𝑊 ) 𝑏 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ) )
38 30 31 34 36 37 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑎 ( +g ‘ 𝑊 ) 𝑏 ) ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑎 ) ( +g ‘ 𝑊 ) ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ) )
39 simpll ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
40 simpr1 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
41 simpr2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
42 4 ad2antlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → 𝑈 ⊆ 𝑉 )
43 simpr3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑈 )
44 42 43 sseldd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → 𝑏 ∈ 𝑉 )
45 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑊 ) ) = ( +g ‘ ( Scalar ‘ 𝑊 ) )
46 2 9 12 15 27 45 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑥 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑎 ) ( ·𝑠 ‘ 𝑊 ) 𝑏 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ( +g ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ) )
47 39 40 41 44 46 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 ( +g ‘ ( Scalar ‘ 𝑊 ) ) 𝑎 ) ( ·𝑠 ‘ 𝑊 ) 𝑏 ) = ( ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ( +g ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ) )
48 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
49 2 12 15 27 48 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑥 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑎 ) ( ·𝑠 ‘ 𝑊 ) 𝑏 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ) )
50 39 40 41 44 49 syl13anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑏 ∈ 𝑈 ) ) → ( ( 𝑥 ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑎 ) ( ·𝑠 ‘ 𝑊 ) 𝑏 ) = ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 𝑎 ( ·𝑠 ‘ 𝑊 ) 𝑏 ) ) )
51 5 sselda ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑉 )
52 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
53 2 12 15 52 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = 𝑥 )
54 53 adantlr ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = 𝑥 )
55 51 54 syldan ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑥 ∈ 𝑈 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = 𝑥 )
56 8 11 14 17 18 19 20 21 23 26 29 38 47 50 55 islmodd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ LMod )
57 5 56 jca ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) )
58 simprl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → 𝑈 ⊆ 𝑉 )
59 58 6 syl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → 𝑈 = ( Base ‘ 𝑋 ) )
60 fvex ⊢ ( Base ‘ 𝑋 ) ∈ V
61 59 60 eqeltrdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → 𝑈 ∈ V )
62 1 12 resssca ⊢ ( 𝑈 ∈ V → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
63 61 62 syl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
64 63 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑊 ) )
65 eqidd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( Base ‘ ( Scalar ‘ 𝑋 ) ) = ( Base ‘ ( Scalar ‘ 𝑋 ) ) )
66 2 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → 𝑉 = ( Base ‘ 𝑊 ) )
67 1 9 ressplusg ⊢ ( 𝑈 ∈ V → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑋 ) )
68 61 67 syl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑋 ) )
69 68 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( +g ‘ 𝑋 ) = ( +g ‘ 𝑊 ) )
70 1 15 ressvsca ⊢ ( 𝑈 ∈ V → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
71 61 70 syl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑋 ) )
72 71 eqcomd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( ·𝑠 ‘ 𝑋 ) = ( ·𝑠 ‘ 𝑊 ) )
73 3 a1i ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → 𝑆 = ( LSubSp ‘ 𝑊 ) )
74 59 58 eqsstrrd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( Base ‘ 𝑋 ) ⊆ 𝑉 )
75 lmodgrp ⊢ ( 𝑋 ∈ LMod → 𝑋 ∈ Grp )
76 75 ad2antll ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → 𝑋 ∈ Grp )
77 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
78 77 grpbn0 ⊢ ( 𝑋 ∈ Grp → ( Base ‘ 𝑋 ) ≠ ∅ )
79 76 78 syl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( Base ‘ 𝑋 ) ≠ ∅ )
80 eqid ⊢ ( LSubSp ‘ 𝑋 ) = ( LSubSp ‘ 𝑋 )
81 77 80 lss1 ⊢ ( 𝑋 ∈ LMod → ( Base ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑋 ) )
82 81 ad2antll ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( Base ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑋 ) )
83 eqid ⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
84 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑋 ) ) = ( Base ‘ ( Scalar ‘ 𝑋 ) )
85 eqid ⊢ ( +g ‘ 𝑋 ) = ( +g ‘ 𝑋 )
86 eqid ⊢ ( ·𝑠 ‘ 𝑋 ) = ( ·𝑠 ‘ 𝑋 )
87 83 84 85 86 80 lsscl ⊢ ( ( ( Base ‘ 𝑋 ) ∈ ( LSubSp ‘ 𝑋 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑋 ) ∧ 𝑏 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑎 ) ( +g ‘ 𝑋 ) 𝑏 ) ∈ ( Base ‘ 𝑋 ) )
88 82 87 sylan ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑋 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑋 ) ∧ 𝑏 ∈ ( Base ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑋 ) 𝑎 ) ( +g ‘ 𝑋 ) 𝑏 ) ∈ ( Base ‘ 𝑋 ) )
89 64 65 66 69 72 73 74 79 88 islssd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → ( Base ‘ 𝑋 ) ∈ 𝑆 )
90 59 89 eqeltrd ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) → 𝑈 ∈ 𝑆 )
91 57 90 impbida ⊢ ( 𝑊 ∈ LMod → ( 𝑈 ∈ 𝑆 ↔ ( 𝑈 ⊆ 𝑉 ∧ 𝑋 ∈ LMod ) ) )