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

Metamath Proof Explorer

Theorem frlmsslsp

Proof