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

### Proof

Step Hyp Ref Expression
1 frlmsslss.y 𝑌 = ( 𝑅 freeLMod 𝐼 )
2 frlmsslss.u 𝑈 = ( LSubSp ‘ 𝑌 )
3 frlmsslss.b 𝐵 = ( Base ‘ 𝑌 )
4 frlmsslss.z 0 = ( 0g𝑅 )
5 frlmsslss2.c 𝐶 = { 𝑥𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 }
6 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 1 6 3 frlmbasf ( ( 𝐼𝑉𝑥𝐵 ) → 𝑥 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
8 7 3ad2antl2 ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → 𝑥 : 𝐼 ⟶ ( Base ‘ 𝑅 ) )
9 8 ffnd ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → 𝑥 Fn 𝐼 )
10 simpl3 ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → 𝐽𝐼 )
11 undif ( 𝐽𝐼 ↔ ( 𝐽 ∪ ( 𝐼𝐽 ) ) = 𝐼 )
12 10 11 sylib ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → ( 𝐽 ∪ ( 𝐼𝐽 ) ) = 𝐼 )
13 12 fneq2d ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → ( 𝑥 Fn ( 𝐽 ∪ ( 𝐼𝐽 ) ) ↔ 𝑥 Fn 𝐼 ) )
14 9 13 mpbird ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → 𝑥 Fn ( 𝐽 ∪ ( 𝐼𝐽 ) ) )
15 simpr ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → 𝑥𝐵 )
16 4 fvexi 0 ∈ V
17 16 a1i ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → 0 ∈ V )
18 disjdif ( 𝐽 ∩ ( 𝐼𝐽 ) ) = ∅
19 18 a1i ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → ( 𝐽 ∩ ( 𝐼𝐽 ) ) = ∅ )
20 fnsuppres ( ( 𝑥 Fn ( 𝐽 ∪ ( 𝐼𝐽 ) ) ∧ ( 𝑥𝐵0 ∈ V ) ∧ ( 𝐽 ∩ ( 𝐼𝐽 ) ) = ∅ ) → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) ) )
21 14 15 17 19 20 syl121anc ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) ∧ 𝑥𝐵 ) → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) ) )
22 21 rabbidva ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → { 𝑥𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 } = { 𝑥𝐵 ∣ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) } )
23 5 22 syl5eq ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐶 = { 𝑥𝐵 ∣ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) } )
24 difssd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → ( 𝐼𝐽 ) ⊆ 𝐼 )
25 eqid { 𝑥𝐵 ∣ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) } = { 𝑥𝐵 ∣ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) }
26 1 2 3 4 25 frlmsslss ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉 ∧ ( 𝐼𝐽 ) ⊆ 𝐼 ) → { 𝑥𝐵 ∣ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) } ∈ 𝑈 )
27 24 26 syld3an3 ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → { 𝑥𝐵 ∣ ( 𝑥 ↾ ( 𝐼𝐽 ) ) = ( ( 𝐼𝐽 ) × { 0 } ) } ∈ 𝑈 )
28 23 27 eqeltrd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑉𝐽𝐼 ) → 𝐶𝑈 )