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 ) )
8 7 3ad2antl2 
 |-  ( ( ( 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 )