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