This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ( 𝑅 ∈ 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 ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐶 ∈ 𝑈 )