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 = ( 0_g ‘ 𝑅 )
	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 = ( 0_g ‘ 𝑅 )
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 ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐶 ∈ 𝑈 )

Metamath Proof Explorer

Theorem frlmsslss2

Proof