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 )