# 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}\mathrm{freeLMod}{I}$
frlmsslss.u ${⊢}{U}=\mathrm{LSubSp}\left({Y}\right)$
frlmsslss.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
frlmsslss.z
frlmsslss.c
Assertion frlmsslss ${⊢}\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 frlmsslss.c
6 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {R}\in \mathrm{Ring}$
7 simp2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {I}\in {V}$
8 simp3 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {J}\subseteq {I}$
9 7 8 ssexd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {J}\in \mathrm{V}$
10 eqid ${⊢}{R}\mathrm{freeLMod}{J}={R}\mathrm{freeLMod}{J}$
11 10 4 frlm0
12 6 9 11 syl2anc
13 12 eqeq2d
14 13 rabbidv
15 5 14 syl5eq ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {C}=\left\{{x}\in {B}|{{x}↾}_{{J}}={0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}$
16 eqid ${⊢}{\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{J}\right)}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}{J}\right)}$
17 eqid ${⊢}\left({x}\in {B}⟼{{x}↾}_{{J}}\right)=\left({x}\in {B}⟼{{x}↾}_{{J}}\right)$
18 1 10 3 16 17 frlmsplit2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to \left({x}\in {B}⟼{{x}↾}_{{J}}\right)\in \left({Y}\mathrm{LMHom}\left({R}\mathrm{freeLMod}{J}\right)\right)$
19 fvex ${⊢}{0}_{\left({R}\mathrm{freeLMod}{J}\right)}\in \mathrm{V}$
20 17 mptiniseg ${⊢}{0}_{\left({R}\mathrm{freeLMod}{J}\right)}\in \mathrm{V}\to {\left({x}\in {B}⟼{{x}↾}_{{J}}\right)}^{-1}\left[\left\{{0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}\right]=\left\{{x}\in {B}|{{x}↾}_{{J}}={0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}$
21 19 20 ax-mp ${⊢}{\left({x}\in {B}⟼{{x}↾}_{{J}}\right)}^{-1}\left[\left\{{0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}\right]=\left\{{x}\in {B}|{{x}↾}_{{J}}={0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}$
22 21 eqcomi ${⊢}\left\{{x}\in {B}|{{x}↾}_{{J}}={0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}={\left({x}\in {B}⟼{{x}↾}_{{J}}\right)}^{-1}\left[\left\{{0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}\right]$
23 eqid ${⊢}{0}_{\left({R}\mathrm{freeLMod}{J}\right)}={0}_{\left({R}\mathrm{freeLMod}{J}\right)}$
24 22 23 2 lmhmkerlss ${⊢}\left({x}\in {B}⟼{{x}↾}_{{J}}\right)\in \left({Y}\mathrm{LMHom}\left({R}\mathrm{freeLMod}{J}\right)\right)\to \left\{{x}\in {B}|{{x}↾}_{{J}}={0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}\in {U}$
25 18 24 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to \left\{{x}\in {B}|{{x}↾}_{{J}}={0}_{\left({R}\mathrm{freeLMod}{J}\right)}\right\}\in {U}$
26 15 25 eqeltrd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {C}\in {U}$