# 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}\mathrm{freeLMod}{I}$
frlmsslss.u ${⊢}{U}=\mathrm{LSubSp}\left({Y}\right)$
frlmsslss.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
frlmsslss.z
frlmsslss2.c
Assertion frlmsslss2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {C}\in {U}$

### Proof

Step Hyp Ref Expression
1 frlmsslss.y ${⊢}{Y}={R}\mathrm{freeLMod}{I}$
2 frlmsslss.u ${⊢}{U}=\mathrm{LSubSp}\left({Y}\right)$
3 frlmsslss.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
4 frlmsslss.z
5 frlmsslss2.c
6 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
7 1 6 3 frlmbasf ${⊢}\left({I}\in {V}\wedge {x}\in {B}\right)\to {x}:{I}⟶{\mathrm{Base}}_{{R}}$
8 7 3ad2antl2 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to {x}:{I}⟶{\mathrm{Base}}_{{R}}$
9 8 ffnd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to {x}Fn{I}$
10 simpl3 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to {J}\subseteq {I}$
11 undif ${⊢}{J}\subseteq {I}↔{J}\cup \left({I}\setminus {J}\right)={I}$
12 10 11 sylib ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to {J}\cup \left({I}\setminus {J}\right)={I}$
13 12 fneq2d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to \left({x}Fn\left({J}\cup \left({I}\setminus {J}\right)\right)↔{x}Fn{I}\right)$
14 9 13 mpbird ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to {x}Fn\left({J}\cup \left({I}\setminus {J}\right)\right)$
15 simpr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to {x}\in {B}$
16 4 fvexi
17 16 a1i
18 disjdif ${⊢}{J}\cap \left({I}\setminus {J}\right)=\varnothing$
19 18 a1i ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\wedge {x}\in {B}\right)\to {J}\cap \left({I}\setminus {J}\right)=\varnothing$
20 fnsuppres
21 14 15 17 19 20 syl121anc
22 21 rabbidva
23 5 22 syl5eq
24 difssd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {I}\setminus {J}\subseteq {I}$
25 eqid
26 1 2 3 4 25 frlmsslss
27 24 26 syld3an3
28 23 27 eqeltrd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {C}\in {U}$