Metamath Proof Explorer


Theorem dsmmlss

Description: The finite hull of a product of modules is additionally closed under scalar multiplication and thus is a linear subspace of the product. (Contributed by Stefan O'Rear, 11-Jan-2015)

Ref Expression
Hypotheses dsmmlss.i
|- ( ph -> I e. W )
dsmmlss.s
|- ( ph -> S e. Ring )
dsmmlss.r
|- ( ph -> R : I --> LMod )
dsmmlss.k
|- ( ( ph /\ x e. I ) -> ( Scalar ` ( R ` x ) ) = S )
dsmmlss.p
|- P = ( S Xs_ R )
dsmmlss.u
|- U = ( LSubSp ` P )
dsmmlss.h
|- H = ( Base ` ( S (+)m R ) )
Assertion dsmmlss
|- ( ph -> H e. U )

Proof

Step Hyp Ref Expression
1 dsmmlss.i
 |-  ( ph -> I e. W )
2 dsmmlss.s
 |-  ( ph -> S e. Ring )
3 dsmmlss.r
 |-  ( ph -> R : I --> LMod )
4 dsmmlss.k
 |-  ( ( ph /\ x e. I ) -> ( Scalar ` ( R ` x ) ) = S )
5 dsmmlss.p
 |-  P = ( S Xs_ R )
6 dsmmlss.u
 |-  U = ( LSubSp ` P )
7 dsmmlss.h
 |-  H = ( Base ` ( S (+)m R ) )
8 lmodgrp
 |-  ( a e. LMod -> a e. Grp )
9 8 ssriv
 |-  LMod C_ Grp
10 fss
 |-  ( ( R : I --> LMod /\ LMod C_ Grp ) -> R : I --> Grp )
11 3 9 10 sylancl
 |-  ( ph -> R : I --> Grp )
12 5 7 1 2 11 dsmmsubg
 |-  ( ph -> H e. ( SubGrp ` P ) )
13 5 2 1 3 4 prdslmodd
 |-  ( ph -> P e. LMod )
14 13 adantr
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> P e. LMod )
15 simprl
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> a e. ( Base ` ( Scalar ` P ) ) )
16 simprr
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> b e. H )
17 eqid
 |-  ( S (+)m R ) = ( S (+)m R )
18 eqid
 |-  ( Base ` P ) = ( Base ` P )
19 3 ffnd
 |-  ( ph -> R Fn I )
20 5 17 18 7 1 19 dsmmelbas
 |-  ( ph -> ( b e. H <-> ( b e. ( Base ` P ) /\ { x e. I | ( b ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin ) ) )
21 20 adantr
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> ( b e. H <-> ( b e. ( Base ` P ) /\ { x e. I | ( b ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin ) ) )
22 16 21 mpbid
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> ( b e. ( Base ` P ) /\ { x e. I | ( b ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin ) )
23 22 simpld
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> b e. ( Base ` P ) )
24 eqid
 |-  ( Scalar ` P ) = ( Scalar ` P )
25 eqid
 |-  ( .s ` P ) = ( .s ` P )
26 eqid
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
27 18 24 25 26 lmodvscl
 |-  ( ( P e. LMod /\ a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( Base ` P ) ) -> ( a ( .s ` P ) b ) e. ( Base ` P ) )
28 14 15 23 27 syl3anc
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> ( a ( .s ` P ) b ) e. ( Base ` P ) )
29 22 simprd
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> { x e. I | ( b ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin )
30 eqid
 |-  ( Base ` S ) = ( Base ` S )
31 2 ad2antrr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> S e. Ring )
32 1 ad2antrr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> I e. W )
33 19 ad2antrr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> R Fn I )
34 3 1 fexd
 |-  ( ph -> R e. _V )
35 5 2 34 prdssca
 |-  ( ph -> S = ( Scalar ` P ) )
36 35 fveq2d
 |-  ( ph -> ( Base ` S ) = ( Base ` ( Scalar ` P ) ) )
37 36 eleq2d
 |-  ( ph -> ( a e. ( Base ` S ) <-> a e. ( Base ` ( Scalar ` P ) ) ) )
38 37 biimpar
 |-  ( ( ph /\ a e. ( Base ` ( Scalar ` P ) ) ) -> a e. ( Base ` S ) )
39 38 adantrr
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> a e. ( Base ` S ) )
40 39 adantr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> a e. ( Base ` S ) )
41 23 adantr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> b e. ( Base ` P ) )
42 simpr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> x e. I )
43 5 18 25 30 31 32 33 40 41 42 prdsvscafval
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( ( a ( .s ` P ) b ) ` x ) = ( a ( .s ` ( R ` x ) ) ( b ` x ) ) )
44 43 adantrr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ ( x e. I /\ ( b ` x ) = ( 0g ` ( R ` x ) ) ) ) -> ( ( a ( .s ` P ) b ) ` x ) = ( a ( .s ` ( R ` x ) ) ( b ` x ) ) )
45 3 ffvelrnda
 |-  ( ( ph /\ x e. I ) -> ( R ` x ) e. LMod )
46 45 adantlr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( R ` x ) e. LMod )
47 simplrl
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> a e. ( Base ` ( Scalar ` P ) ) )
48 35 adantr
 |-  ( ( ph /\ x e. I ) -> S = ( Scalar ` P ) )
49 4 48 eqtrd
 |-  ( ( ph /\ x e. I ) -> ( Scalar ` ( R ` x ) ) = ( Scalar ` P ) )
50 49 fveq2d
 |-  ( ( ph /\ x e. I ) -> ( Base ` ( Scalar ` ( R ` x ) ) ) = ( Base ` ( Scalar ` P ) ) )
51 50 adantlr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( Base ` ( Scalar ` ( R ` x ) ) ) = ( Base ` ( Scalar ` P ) ) )
52 47 51 eleqtrrd
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> a e. ( Base ` ( Scalar ` ( R ` x ) ) ) )
53 eqid
 |-  ( Scalar ` ( R ` x ) ) = ( Scalar ` ( R ` x ) )
54 eqid
 |-  ( .s ` ( R ` x ) ) = ( .s ` ( R ` x ) )
55 eqid
 |-  ( Base ` ( Scalar ` ( R ` x ) ) ) = ( Base ` ( Scalar ` ( R ` x ) ) )
56 eqid
 |-  ( 0g ` ( R ` x ) ) = ( 0g ` ( R ` x ) )
57 53 54 55 56 lmodvs0
 |-  ( ( ( R ` x ) e. LMod /\ a e. ( Base ` ( Scalar ` ( R ` x ) ) ) ) -> ( a ( .s ` ( R ` x ) ) ( 0g ` ( R ` x ) ) ) = ( 0g ` ( R ` x ) ) )
58 46 52 57 syl2anc
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( a ( .s ` ( R ` x ) ) ( 0g ` ( R ` x ) ) ) = ( 0g ` ( R ` x ) ) )
59 oveq2
 |-  ( ( b ` x ) = ( 0g ` ( R ` x ) ) -> ( a ( .s ` ( R ` x ) ) ( b ` x ) ) = ( a ( .s ` ( R ` x ) ) ( 0g ` ( R ` x ) ) ) )
60 59 eqeq1d
 |-  ( ( b ` x ) = ( 0g ` ( R ` x ) ) -> ( ( a ( .s ` ( R ` x ) ) ( b ` x ) ) = ( 0g ` ( R ` x ) ) <-> ( a ( .s ` ( R ` x ) ) ( 0g ` ( R ` x ) ) ) = ( 0g ` ( R ` x ) ) ) )
61 58 60 syl5ibrcom
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( ( b ` x ) = ( 0g ` ( R ` x ) ) -> ( a ( .s ` ( R ` x ) ) ( b ` x ) ) = ( 0g ` ( R ` x ) ) ) )
62 61 impr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ ( x e. I /\ ( b ` x ) = ( 0g ` ( R ` x ) ) ) ) -> ( a ( .s ` ( R ` x ) ) ( b ` x ) ) = ( 0g ` ( R ` x ) ) )
63 44 62 eqtrd
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ ( x e. I /\ ( b ` x ) = ( 0g ` ( R ` x ) ) ) ) -> ( ( a ( .s ` P ) b ) ` x ) = ( 0g ` ( R ` x ) ) )
64 63 expr
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( ( b ` x ) = ( 0g ` ( R ` x ) ) -> ( ( a ( .s ` P ) b ) ` x ) = ( 0g ` ( R ` x ) ) ) )
65 64 necon3d
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( ( ( a ( .s ` P ) b ) ` x ) =/= ( 0g ` ( R ` x ) ) -> ( b ` x ) =/= ( 0g ` ( R ` x ) ) ) )
66 65 ss2rabdv
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> { x e. I | ( ( a ( .s ` P ) b ) ` x ) =/= ( 0g ` ( R ` x ) ) } C_ { x e. I | ( b ` x ) =/= ( 0g ` ( R ` x ) ) } )
67 29 66 ssfid
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> { x e. I | ( ( a ( .s ` P ) b ) ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin )
68 5 17 18 7 1 19 dsmmelbas
 |-  ( ph -> ( ( a ( .s ` P ) b ) e. H <-> ( ( a ( .s ` P ) b ) e. ( Base ` P ) /\ { x e. I | ( ( a ( .s ` P ) b ) ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin ) ) )
69 68 adantr
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> ( ( a ( .s ` P ) b ) e. H <-> ( ( a ( .s ` P ) b ) e. ( Base ` P ) /\ { x e. I | ( ( a ( .s ` P ) b ) ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin ) ) )
70 28 67 69 mpbir2and
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> ( a ( .s ` P ) b ) e. H )
71 70 ralrimivva
 |-  ( ph -> A. a e. ( Base ` ( Scalar ` P ) ) A. b e. H ( a ( .s ` P ) b ) e. H )
72 24 26 18 25 6 islss4
 |-  ( P e. LMod -> ( H e. U <-> ( H e. ( SubGrp ` P ) /\ A. a e. ( Base ` ( Scalar ` P ) ) A. b e. H ( a ( .s ` P ) b ) e. H ) ) )
73 13 72 syl
 |-  ( ph -> ( H e. U <-> ( H e. ( SubGrp ` P ) /\ A. a e. ( Base ` ( Scalar ` P ) ) A. b e. H ( a ( .s ` P ) b ) e. H ) ) )
74 12 71 73 mpbir2and
 |-  ( ph -> H e. U )