Step |
Hyp |
Ref |
Expression |
1 |
|
frlmsslss.y |
|- Y = ( R freeLMod I ) |
2 |
|
frlmsslss.u |
|- U = ( LSubSp ` Y ) |
3 |
|
frlmsslss.b |
|- B = ( Base ` Y ) |
4 |
|
frlmsslss.z |
|- .0. = ( 0g ` R ) |
5 |
|
frlmsslss.c |
|- C = { x e. B | ( x |` J ) = ( J X. { .0. } ) } |
6 |
|
simp1 |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> R e. Ring ) |
7 |
|
simp2 |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> I e. V ) |
8 |
|
simp3 |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> J C_ I ) |
9 |
7 8
|
ssexd |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> J e. _V ) |
10 |
|
eqid |
|- ( R freeLMod J ) = ( R freeLMod J ) |
11 |
10 4
|
frlm0 |
|- ( ( R e. Ring /\ J e. _V ) -> ( J X. { .0. } ) = ( 0g ` ( R freeLMod J ) ) ) |
12 |
6 9 11
|
syl2anc |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( J X. { .0. } ) = ( 0g ` ( R freeLMod J ) ) ) |
13 |
12
|
eqeq2d |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( ( x |` J ) = ( J X. { .0. } ) <-> ( x |` J ) = ( 0g ` ( R freeLMod J ) ) ) ) |
14 |
13
|
rabbidv |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> { x e. B | ( x |` J ) = ( J X. { .0. } ) } = { x e. B | ( x |` J ) = ( 0g ` ( R freeLMod J ) ) } ) |
15 |
5 14
|
syl5eq |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C = { x e. B | ( x |` J ) = ( 0g ` ( R freeLMod J ) ) } ) |
16 |
|
eqid |
|- ( Base ` ( R freeLMod J ) ) = ( Base ` ( R freeLMod J ) ) |
17 |
|
eqid |
|- ( x e. B |-> ( x |` J ) ) = ( x e. B |-> ( x |` J ) ) |
18 |
1 10 3 16 17
|
frlmsplit2 |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( x e. B |-> ( x |` J ) ) e. ( Y LMHom ( R freeLMod J ) ) ) |
19 |
|
fvex |
|- ( 0g ` ( R freeLMod J ) ) e. _V |
20 |
17
|
mptiniseg |
|- ( ( 0g ` ( R freeLMod J ) ) e. _V -> ( `' ( x e. B |-> ( x |` J ) ) " { ( 0g ` ( R freeLMod J ) ) } ) = { x e. B | ( x |` J ) = ( 0g ` ( R freeLMod J ) ) } ) |
21 |
19 20
|
ax-mp |
|- ( `' ( x e. B |-> ( x |` J ) ) " { ( 0g ` ( R freeLMod J ) ) } ) = { x e. B | ( x |` J ) = ( 0g ` ( R freeLMod J ) ) } |
22 |
21
|
eqcomi |
|- { x e. B | ( x |` J ) = ( 0g ` ( R freeLMod J ) ) } = ( `' ( x e. B |-> ( x |` J ) ) " { ( 0g ` ( R freeLMod J ) ) } ) |
23 |
|
eqid |
|- ( 0g ` ( R freeLMod J ) ) = ( 0g ` ( R freeLMod J ) ) |
24 |
22 23 2
|
lmhmkerlss |
|- ( ( x e. B |-> ( x |` J ) ) e. ( Y LMHom ( R freeLMod J ) ) -> { x e. B | ( x |` J ) = ( 0g ` ( R freeLMod J ) ) } e. U ) |
25 |
18 24
|
syl |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> { x e. B | ( x |` J ) = ( 0g ` ( R freeLMod J ) ) } e. U ) |
26 |
15 25
|
eqeltrd |
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C e. U ) |