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