Metamath Proof Explorer

Theorem frlmsslss

Description: A subset of a free module obtained by restricting the support set is a submodule. J is the set of forbidden unit vectors. (Contributed by Stefan O'Rear, 4-Feb-2015)

Ref Expression
Hypotheses frlmsslss.y 
|- Y = ( R freeLMod I )
frlmsslss.u 
|- U = ( LSubSp ` Y )
frlmsslss.b 
|- B = ( Base ` Y )
frlmsslss.z 
|- .0. = ( 0g ` R )
frlmsslss.c 
|- C = { x e. B | ( x |` J ) = ( J X. { .0. } ) }
Assertion frlmsslss 
|- ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C e. U )

Proof

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 )