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 𝑌 = ( 𝑅 freeLMod 𝐼 )
frlmsslss.u 𝑈 = ( LSubSp ‘ 𝑌 )
frlmsslss.b 𝐵 = ( Base ‘ 𝑌 )
frlmsslss.z 0 = ( 0g𝑅 )
frlmsslss.c 𝐶 = { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 𝐽 × { 0 } ) }
Assertion frlmsslss ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐶𝑈 )

Proof

Step Hyp Ref Expression
1 frlmsslss.y 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmsslss.u 𝑈 = ( LSubSp ‘ 𝑌 )
3 frlmsslss.b 𝐵 = ( Base ‘ 𝑌 )
4 frlmsslss.z 0 = ( 0g𝑅 )
5 frlmsslss.c 𝐶 = { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 𝐽 × { 0 } ) }
6 simp1 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝑅 ∈ Ring )
7 simp2 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐼𝑉 )
8 simp3 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐽𝐼 )
9 7 8 ssexd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐽 ∈ V )
10 eqid ( 𝑅 freeLMod 𝐽 ) = ( 𝑅 freeLMod 𝐽 )
11 10 4 frlm0 ( ( 𝑅 ∈ Ring ∧ 𝐽 ∈ V ) → ( 𝐽 × { 0 } ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) )
12 6 9 11 syl2anc ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → ( 𝐽 × { 0 } ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) )
13 12 eqeq2d ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → ( ( 𝑥𝐽 ) = ( 𝐽 × { 0 } ) ↔ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) ) )
14 13 rabbidv ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 𝐽 × { 0 } ) } = { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } )
15 5 14 syl5eq ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐶 = { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } )
16 eqid ( Base ‘ ( 𝑅 freeLMod 𝐽 ) ) = ( Base ‘ ( 𝑅 freeLMod 𝐽 ) )
17 eqid ( 𝑥𝐵 ↦ ( 𝑥𝐽 ) ) = ( 𝑥𝐵 ↦ ( 𝑥𝐽 ) )
18 1 10 3 16 17 frlmsplit2 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → ( 𝑥𝐵 ↦ ( 𝑥𝐽 ) ) ∈ ( 𝑌 LMHom ( 𝑅 freeLMod 𝐽 ) ) )
19 fvex ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) ∈ V
20 17 mptiniseg ( ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) ∈ V → ( ( 𝑥𝐵 ↦ ( 𝑥𝐽 ) ) “ { ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } ) = { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } )
21 19 20 ax-mp ( ( 𝑥𝐵 ↦ ( 𝑥𝐽 ) ) “ { ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } ) = { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) }
22 21 eqcomi { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } = ( ( 𝑥𝐵 ↦ ( 𝑥𝐽 ) ) “ { ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } )
23 eqid ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) )
24 22 23 2 lmhmkerlss ( ( 𝑥𝐵 ↦ ( 𝑥𝐽 ) ) ∈ ( 𝑌 LMHom ( 𝑅 freeLMod 𝐽 ) ) → { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } ∈ 𝑈 )
25 18 24 syl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → { 𝑥𝐵 ∣ ( 𝑥𝐽 ) = ( 0g ‘ ( 𝑅 freeLMod 𝐽 ) ) } ∈ 𝑈 )
26 15 25 eqeltrd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐶𝑈 )