Metamath Proof Explorer

Theorem mpllsslem

Description: If A is an ideal of subsets (a nonempty collection closed under subset and binary union) of the set D of finite bags (the primary applications being A = Fin and A = ~P B for some B ), then the set of all power series whose coefficient functions are supported on an element of A is a linear subspace of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015) (Revised by AV, 16-Jul-2019)

Ref Expression
Hypotheses mplsubglem.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplsubglem.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
mplsubglem.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplsubglem.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplsubglem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplsubglem.0 ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
mplsubglem.a ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝐴 )
mplsubglem.y ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ 𝐴 )
mplsubglem.u ⊢ ( 𝜑 → 𝑈 = { 𝑔 ∈ 𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
mpllsslem.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion mpllsslem ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mplsubglem.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 mplsubglem.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 mplsubglem.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mplsubglem.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
5 mplsubglem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mplsubglem.0 ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
7 mplsubglem.a ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝐴 )
8 mplsubglem.y ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑦 ∈ 𝐴 )
9 mplsubglem.u ⊢ ( 𝜑 → 𝑈 = { 𝑔 ∈ 𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
10 mpllsslem.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
11 1 5 10 psrsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )
12 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
13 2 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑆 ) )
14 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) )
15 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 ) )
16 eqidd ⊢ ( 𝜑 → ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 ) )
17 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
18 10 17 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
19 1 2 3 4 5 6 7 8 9 18 mplsubglem ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑆 ) )
20 2 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) → 𝑈 ⊆ 𝐵 )
21 19 20 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
22 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
23 22 subg0cl ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) ∈ 𝑈 )
24 ne0i ⊢ ( ( 0g ‘ 𝑆 ) ∈ 𝑈 → 𝑈 ≠ ∅ )
25 19 23 24 3syl ⊢ ( 𝜑 → 𝑈 ≠ ∅ )
26 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑆 ) )
27 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
28 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
29 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑅 ∈ Ring )
30 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
31 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑣 ∈ 𝑈 )
32 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑈 = { 𝑔 ∈ 𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } )
33 32 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑣 ∈ 𝑈 ↔ 𝑣 ∈ { 𝑔 ∈ 𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
34 oveq1 ⊢ ( 𝑔 = 𝑣 → ( 𝑔 supp 0 ) = ( 𝑣 supp 0 ) )
35 34 eleq1d ⊢ ( 𝑔 = 𝑣 → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
36 35 elrab ⊢ ( 𝑣 ∈ { 𝑔 ∈ 𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( 𝑣 ∈ 𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
37 33 36 syl6bb ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑣 ∈ 𝑈 ↔ ( 𝑣 ∈ 𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) ) )
38 31 37 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑣 ∈ 𝐵 ∧ ( 𝑣 supp 0 ) ∈ 𝐴 ) )
39 38 simpld ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑣 ∈ 𝐵 )
40 1 27 28 2 29 30 39 psrvscacl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝐵 )
41 ovex ⊢ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ V
42 41 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ V )
43 sseq2 ⊢ ( 𝑥 = ( 𝑣 supp 0 ) → ( 𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ( 𝑣 supp 0 ) ) )
44 43 imbi1d ⊢ ( 𝑥 = ( 𝑣 supp 0 ) → ( ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦 ∈ 𝐴 ) ) )
45 44 albidv ⊢ ( 𝑥 = ( 𝑣 supp 0 ) → ( ∀ 𝑦 ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦 ∈ 𝐴 ) ) )
46 8 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴 ) )
47 46 alrimiv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴 ) )
48 47 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝐴 ) )
50 38 simprd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑣 supp 0 ) ∈ 𝐴 )
51 45 49 50 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ∀ 𝑦 ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦 ∈ 𝐴 ) )
52 1 28 4 2 40 psrelbas ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
53 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
54 30 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → 𝑢 ∈ ( Base ‘ 𝑅 ) )
55 39 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → 𝑣 ∈ 𝐵 )
56 eldifi ⊢ ( 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) → 𝑘 ∈ 𝐷 )
57 56 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → 𝑘 ∈ 𝐷 )
58 1 27 28 2 53 4 54 55 57 psrvscaval ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ‘ 𝑘 ) = ( 𝑢 ( .r ‘ 𝑅 ) ( 𝑣 ‘ 𝑘 ) ) )
59 1 28 4 2 39 psrelbas ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝑣 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
60 ssidd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑣 supp 0 ) ⊆ ( 𝑣 supp 0 ) )
61 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
62 4 61 rabex2 ⊢ 𝐷 ∈ V
63 62 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 𝐷 ∈ V )
64 3 fvexi ⊢ 0 ∈ V
65 64 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → 0 ∈ V )
66 59 60 63 65 suppssr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( 𝑣 ‘ 𝑘 ) = 0 )
67 66 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( 𝑢 ( .r ‘ 𝑅 ) ( 𝑣 ‘ 𝑘 ) ) = ( 𝑢 ( .r ‘ 𝑅 ) 0 ) )
68 28 53 3 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑢 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑢 ( .r ‘ 𝑅 ) 0 ) = 0 )
69 10 30 68 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑢 ( .r ‘ 𝑅 ) 0 ) = 0 )
70 69 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( 𝑢 ( .r ‘ 𝑅 ) 0 ) = 0 )
71 58 67 70 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑣 supp 0 ) ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ‘ 𝑘 ) = 0 )
72 52 71 suppss ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) )
73 sseq1 ⊢ ( 𝑦 = ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) → ( 𝑦 ⊆ ( 𝑣 supp 0 ) ↔ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) ) )
74 eleq1 ⊢ ( 𝑦 = ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) → ( 𝑦 ∈ 𝐴 ↔ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
75 73 74 imbi12d ⊢ ( 𝑦 = ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) → ( ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦 ∈ 𝐴 ) ↔ ( ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
76 75 spcgv ⊢ ( ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ V → ( ∀ 𝑦 ( 𝑦 ⊆ ( 𝑣 supp 0 ) → 𝑦 ∈ 𝐴 ) → ( ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ⊆ ( 𝑣 supp 0 ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
77 42 51 72 76 syl3c ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 )
78 32 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝑈 ↔ ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ { 𝑔 ∈ 𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ) )
79 oveq1 ⊢ ( 𝑔 = ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) → ( 𝑔 supp 0 ) = ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) )
80 79 eleq1d ⊢ ( 𝑔 = ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) → ( ( 𝑔 supp 0 ) ∈ 𝐴 ↔ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
81 80 elrab ⊢ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ { 𝑔 ∈ 𝐵 ∣ ( 𝑔 supp 0 ) ∈ 𝐴 } ↔ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝐵 ∧ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) )
82 78 81 syl6bb ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝑈 ↔ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝐵 ∧ ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) supp 0 ) ∈ 𝐴 ) ) )
83 40 77 82 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ) ) → ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝑈 )
84 83 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈 ) ) → ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝑈 )
85 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈 ) ) → 𝑤 ∈ 𝑈 )
86 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
87 86 subgcl ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑆 ) ∧ ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ∈ 𝑈 ∧ 𝑤 ∈ 𝑈 ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ( +g ‘ 𝑆 ) 𝑤 ) ∈ 𝑈 )
88 26 84 85 87 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( Base ‘ 𝑅 ) ∧ 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈 ) ) → ( ( 𝑢 ( ·𝑠 ‘ 𝑆 ) 𝑣 ) ( +g ‘ 𝑆 ) 𝑤 ) ∈ 𝑈 )
89 11 12 13 14 15 16 21 25 88 islssd ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑆 ) )