frlmsslsp

Description: A subset of a free module obtained by restricting the support set is spanned by the relevant unit vectors. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by AV, 24-Jun-2019)

	Ref	Expression
Hypotheses	frlmsslsp.y	$⊢ Y = R freeLMod I$
	frlmsslsp.u	$⊢ U = R unitVec I$
	frlmsslsp.k	$⊢ K = LSpan (Y)$
	frlmsslsp.b	$⊢ B = {Base}_{Y}$
	frlmsslsp.z	$⊢ \underset{˙}{0} = 0_{R}$
	frlmsslsp.c	$⊢ C = \{x \in B \| x supp \underset{˙}{0} \subseteq J\}$
Assertion	frlmsslsp	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to K (U [J]) = C$

Proof

Step	Hyp	Ref	Expression
1		frlmsslsp.y	$⊢ Y = R freeLMod I$
2		frlmsslsp.u	$⊢ U = R unitVec I$
3		frlmsslsp.k	$⊢ K = LSpan (Y)$
4		frlmsslsp.b	$⊢ B = {Base}_{Y}$
5		frlmsslsp.z	$⊢ \underset{˙}{0} = 0_{R}$
6		frlmsslsp.c	$⊢ C = \{x \in B \| x supp \underset{˙}{0} \subseteq J\}$
7	1	frlmlmod	$⊢ (R \in Ring \land I \in V) \to Y \in LMod$
8	7	3adant3	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to Y \in LMod$
9		eqid	$⊢ LSubSp (Y) = LSubSp (Y)$
10	1 9 4 5 6	frlmsslss2	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to C \in LSubSp (Y)$
11	2 1 4	uvcff	$⊢ (R \in Ring \land I \in V) \to U : I ⟶ B$
12	11	3adant3	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to U : I ⟶ B$
13	12	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \to U : I ⟶ B$
14		simp3	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to J \subseteq I$
15	14	sselda	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \to y \in I$
16	13 15	ffvelrnd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \to U (y) \in B$
17		simpl2	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \to I \in V$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19	1 18 4	frlmbasf	$⊢ (I \in V \land U (y) \in B) \to U (y) : I ⟶ {Base}_{R}$
20	17 16 19	syl2anc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \to U (y) : I ⟶ {Base}_{R}$
21		simpll1	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \land x \in (I ∖ J)) \to R \in Ring$
22		simpll2	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \land x \in (I ∖ J)) \to I \in V$
23	15	adantr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \land x \in (I ∖ J)) \to y \in I$
24		eldifi	$⊢ x \in (I ∖ J) \to x \in I$
25	24	adantl	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \land x \in (I ∖ J)) \to x \in I$
26		elneeldif	$⊢ (y \in J \land x \in (I ∖ J)) \to y \neq x$
27	26	adantll	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \land x \in (I ∖ J)) \to y \neq x$
28	2 21 22 23 25 27 5	uvcvv0	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \land x \in (I ∖ J)) \to U (y) (x) = \underset{˙}{0}$
29	20 28	suppss	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \to U (y) supp \underset{˙}{0} \subseteq J$
30		oveq1	$⊢ x = U (y) \to x supp \underset{˙}{0} = U (y) supp \underset{˙}{0}$
31	30	sseq1d	$⊢ x = U (y) \to (x supp \underset{˙}{0} \subseteq J \leftrightarrow U (y) supp \underset{˙}{0} \subseteq J)$
32	31 6	elrab2	$⊢ U (y) \in C \leftrightarrow (U (y) \in B \land U (y) supp \underset{˙}{0} \subseteq J)$
33	16 29 32	sylanbrc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in J) \to U (y) \in C$
34	33	ralrimiva	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to \forall y \in J U (y) \in C$
35	12	ffund	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to Fun U$
36	12	fdmd	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to dom U = I$
37	14 36	sseqtrrd	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to J \subseteq dom U$
38		funimass4	$⊢ (Fun U \land J \subseteq dom U) \to (U [J] \subseteq C \leftrightarrow \forall y \in J U (y) \in C)$
39	35 37 38	syl2anc	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to (U [J] \subseteq C \leftrightarrow \forall y \in J U (y) \in C)$
40	34 39	mpbird	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to U [J] \subseteq C$
41	9 3	lspssp	$⊢ (Y \in LMod \land C \in LSubSp (Y) \land U [J] \subseteq C) \to K (U [J]) \subseteq C$
42	8 10 40 41	syl3anc	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to K (U [J]) \subseteq C$
43		simpl1	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to R \in Ring$
44		simpl2	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to I \in V$
45	6	ssrab3	$⊢ C \subseteq B$
46	45	a1i	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to C \subseteq B$
47	46	sselda	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y \in B$
48		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
49	2 1 4 48	uvcresum	$⊢ (R \in Ring \land I \in V \land y \in B) \to y = \sum_{Y} (y {\cdot_{Y}}_{f} U)$
50	43 44 47 49	syl3anc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y = \sum_{Y} (y {\cdot_{Y}}_{f} U)$
51		eqid	$⊢ 0_{Y} = 0_{Y}$
52		lmodabl	$⊢ Y \in LMod \to Y \in Abel$
53	8 52	syl	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to Y \in Abel$
54	53	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to Y \in Abel$
55		imassrn	$⊢ U [J] \subseteq ran U$
56	12	frnd	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to ran U \subseteq B$
57	55 56	sstrid	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to U [J] \subseteq B$
58	4 9 3	lspcl	$⊢ (Y \in LMod \land U [J] \subseteq B) \to K (U [J]) \in LSubSp (Y)$
59	8 57 58	syl2anc	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to K (U [J]) \in LSubSp (Y)$
60	9	lsssubg	$⊢ (Y \in LMod \land K (U [J]) \in LSubSp (Y)) \to K (U [J]) \in SubGrp (Y)$
61	8 59 60	syl2anc	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to K (U [J]) \in SubGrp (Y)$
62	61	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to K (U [J]) \in SubGrp (Y)$
63	1 18 4	frlmbasf	$⊢ (I \in V \land y \in B) \to y : I ⟶ {Base}_{R}$
64	63	3ad2antl2	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to y : I ⟶ {Base}_{R}$
65	64	ffnd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to y Fn I$
66	12	ffnd	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to U Fn I$
67	66	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to U Fn I$
68		simpl2	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to I \in V$
69		inidm	$⊢ I \cap I = I$
70	65 67 68 68 69	offn	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to (y {\cdot_{Y}}_{f} U) Fn I$
71	47 70	syldan	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to (y {\cdot_{Y}}_{f} U) Fn I$
72	47 65	syldan	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y Fn I$
73	72	adantrr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to y Fn I$
74	66	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to U Fn I$
75		simpl2	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to I \in V$
76		simprr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to z \in I$
77		fnfvof	$⊢ ((y Fn I \land U Fn I) \land (I \in V \land z \in I)) \to (y {\cdot_{Y}}_{f} U) (z) = y (z) \cdot_{Y} U (z)$
78	73 74 75 76 77	syl22anc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to (y {\cdot_{Y}}_{f} U) (z) = y (z) \cdot_{Y} U (z)$
79	8	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to Y \in LMod$
80	59	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to K (U [J]) \in LSubSp (Y)$
81	45	sseli	$⊢ y \in C \to y \in B$
82	81 64	sylan2	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y : I ⟶ {Base}_{R}$
83	82	adantrr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to y : I ⟶ {Base}_{R}$
84	14	sselda	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land z \in J) \to z \in I$
85	84	adantrl	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to z \in I$
86	83 85	ffvelrnd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to y (z) \in {Base}_{R}$
87	1	frlmsca	$⊢ (R \in Ring \land I \in V) \to R = Scalar (Y)$
88	87	3adant3	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to R = Scalar (Y)$
89	88	fveq2d	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to {Base}_{R} = {Base}_{Scalar (Y)}$
90	89	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to {Base}_{R} = {Base}_{Scalar (Y)}$
91	86 90	eleqtrd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to y (z) \in {Base}_{Scalar (Y)}$
92	4 3	lspssid	$⊢ (Y \in LMod \land U [J] \subseteq B) \to U [J] \subseteq K (U [J])$
93	8 57 92	syl2anc	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to U [J] \subseteq K (U [J])$
94	93	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to U [J] \subseteq K (U [J])$
95		funfvima2	$⊢ (Fun U \land J \subseteq dom U) \to (z \in J \to U (z) \in U [J])$
96	35 37 95	syl2anc	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to (z \in J \to U (z) \in U [J])$
97	96	imp	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land z \in J) \to U (z) \in U [J]$
98	97	adantrl	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to U (z) \in U [J]$
99	94 98	sseldd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to U (z) \in K (U [J])$
100		eqid	$⊢ Scalar (Y) = Scalar (Y)$
101		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
102	100 48 101 9	lssvscl	$⊢ ((Y \in LMod \land K (U [J]) \in LSubSp (Y)) \land (y (z) \in {Base}_{Scalar (Y)} \land U (z) \in K (U [J]))) \to y (z) \cdot_{Y} U (z) \in K (U [J])$
103	79 80 91 99 102	syl22anc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in J)) \to y (z) \cdot_{Y} U (z) \in K (U [J])$
104	103	anassrs	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \land z \in J) \to y (z) \cdot_{Y} U (z) \in K (U [J])$
105	104	adantlrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land z \in J) \to y (z) \cdot_{Y} U (z) \in K (U [J])$
106		id	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C)$
107	106	adantrr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C)$
108	107	adantr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C)$
109		simplrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to z \in I$
110		simpr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to \neg z \in J$
111	109 110	eldifd	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to z \in (I ∖ J)$
112		oveq1	$⊢ x = y \to x supp \underset{˙}{0} = y supp \underset{˙}{0}$
113	112	sseq1d	$⊢ x = y \to (x supp \underset{˙}{0} \subseteq J \leftrightarrow y supp \underset{˙}{0} \subseteq J)$
114	113 6	elrab2	$⊢ y \in C \leftrightarrow (y \in B \land y supp \underset{˙}{0} \subseteq J)$
115	114	simprbi	$⊢ y \in C \to y supp \underset{˙}{0} \subseteq J$
116	115	adantl	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y supp \underset{˙}{0} \subseteq J$
117	5	fvexi	$⊢ \underset{˙}{0} \in V$
118	117	a1i	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to \underset{˙}{0} \in V$
119	82 116 44 118	suppssr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \land z \in (I ∖ J)) \to y (z) = \underset{˙}{0}$
120	108 111 119	syl2anc	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to y (z) = \underset{˙}{0}$
121	88	fveq2d	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to 0_{R} = 0_{Scalar (Y)}$
122	5 121	syl5eq	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to \underset{˙}{0} = 0_{Scalar (Y)}$
123	122	ad2antrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to \underset{˙}{0} = 0_{Scalar (Y)}$
124	120 123	eqtrd	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to y (z) = 0_{Scalar (Y)}$
125	124	oveq1d	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to y (z) \cdot_{Y} U (z) = 0_{Scalar (Y)} \cdot_{Y} U (z)$
126	8	ad2antrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to Y \in LMod$
127	12	ffvelrnda	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land z \in I) \to U (z) \in B$
128	127	adantrl	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to U (z) \in B$
129	128	adantr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to U (z) \in B$
130		eqid	$⊢ 0_{Scalar (Y)} = 0_{Scalar (Y)}$
131	4 100 48 130 51	lmod0vs	$⊢ (Y \in LMod \land U (z) \in B) \to 0_{Scalar (Y)} \cdot_{Y} U (z) = 0_{Y}$
132	126 129 131	syl2anc	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to 0_{Scalar (Y)} \cdot_{Y} U (z) = 0_{Y}$
133	125 132	eqtrd	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to y (z) \cdot_{Y} U (z) = 0_{Y}$
134	59	ad2antrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to K (U [J]) \in LSubSp (Y)$
135	51 9	lss0cl	$⊢ (Y \in LMod \land K (U [J]) \in LSubSp (Y)) \to 0_{Y} \in K (U [J])$
136	126 134 135	syl2anc	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to 0_{Y} \in K (U [J])$
137	133 136	eqeltrd	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \land \neg z \in J) \to y (z) \cdot_{Y} U (z) \in K (U [J])$
138	105 137	pm2.61dan	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to y (z) \cdot_{Y} U (z) \in K (U [J])$
139	78 138	eqeltrd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land (y \in C \land z \in I)) \to (y {\cdot_{Y}}_{f} U) (z) \in K (U [J])$
140	139	expr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to (z \in I \to (y {\cdot_{Y}}_{f} U) (z) \in K (U [J]))$
141	140	ralrimiv	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to \forall z \in I (y {\cdot_{Y}}_{f} U) (z) \in K (U [J])$
142		ffnfv	$⊢ (y {\cdot_{Y}}_{f} U) : I ⟶ K (U [J]) \leftrightarrow ((y {\cdot_{Y}}_{f} U) Fn I \land \forall z \in I (y {\cdot_{Y}}_{f} U) (z) \in K (U [J]))$
143	71 141 142	sylanbrc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to (y {\cdot_{Y}}_{f} U) : I ⟶ K (U [J])$
144	1 5 4	frlmbasfsupp	$⊢ (I \in V \land y \in B) \to {finSupp}_{\underset{˙}{0}} (y)$
145	144	fsuppimpd	$⊢ (I \in V \land y \in B) \to y supp \underset{˙}{0} \in Fin$
146	44 47 145	syl2anc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y supp \underset{˙}{0} \in Fin$
147		dffn2	$⊢ (y {\cdot_{Y}}_{f} U) Fn I \leftrightarrow (y {\cdot_{Y}}_{f} U) : I ⟶ V$
148	70 147	sylib	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to (y {\cdot_{Y}}_{f} U) : I ⟶ V$
149	65	adantr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to y Fn I$
150	66	ad2antrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to U Fn I$
151		simpll2	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to I \in V$
152		eldifi	$⊢ x \in (I ∖ {supp}_{\underset{˙}{0}} (y)) \to x \in I$
153	152	adantl	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to x \in I$
154		fnfvof	$⊢ ((y Fn I \land U Fn I) \land (I \in V \land x \in I)) \to (y {\cdot_{Y}}_{f} U) (x) = y (x) \cdot_{Y} U (x)$
155	149 150 151 153 154	syl22anc	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to (y {\cdot_{Y}}_{f} U) (x) = y (x) \cdot_{Y} U (x)$
156		ssidd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to y supp \underset{˙}{0} \subseteq y supp \underset{˙}{0}$
157	117	a1i	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to \underset{˙}{0} \in V$
158	64 156 68 157	suppssr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to y (x) = \underset{˙}{0}$
159	122	ad2antrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to \underset{˙}{0} = 0_{Scalar (Y)}$
160	158 159	eqtrd	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to y (x) = 0_{Scalar (Y)}$
161	160	oveq1d	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to y (x) \cdot_{Y} U (x) = 0_{Scalar (Y)} \cdot_{Y} U (x)$
162	8	ad2antrr	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to Y \in LMod$
163	12	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to U : I ⟶ B$
164		ffvelrn	$⊢ (U : I ⟶ B \land x \in I) \to U (x) \in B$
165	163 152 164	syl2an	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to U (x) \in B$
166	4 100 48 130 51	lmod0vs	$⊢ (Y \in LMod \land U (x) \in B) \to 0_{Scalar (Y)} \cdot_{Y} U (x) = 0_{Y}$
167	162 165 166	syl2anc	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to 0_{Scalar (Y)} \cdot_{Y} U (x) = 0_{Y}$
168	155 161 167	3eqtrd	$⊢ (((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \land x \in (I ∖ {supp}_{\underset{˙}{0}} (y))) \to (y {\cdot_{Y}}_{f} U) (x) = 0_{Y}$
169	148 168	suppss	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in B) \to (y {\cdot_{Y}}_{f} U) supp 0_{Y} \subseteq y supp \underset{˙}{0}$
170	47 169	syldan	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to (y {\cdot_{Y}}_{f} U) supp 0_{Y} \subseteq y supp \underset{˙}{0}$
171	146 170	ssfid	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to (y {\cdot_{Y}}_{f} U) supp 0_{Y} \in Fin$
172		simp2	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to I \in V$
173	1 18 4	frlmbasmap	$⊢ (I \in V \land y \in B) \to y \in ({Base}_{R}^{I})$
174	172 81 173	syl2an	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y \in ({Base}_{R}^{I})$
175		elmapfn	$⊢ y \in ({Base}_{R}^{I}) \to y Fn I$
176	174 175	syl	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y Fn I$
177	12	adantr	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to U : I ⟶ B$
178	177	ffnd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to U Fn I$
179	176 178 44 44	offun	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to Fun (y {\cdot_{Y}}_{f} U)$
180		ovexd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y {\cdot_{Y}}_{f} U \in V$
181		fvexd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to 0_{Y} \in V$
182		funisfsupp	$⊢ (Fun (y {\cdot_{Y}}_{f} U) \land y {\cdot_{Y}}_{f} U \in V \land 0_{Y} \in V) \to ({finSupp}_{0_{Y}} ((y {\cdot_{Y}}_{f} U)) \leftrightarrow (y {\cdot_{Y}}_{f} U) supp 0_{Y} \in Fin)$
183	179 180 181 182	syl3anc	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to ({finSupp}_{0_{Y}} ((y {\cdot_{Y}}_{f} U)) \leftrightarrow (y {\cdot_{Y}}_{f} U) supp 0_{Y} \in Fin)$
184	171 183	mpbird	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to {finSupp}_{0_{Y}} ((y {\cdot_{Y}}_{f} U))$
185	51 54 44 62 143 184	gsumsubgcl	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to \sum_{Y} (y {\cdot_{Y}}_{f} U) \in K (U [J])$
186	50 185	eqeltrd	$⊢ ((R \in Ring \land I \in V \land J \subseteq I) \land y \in C) \to y \in K (U [J])$
187	42 186	eqelssd	$⊢ (R \in Ring \land I \in V \land J \subseteq I) \to K (U [J]) = C$

Metamath Proof Explorer

Theorem frlmsslsp

Proof