# Metamath Proof Explorer

## Theorem frlmsslss2

Description: A subset of a free module obtained by restricting the support set is a submodule. J is the set of permitted unit vectors. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 23-Jun-2019)

Ref Expression
Hypotheses frlmsslss.y
`|- Y = ( R freeLMod I )`
frlmsslss.u
`|- U = ( LSubSp ` Y )`
frlmsslss.b
`|- B = ( Base ` Y )`
frlmsslss.z
`|- .0. = ( 0g ` R )`
frlmsslss2.c
`|- C = { x e. B | ( x supp .0. ) C_ J }`
Assertion frlmsslss2
`|- ( ( 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 frlmsslss2.c
` |-  C = { x e. B | ( x supp .0. ) C_ J }`
6 eqid
` |-  ( Base ` R ) = ( Base ` R )`
7 1 6 3 frlmbasf
` |-  ( ( I e. V /\ x e. B ) -> x : I --> ( Base ` R ) )`
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> x : I --> ( Base ` R ) )`
9 8 ffnd
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> x Fn I )`
10 simpl3
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> J C_ I )`
11 undif
` |-  ( J C_ I <-> ( J u. ( I \ J ) ) = I )`
12 10 11 sylib
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> ( J u. ( I \ J ) ) = I )`
13 12 fneq2d
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> ( x Fn ( J u. ( I \ J ) ) <-> x Fn I ) )`
14 9 13 mpbird
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> x Fn ( J u. ( I \ J ) ) )`
15 simpr
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> x e. B )`
16 4 fvexi
` |-  .0. e. _V`
17 16 a1i
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> .0. e. _V )`
18 disjdif
` |-  ( J i^i ( I \ J ) ) = (/)`
19 18 a1i
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> ( J i^i ( I \ J ) ) = (/) )`
20 fnsuppres
` |-  ( ( x Fn ( J u. ( I \ J ) ) /\ ( x e. B /\ .0. e. _V ) /\ ( J i^i ( I \ J ) ) = (/) ) -> ( ( x supp .0. ) C_ J <-> ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) ) )`
21 14 15 17 19 20 syl121anc
` |-  ( ( ( R e. Ring /\ I e. V /\ J C_ I ) /\ x e. B ) -> ( ( x supp .0. ) C_ J <-> ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) ) )`
22 21 rabbidva
` |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> { x e. B | ( x supp .0. ) C_ J } = { x e. B | ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) } )`
23 5 22 syl5eq
` |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C = { x e. B | ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) } )`
24 difssd
` |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> ( I \ J ) C_ I )`
25 eqid
` |-  { x e. B | ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) } = { x e. B | ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) }`
26 1 2 3 4 25 frlmsslss
` |-  ( ( R e. Ring /\ I e. V /\ ( I \ J ) C_ I ) -> { x e. B | ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) } e. U )`
27 24 26 syld3an3
` |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> { x e. B | ( x |` ( I \ J ) ) = ( ( I \ J ) X. { .0. } ) } e. U )`
28 23 27 eqeltrd
` |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C e. U )`