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 fex 
 |-  ( ( R : I --> LMod /\ I e. W ) -> R e. _V )
35 3 1 34 syl2anc 
 |-  ( ph -> R e. _V )
36 5 2 35 prdssca 
 |-  ( ph -> S = ( Scalar ` P ) )
37 36 fveq2d 
 |-  ( ph -> ( Base ` S ) = ( Base ` ( Scalar ` P ) ) )
38 37 eleq2d 
 |-  ( ph -> ( a e. ( Base ` S ) <-> a e. ( Base ` ( Scalar ` P ) ) ) )
39 38 biimpar 
 |-  ( ( ph /\ a e. ( Base ` ( Scalar ` P ) ) ) -> a e. ( Base ` S ) )
40 39 adantrr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> a e. ( Base ` S ) )
41 40 adantr 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> a e. ( Base ` S ) )
42 23 adantr 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> b e. ( Base ` P ) )
43 simpr 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> x e. I )
44 5 18 25 30 31 32 33 41 42 43 prdsvscafval 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( ( a ( .s ` P ) b ) ` x ) = ( a ( .s ` ( R ` x ) ) ( b ` x ) ) )
45 44 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 ) ) )
46 3 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( R ` x ) e. LMod )
47 46 adantlr 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( R ` x ) e. LMod )
48 simplrl 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> a e. ( Base ` ( Scalar ` P ) ) )
49 36 adantr 
 |-  ( ( ph /\ x e. I ) -> S = ( Scalar ` P ) )
50 4 49 eqtrd 
 |-  ( ( ph /\ x e. I ) -> ( Scalar ` ( R ` x ) ) = ( Scalar ` P ) )
51 50 fveq2d 
 |-  ( ( ph /\ x e. I ) -> ( Base ` ( Scalar ` ( R ` x ) ) ) = ( Base ` ( Scalar ` P ) ) )
52 51 adantlr 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( Base ` ( Scalar ` ( R ` x ) ) ) = ( Base ` ( Scalar ` P ) ) )
53 48 52 eleqtrrd 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> a e. ( Base ` ( Scalar ` ( R ` x ) ) ) )
54 eqid 
 |-  ( Scalar ` ( R ` x ) ) = ( Scalar ` ( R ` x ) )
55 eqid 
 |-  ( .s ` ( R ` x ) ) = ( .s ` ( R ` x ) )
56 eqid 
 |-  ( Base ` ( Scalar ` ( R ` x ) ) ) = ( Base ` ( Scalar ` ( R ` x ) ) )
57 eqid 
 |-  ( 0g ` ( R ` x ) ) = ( 0g ` ( R ` x ) )
58 54 55 56 57 lmodvs0 
 |-  ( ( ( R ` x ) e. LMod /\ a e. ( Base ` ( Scalar ` ( R ` x ) ) ) ) -> ( a ( .s ` ( R ` x ) ) ( 0g ` ( R ` x ) ) ) = ( 0g ` ( R ` x ) ) )
59 47 53 58 syl2anc 
 |-  ( ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) /\ x e. I ) -> ( a ( .s ` ( R ` x ) ) ( 0g ` ( R ` x ) ) ) = ( 0g ` ( R ` x ) ) )
60 oveq2 
 |-  ( ( b ` x ) = ( 0g ` ( R ` x ) ) -> ( a ( .s ` ( R ` x ) ) ( b ` x ) ) = ( a ( .s ` ( R ` x ) ) ( 0g ` ( R ` x ) ) ) )
61 60 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 ) ) ) )
62 59 61 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 ) ) ) )
63 62 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 ) ) )
64 45 63 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 ) ) )
65 64 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 ) ) ) )
66 65 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 ) ) ) )
67 66 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 ) ) } )
68 29 67 ssfid 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> { x e. I | ( ( a ( .s ` P ) b ) ` x ) =/= ( 0g ` ( R ` x ) ) } e. Fin )
69 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 ) ) )
70 69 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 ) ) )
71 28 68 70 mpbir2and 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. H ) ) -> ( a ( .s ` P ) b ) e. H )
72 71 ralrimivva 
 |-  ( ph -> A. a e. ( Base ` ( Scalar ` P ) ) A. b e. H ( a ( .s ` P ) b ) e. H )
73 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 ) ) )
74 13 73 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 ) ) )
75 12 72 74 mpbir2and 
 |-  ( ph -> H e. U )