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	$⊢ Y = R freeLMod I$
	frlmsslss.u	$⊢ U = LSubSp (Y)$
	frlmsslss.b	$⊢ B = {Base}_{Y}$
	frlmsslss.z	$⊢ \underset{˙}{0} = 0_{R}$
	frlmsslss2.c	$⊢ C = \{x \in B \| x supp \underset{˙}{0} \subseteq J\}$
Assertion	frlmsslss2	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to C \in U$

Proof

Step	Hyp	Ref	Expression
1		frlmsslss.y	$⊢ Y = R freeLMod I$
2		frlmsslss.u	$⊢ U = LSubSp (Y)$
3		frlmsslss.b	$⊢ B = {Base}_{Y}$
4		frlmsslss.z	$⊢ \underset{˙}{0} = 0_{R}$
5		frlmsslss2.c	$⊢ C = \{x \in B \| x supp \underset{˙}{0} \subseteq J\}$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	1 6 3	frlmbasf	$⊢ (I \in V \land x \in B) \to x : I ⟶ {Base}_{R}$
8	7	3ad2antl2	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to x : I ⟶ {Base}_{R}$
9	8	ffnd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to x Fn I$
10		simpl3	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to J \subseteq I$
11		undif	$⊢ J \subseteq I \leftrightarrow J \cup (I ∖ J) = I$
12	10 11	sylib	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to J \cup (I ∖ J) = I$
13	12	fneq2d	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to (x Fn (J \cup (I ∖ J)) \leftrightarrow x Fn I)$
14	9 13	mpbird	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to x Fn (J \cup (I ∖ J))$
15		simpr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to x \in B$
16	4	fvexi	$⊢ \underset{˙}{0} \in V$
17	16	a1i	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to \underset{˙}{0} \in V$
18		disjdif	$⊢ J \cap (I ∖ J) = \emptyset$
19	18	a1i	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to J \cap (I ∖ J) = \emptyset$
20		fnsuppres	$⊢ (x Fn (J \cup (I ∖ J)) \land (x \in B \land \underset{˙}{0} \in V) \land J \cap (I ∖ J) = \emptyset) \to (x supp \underset{˙}{0} \subseteq J \leftrightarrow {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\})$
21	14 15 17 19 20	syl121anc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land x \in B) \to (x supp \underset{˙}{0} \subseteq J \leftrightarrow {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\})$
22	21	rabbidva	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to \{x \in B \| x supp \underset{˙}{0} \subseteq J\} = \{x \in B \| {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\}\}$
23	5 22	syl5eq	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to C = \{x \in B \| {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\}\}$
24		difssd	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to I ∖ J \subseteq I$
25		eqid	$⊢ \{x \in B \| {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\}\} = \{x \in B \| {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\}\}$
26	1 2 3 4 25	frlmsslss	$⊢ (R \in Ring \land I \in V \land I ∖ J \subseteq I) \to \{x \in B \| {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\}\} \in U$
27	24 26	syld3an3	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to \{x \in B \| {x ↾}_{(I ∖ J)} = (I ∖ J) \times \{\underset{˙}{0}\}\} \in U$
28	23 27	eqeltrd	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to C \in U$

Metamath Proof Explorer

Theorem frlmsslss2

Proof