MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpllsslem Structured version   Visualization version   GIF version
Theorem mpllsslem 21550
Description: If 𝐴 is an ideal of subsets (a nonempty collection closed under subset and binary union) of the set 𝐷 of finite bags (the primary applications being 𝐴 = Fin and 𝐴 = 𝒫 𝐡 for some 𝐡), then the set of all power series whose coefficient functions are supported on an element of 𝐴 is a linear subspace of the set of all power series. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 16-Jul-2019.)
Hypotheses
Ref Expression
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
Ref Expression
mpllsslem (πœ‘ β†’ π‘ˆ ∈ (LSubSpβ€˜π‘†))
Distinct variable groups:   𝑓,𝑔,π‘₯,𝑦, 0   𝐴,𝑓,𝑔,π‘₯,𝑦   𝐡,𝑓,𝑔   𝐷,𝑔   𝑓,𝐼   πœ‘,π‘₯,𝑦   𝑆,𝑓,𝑔,𝑦
Allowed substitution hints:   πœ‘(𝑓,𝑔)   𝐡(π‘₯,𝑦)   𝐷(π‘₯,𝑦,𝑓)   𝑅(π‘₯,𝑦,𝑓,𝑔)   𝑆(π‘₯)   π‘ˆ(π‘₯,𝑦,𝑓,𝑔)   𝐼(π‘₯,𝑦,𝑔)   π‘Š(π‘₯,𝑦,𝑓,𝑔)
Proof of Theorem mpllsslem
Dummy variables π‘˜ 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplsubglem.s . . 3 𝑆 = (𝐼 mPwSer 𝑅)
2 mplsubglem.i . . 3 (πœ‘ β†’ 𝐼 ∈ π‘Š)
3 mpllsslem.r . . 3 (πœ‘ β†’ 𝑅 ∈ Ring)
41, 2, 3psrsca 21499 . 2 (πœ‘ β†’ 𝑅 = (Scalarβ€˜π‘†))
5 eqidd 2733 . 2 (πœ‘ β†’ (Baseβ€˜π‘…) = (Baseβ€˜π‘…))
6 mplsubglem.b . . 3 𝐡 = (Baseβ€˜π‘†)
76a1i 11 . 2 (πœ‘ β†’ 𝐡 = (Baseβ€˜π‘†))
8 eqidd 2733 . 2 (πœ‘ β†’ (+gβ€˜π‘†) = (+gβ€˜π‘†))
9 eqidd 2733 . 2 (πœ‘ β†’ ( ·𝑠 β€˜π‘†) = ( ·𝑠 β€˜π‘†))
10 eqidd 2733 . 2 (πœ‘ β†’ (LSubSpβ€˜π‘†) = (LSubSpβ€˜π‘†))
11 mplsubglem.z . . . 4 0 = (0gβ€˜π‘…)
12 mplsubglem.d . . . 4 𝐷 = {𝑓 ∈ (β„•0 ↑m 𝐼) ∣ (◑𝑓 β€œ β„•) ∈ Fin}
13 mplsubglem.0 . . . 4 (πœ‘ β†’ βˆ… ∈ 𝐴)
14 mplsubglem.a . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) β†’ (π‘₯ βˆͺ 𝑦) ∈ 𝐴)
15 mplsubglem.y . . . 4 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ∧ 𝑦 βŠ† π‘₯)) β†’ 𝑦 ∈ 𝐴)
16 mplsubglem.u . . . 4 (πœ‘ β†’ π‘ˆ = {𝑔 ∈ 𝐡 ∣ (𝑔 supp 0 ) ∈ 𝐴})
17 ringgrp 20054 . . . . 5 (𝑅 ∈ Ring β†’ 𝑅 ∈ Grp)
183, 17syl 17 . . . 4 (πœ‘ β†’ 𝑅 ∈ Grp)
191, 6, 11, 12, 2, 13, 14, 15, 16, 18mplsubglem 21549 . . 3 (πœ‘ β†’ π‘ˆ ∈ (SubGrpβ€˜π‘†))
206subgss 19001 . . 3 (π‘ˆ ∈ (SubGrpβ€˜π‘†) β†’ π‘ˆ βŠ† 𝐡)
2119, 20syl 17 . 2 (πœ‘ β†’ π‘ˆ βŠ† 𝐡)
22 eqid 2732 . . . 4 (0gβ€˜π‘†) = (0gβ€˜π‘†)
2322subg0cl 19008 . . 3 (π‘ˆ ∈ (SubGrpβ€˜π‘†) β†’ (0gβ€˜π‘†) ∈ π‘ˆ)
24 ne0i 4333 . . 3 ((0gβ€˜π‘†) ∈ π‘ˆ β†’ π‘ˆ β‰  βˆ…)
2519, 23, 243syl 18 . 2 (πœ‘ β†’ π‘ˆ β‰  βˆ…)
2619adantr 481 . . 3 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ ∧ 𝑀 ∈ π‘ˆ)) β†’ π‘ˆ ∈ (SubGrpβ€˜π‘†))
27 eqid 2732 . . . . . 6 ( ·𝑠 β€˜π‘†) = ( ·𝑠 β€˜π‘†)
28 eqid 2732 . . . . . 6 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
293adantr 481 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ 𝑅 ∈ Ring)
30 simprl 769 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ 𝑒 ∈ (Baseβ€˜π‘…))
31 simprr 771 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ 𝑣 ∈ π‘ˆ)
3216adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ π‘ˆ = {𝑔 ∈ 𝐡 ∣ (𝑔 supp 0 ) ∈ 𝐴})
3332eleq2d 2819 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑣 ∈ π‘ˆ ↔ 𝑣 ∈ {𝑔 ∈ 𝐡 ∣ (𝑔 supp 0 ) ∈ 𝐴}))
34 oveq1 7412 . . . . . . . . . . 11 (𝑔 = 𝑣 β†’ (𝑔 supp 0 ) = (𝑣 supp 0 ))
3534eleq1d 2818 . . . . . . . . . 10 (𝑔 = 𝑣 β†’ ((𝑔 supp 0 ) ∈ 𝐴 ↔ (𝑣 supp 0 ) ∈ 𝐴))
3635elrab 3682 . . . . . . . . 9 (𝑣 ∈ {𝑔 ∈ 𝐡 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ (𝑣 ∈ 𝐡 ∧ (𝑣 supp 0 ) ∈ 𝐴))
3733, 36bitrdi 286 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑣 ∈ π‘ˆ ↔ (𝑣 ∈ 𝐡 ∧ (𝑣 supp 0 ) ∈ 𝐴)))
3831, 37mpbid 231 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑣 ∈ 𝐡 ∧ (𝑣 supp 0 ) ∈ 𝐴))
3938simpld 495 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ 𝑣 ∈ 𝐡)
401, 27, 28, 6, 29, 30, 39psrvscacl 21503 . . . . 5 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ 𝐡)
41 ovex 7438 . . . . . . 7 ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ V
4241a1i 11 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ V)
43 sseq2 4007 . . . . . . . . 9 (π‘₯ = (𝑣 supp 0 ) β†’ (𝑦 βŠ† π‘₯ ↔ 𝑦 βŠ† (𝑣 supp 0 )))
4443imbi1d 341 . . . . . . . 8 (π‘₯ = (𝑣 supp 0 ) β†’ ((𝑦 βŠ† π‘₯ β†’ 𝑦 ∈ 𝐴) ↔ (𝑦 βŠ† (𝑣 supp 0 ) β†’ 𝑦 ∈ 𝐴)))
4544albidv 1923 . . . . . . 7 (π‘₯ = (𝑣 supp 0 ) β†’ (βˆ€π‘¦(𝑦 βŠ† π‘₯ β†’ 𝑦 ∈ 𝐴) ↔ βˆ€π‘¦(𝑦 βŠ† (𝑣 supp 0 ) β†’ 𝑦 ∈ 𝐴)))
4615expr 457 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (𝑦 βŠ† π‘₯ β†’ 𝑦 ∈ 𝐴))
4746alrimiv 1930 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ βˆ€π‘¦(𝑦 βŠ† π‘₯ β†’ 𝑦 ∈ 𝐴))
4847ralrimiva 3146 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦(𝑦 βŠ† π‘₯ β†’ 𝑦 ∈ 𝐴))
4948adantr 481 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ βˆ€π‘₯ ∈ 𝐴 βˆ€π‘¦(𝑦 βŠ† π‘₯ β†’ 𝑦 ∈ 𝐴))
5038simprd 496 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑣 supp 0 ) ∈ 𝐴)
5145, 49, 50rspcdva 3613 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ βˆ€π‘¦(𝑦 βŠ† (𝑣 supp 0 ) β†’ 𝑦 ∈ 𝐴))
521, 28, 12, 6, 40psrelbas 21489 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑒( ·𝑠 β€˜π‘†)𝑣):𝐷⟢(Baseβ€˜π‘…))
53 eqid 2732 . . . . . . . . 9 (.rβ€˜π‘…) = (.rβ€˜π‘…)
5430adantr 481 . . . . . . . . 9 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ 𝑒 ∈ (Baseβ€˜π‘…))
5539adantr 481 . . . . . . . . 9 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ 𝑣 ∈ 𝐡)
56 eldifi 4125 . . . . . . . . . 10 (π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 )) β†’ π‘˜ ∈ 𝐷)
5756adantl 482 . . . . . . . . 9 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ π‘˜ ∈ 𝐷)
581, 27, 28, 6, 53, 12, 54, 55, 57psrvscaval 21502 . . . . . . . 8 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣)β€˜π‘˜) = (𝑒(.rβ€˜π‘…)(π‘£β€˜π‘˜)))
591, 28, 12, 6, 39psrelbas 21489 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ 𝑣:𝐷⟢(Baseβ€˜π‘…))
60 ssidd 4004 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑣 supp 0 ) βŠ† (𝑣 supp 0 ))
61 ovex 7438 . . . . . . . . . . . 12 (β„•0 ↑m 𝐼) ∈ V
6212, 61rabex2 5333 . . . . . . . . . . 11 𝐷 ∈ V
6362a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ 𝐷 ∈ V)
6411fvexi 6902 . . . . . . . . . . 11 0 ∈ V
6564a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ 0 ∈ V)
6659, 60, 63, 65suppssr 8177 . . . . . . . . 9 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ (π‘£β€˜π‘˜) = 0 )
6766oveq2d 7421 . . . . . . . 8 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ (𝑒(.rβ€˜π‘…)(π‘£β€˜π‘˜)) = (𝑒(.rβ€˜π‘…) 0 ))
6828, 53, 11ringrz 20101 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝑒 ∈ (Baseβ€˜π‘…)) β†’ (𝑒(.rβ€˜π‘…) 0 ) = 0 )
693, 30, 68syl2an2r 683 . . . . . . . . 9 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑒(.rβ€˜π‘…) 0 ) = 0 )
7069adantr 481 . . . . . . . 8 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ (𝑒(.rβ€˜π‘…) 0 ) = 0 )
7158, 67, 703eqtrd 2776 . . . . . . 7 (((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) ∧ π‘˜ ∈ (𝐷 βˆ– (𝑣 supp 0 ))) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣)β€˜π‘˜) = 0 )
7252, 71suppss 8175 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) βŠ† (𝑣 supp 0 ))
73 sseq1 4006 . . . . . . . 8 (𝑦 = ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) β†’ (𝑦 βŠ† (𝑣 supp 0 ) ↔ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) βŠ† (𝑣 supp 0 )))
74 eleq1 2821 . . . . . . . 8 (𝑦 = ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) β†’ (𝑦 ∈ 𝐴 ↔ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ 𝐴))
7573, 74imbi12d 344 . . . . . . 7 (𝑦 = ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) β†’ ((𝑦 βŠ† (𝑣 supp 0 ) β†’ 𝑦 ∈ 𝐴) ↔ (((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) βŠ† (𝑣 supp 0 ) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ 𝐴)))
7675spcgv 3586 . . . . . 6 (((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ V β†’ (βˆ€π‘¦(𝑦 βŠ† (𝑣 supp 0 ) β†’ 𝑦 ∈ 𝐴) β†’ (((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) βŠ† (𝑣 supp 0 ) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ 𝐴)))
7742, 51, 72, 76syl3c 66 . . . . 5 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ 𝐴)
7832eleq2d 2819 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ π‘ˆ ↔ (𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ {𝑔 ∈ 𝐡 ∣ (𝑔 supp 0 ) ∈ 𝐴}))
79 oveq1 7412 . . . . . . . 8 (𝑔 = (𝑒( ·𝑠 β€˜π‘†)𝑣) β†’ (𝑔 supp 0 ) = ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ))
8079eleq1d 2818 . . . . . . 7 (𝑔 = (𝑒( ·𝑠 β€˜π‘†)𝑣) β†’ ((𝑔 supp 0 ) ∈ 𝐴 ↔ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ 𝐴))
8180elrab 3682 . . . . . 6 ((𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ {𝑔 ∈ 𝐡 ∣ (𝑔 supp 0 ) ∈ 𝐴} ↔ ((𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ 𝐡 ∧ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ 𝐴))
8278, 81bitrdi 286 . . . . 5 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ π‘ˆ ↔ ((𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ 𝐡 ∧ ((𝑒( ·𝑠 β€˜π‘†)𝑣) supp 0 ) ∈ 𝐴)))
8340, 77, 82mpbir2and 711 . . . 4 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ)) β†’ (𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ π‘ˆ)
84833adantr3 1171 . . 3 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ ∧ 𝑀 ∈ π‘ˆ)) β†’ (𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ π‘ˆ)
85 simpr3 1196 . . 3 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ ∧ 𝑀 ∈ π‘ˆ)) β†’ 𝑀 ∈ π‘ˆ)
86 eqid 2732 . . . 4 (+gβ€˜π‘†) = (+gβ€˜π‘†)
8786subgcl 19010 . . 3 ((π‘ˆ ∈ (SubGrpβ€˜π‘†) ∧ (𝑒( ·𝑠 β€˜π‘†)𝑣) ∈ π‘ˆ ∧ 𝑀 ∈ π‘ˆ) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣)(+gβ€˜π‘†)𝑀) ∈ π‘ˆ)
8826, 84, 85, 87syl3anc 1371 . 2 ((πœ‘ ∧ (𝑒 ∈ (Baseβ€˜π‘…) ∧ 𝑣 ∈ π‘ˆ ∧ 𝑀 ∈ π‘ˆ)) β†’ ((𝑒( ·𝑠 β€˜π‘†)𝑣)(+gβ€˜π‘†)𝑀) ∈ π‘ˆ)
894, 5, 7, 8, 9, 10, 21, 25, 88islssd 20538 1 (πœ‘ β†’ π‘ˆ ∈ (LSubSpβ€˜π‘†))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087  βˆ€wal 1539   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  {crab 3432  Vcvv 3474   βˆ– cdif 3944   βˆͺ cun 3945   βŠ† wss 3947  βˆ…c0 4321  β—‘ccnv 5674   β€œ cima 5678  β€˜cfv 6540  (class class class)co 7405   supp csupp 8142   ↑m cmap 8816  Fincfn 8935  β„•cn 12208  β„•0cn0 12468  Basecbs 17140  +gcplusg 17193  .rcmulr 17194   ·𝑠 cvsca 17197  0gc0g 17381  Grpcgrp 18815  SubGrpcsubg 18994  Ringcrg 20049  LSubSpclss 20534   mPwSer cmps 21448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-fz 13481  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-hom 17217  df-cco 17218  df-0g 17383  df-prds 17389  df-pws 17391  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-grp 18818  df-minusg 18819  df-subg 18997  df-mgp 19982  df-ring 20051  df-lss 20535  df-psr 21453
This theorem is referenced by:  mpllss  21553
  Copyright terms: Public domain W3C validator