This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda 
 |-  ( ( 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 )