fedgmullem2

	Ref	Expression
Hypotheses	fedgmul.a	\|- A = ( ( subringAlg ` E ) ` V )
	fedgmul.b	\|- B = ( ( subringAlg ` E ) ` U )
	fedgmul.c	\|- C = ( ( subringAlg ` F ) ` V )
	fedgmul.f	\|- F = ( E \|`s U )
	fedgmul.k	\|- K = ( E \|`s V )
	fedgmul.1	\|- ( ph -> E e. DivRing )
	fedgmul.2	\|- ( ph -> F e. DivRing )
	fedgmul.3	\|- ( ph -> K e. DivRing )
	fedgmul.4	\|- ( ph -> U e. ( SubRing ` E ) )
	fedgmul.5	\|- ( ph -> V e. ( SubRing ` F ) )
	fedgmullem.d	\|- D = ( j e. Y , i e. X \|-> ( i ( .r ` E ) j ) )
	fedgmullem.h	\|- H = ( j e. Y , i e. X \|-> ( ( G ` j ) ` i ) )
	fedgmullem.x	\|- ( ph -> X e. ( LBasis ` C ) )
	fedgmullem.y	\|- ( ph -> Y e. ( LBasis ` B ) )
	fedgmullem2.1	\|- ( ph -> W e. ( Base ` ( ( Scalar ` A ) freeLMod ( Y X. X ) ) ) )
	fedgmullem2.2	\|- ( ph -> ( A gsum ( W oF ( .s ` A ) D ) ) = ( 0g ` A ) )
Assertion	fedgmullem2	\|- ( ph -> W = ( ( Y X. X ) X. { ( 0g ` ( Scalar ` A ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		fedgmul.a	\|- A = ( ( subringAlg ` E ) ` V )
2		fedgmul.b	\|- B = ( ( subringAlg ` E ) ` U )
3		fedgmul.c	\|- C = ( ( subringAlg ` F ) ` V )
4		fedgmul.f	\|- F = ( E \|`s U )
5		fedgmul.k	\|- K = ( E \|`s V )
6		fedgmul.1	\|- ( ph -> E e. DivRing )
7		fedgmul.2	\|- ( ph -> F e. DivRing )
8		fedgmul.3	\|- ( ph -> K e. DivRing )
9		fedgmul.4	\|- ( ph -> U e. ( SubRing ` E ) )
10		fedgmul.5	\|- ( ph -> V e. ( SubRing ` F ) )
11		fedgmullem.d	\|- D = ( j e. Y , i e. X \|-> ( i ( .r ` E ) j ) )
12		fedgmullem.h	\|- H = ( j e. Y , i e. X \|-> ( ( G ` j ) ` i ) )
13		fedgmullem.x	\|- ( ph -> X e. ( LBasis ` C ) )
14		fedgmullem.y	\|- ( ph -> Y e. ( LBasis ` B ) )
15		fedgmullem2.1	\|- ( ph -> W e. ( Base ` ( ( Scalar ` A ) freeLMod ( Y X. X ) ) ) )
16		fedgmullem2.2	\|- ( ph -> ( A gsum ( W oF ( .s ` A ) D ) ) = ( 0g ` A ) )
17	4	subsubrg	\|- ( U e. ( SubRing ` E ) -> ( V e. ( SubRing ` F ) <-> ( V e. ( SubRing ` E ) /\ V C_ U ) ) )
18	17	biimpa	\|- ( ( U e. ( SubRing ` E ) /\ V e. ( SubRing ` F ) ) -> ( V e. ( SubRing ` E ) /\ V C_ U ) )
19	9 10 18	syl2anc	\|- ( ph -> ( V e. ( SubRing ` E ) /\ V C_ U ) )
20	19	simpld	\|- ( ph -> V e. ( SubRing ` E ) )
21	1 5	sralvec	\|- ( ( E e. DivRing /\ K e. DivRing /\ V e. ( SubRing ` E ) ) -> A e. LVec )
22	6 8 20 21	syl3anc	\|- ( ph -> A e. LVec )
23		lveclmod	\|- ( A e. LVec -> A e. LMod )
24	22 23	syl	\|- ( ph -> A e. LMod )
25		eqid	\|- ( Base ` C ) = ( Base ` C )
26		eqid	\|- ( LBasis ` C ) = ( LBasis ` C )
27	25 26	lbsss	\|- ( X e. ( LBasis ` C ) -> X C_ ( Base ` C ) )
28	13 27	syl	\|- ( ph -> X C_ ( Base ` C ) )
29		eqid	\|- ( Base ` E ) = ( Base ` E )
30	29	subrgss	\|- ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
31	9 30	syl	\|- ( ph -> U C_ ( Base ` E ) )
32	4 29	ressbas2	\|- ( U C_ ( Base ` E ) -> U = ( Base ` F ) )
33	31 32	syl	\|- ( ph -> U = ( Base ` F ) )
34	3	a1i	\|- ( ph -> C = ( ( subringAlg ` F ) ` V ) )
35		eqid	\|- ( Base ` F ) = ( Base ` F )
36	35	subrgss	\|- ( V e. ( SubRing ` F ) -> V C_ ( Base ` F ) )
37	10 36	syl	\|- ( ph -> V C_ ( Base ` F ) )
38	34 37	srabase	\|- ( ph -> ( Base ` F ) = ( Base ` C ) )
39	33 38	eqtrd	\|- ( ph -> U = ( Base ` C ) )
40	39 31	eqsstrrd	\|- ( ph -> ( Base ` C ) C_ ( Base ` E ) )
41	1	a1i	\|- ( ph -> A = ( ( subringAlg ` E ) ` V ) )
42	29	subrgss	\|- ( V e. ( SubRing ` E ) -> V C_ ( Base ` E ) )
43	20 42	syl	\|- ( ph -> V C_ ( Base ` E ) )
44	41 43	srabase	\|- ( ph -> ( Base ` E ) = ( Base ` A ) )
45	40 44	sseqtrd	\|- ( ph -> ( Base ` C ) C_ ( Base ` A ) )
46	28 45	sstrd	\|- ( ph -> X C_ ( Base ` A ) )
47	41 9 43	srasubrg	\|- ( ph -> U e. ( SubRing ` A ) )
48		subrgsubg	\|- ( U e. ( SubRing ` A ) -> U e. ( SubGrp ` A ) )
49	47 48	syl	\|- ( ph -> U e. ( SubGrp ` A ) )
50	1 6 20	drgextvsca	\|- ( ph -> ( .r ` E ) = ( .s ` A ) )
51	50	oveqdr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> ( x ( .r ` E ) y ) = ( x ( .s ` A ) y ) )
52	9	adantr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> U e. ( SubRing ` E ) )
53	19	simprd	\|- ( ph -> V C_ U )
54	53	adantr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> V C_ U )
55		simprl	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> x e. ( Base ` ( Scalar ` A ) ) )
56		ressabs	\|- ( ( U e. ( SubRing ` E ) /\ V C_ U ) -> ( ( E \|`s U ) \|`s V ) = ( E \|`s V ) )
57	9 53 56	syl2anc	\|- ( ph -> ( ( E \|`s U ) \|`s V ) = ( E \|`s V ) )
58	4	oveq1i	\|- ( F \|`s V ) = ( ( E \|`s U ) \|`s V )
59	57 58 5	3eqtr4g	\|- ( ph -> ( F \|`s V ) = K )
60	34 37	srasca	\|- ( ph -> ( F \|`s V ) = ( Scalar ` C ) )
61	59 60	eqtr3d	\|- ( ph -> K = ( Scalar ` C ) )
62	61	fveq2d	\|- ( ph -> ( Base ` K ) = ( Base ` ( Scalar ` C ) ) )
63	5 29	ressbas2	\|- ( V C_ ( Base ` E ) -> V = ( Base ` K ) )
64	43 63	syl	\|- ( ph -> V = ( Base ` K ) )
65	41 43	srasca	\|- ( ph -> ( E \|`s V ) = ( Scalar ` A ) )
66	5 65	eqtrid	\|- ( ph -> K = ( Scalar ` A ) )
67	59 60 66	3eqtr3rd	\|- ( ph -> ( Scalar ` A ) = ( Scalar ` C ) )
68	67	fveq2d	\|- ( ph -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` C ) ) )
69	62 64 68	3eqtr4d	\|- ( ph -> V = ( Base ` ( Scalar ` A ) ) )
70	69	adantr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> V = ( Base ` ( Scalar ` A ) ) )
71	55 70	eleqtrrd	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> x e. V )
72	54 71	sseldd	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> x e. U )
73		simprr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> y e. U )
74		eqid	\|- ( .r ` E ) = ( .r ` E )
75	74	subrgmcl	\|- ( ( U e. ( SubRing ` E ) /\ x e. U /\ y e. U ) -> ( x ( .r ` E ) y ) e. U )
76	52 72 73 75	syl3anc	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> ( x ( .r ` E ) y ) e. U )
77	51 76	eqeltrrd	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` A ) ) /\ y e. U ) ) -> ( x ( .s ` A ) y ) e. U )
78	77	ralrimivva	\|- ( ph -> A. x e. ( Base ` ( Scalar ` A ) ) A. y e. U ( x ( .s ` A ) y ) e. U )
79		eqid	\|- ( Scalar ` A ) = ( Scalar ` A )
80		eqid	\|- ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
81		eqid	\|- ( Base ` A ) = ( Base ` A )
82		eqid	\|- ( .s ` A ) = ( .s ` A )
83		eqid	\|- ( LSubSp ` A ) = ( LSubSp ` A )
84	79 80 81 82 83	islss4	\|- ( A e. LMod -> ( U e. ( LSubSp ` A ) <-> ( U e. ( SubGrp ` A ) /\ A. x e. ( Base ` ( Scalar ` A ) ) A. y e. U ( x ( .s ` A ) y ) e. U ) ) )
85	84	biimpar	\|- ( ( A e. LMod /\ ( U e. ( SubGrp ` A ) /\ A. x e. ( Base ` ( Scalar ` A ) ) A. y e. U ( x ( .s ` A ) y ) e. U ) ) -> U e. ( LSubSp ` A ) )
86	24 49 78 85	syl12anc	\|- ( ph -> U e. ( LSubSp ` A ) )
87	28 39	sseqtrrd	\|- ( ph -> X C_ U )
88	26	lbslinds	\|- ( LBasis ` C ) C_ ( LIndS ` C )
89	88 13	sselid	\|- ( ph -> X e. ( LIndS ` C ) )
90	31 44	sseqtrd	\|- ( ph -> U C_ ( Base ` A ) )
91		eqid	\|- ( A \|`s U ) = ( A \|`s U )
92	91 81	ressbas2	\|- ( U C_ ( Base ` A ) -> U = ( Base ` ( A \|`s U ) ) )
93	90 92	syl	\|- ( ph -> U = ( Base ` ( A \|`s U ) ) )
94	33 93 38	3eqtr3rd	\|- ( ph -> ( Base ` C ) = ( Base ` ( A \|`s U ) ) )
95	91 79	resssca	\|- ( U e. ( SubRing ` E ) -> ( Scalar ` A ) = ( Scalar ` ( A \|`s U ) ) )
96	9 95	syl	\|- ( ph -> ( Scalar ` A ) = ( Scalar ` ( A \|`s U ) ) )
97	67 96	eqtr3d	\|- ( ph -> ( Scalar ` C ) = ( Scalar ` ( A \|`s U ) ) )
98	97	fveq2d	\|- ( ph -> ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` ( A \|`s U ) ) ) )
99	97	fveq2d	\|- ( ph -> ( 0g ` ( Scalar ` C ) ) = ( 0g ` ( Scalar ` ( A \|`s U ) ) ) )
100		eqid	\|- ( +g ` E ) = ( +g ` E )
101	4 100	ressplusg	\|- ( U e. ( SubRing ` E ) -> ( +g ` E ) = ( +g ` F ) )
102	9 101	syl	\|- ( ph -> ( +g ` E ) = ( +g ` F ) )
103	41 43	sraaddg	\|- ( ph -> ( +g ` E ) = ( +g ` A ) )
104	34 37	sraaddg	\|- ( ph -> ( +g ` F ) = ( +g ` C ) )
105	102 103 104	3eqtr3rd	\|- ( ph -> ( +g ` C ) = ( +g ` A ) )
106		eqid	\|- ( +g ` A ) = ( +g ` A )
107	91 106	ressplusg	\|- ( U e. ( SubRing ` E ) -> ( +g ` A ) = ( +g ` ( A \|`s U ) ) )
108	9 107	syl	\|- ( ph -> ( +g ` A ) = ( +g ` ( A \|`s U ) ) )
109	105 108	eqtrd	\|- ( ph -> ( +g ` C ) = ( +g ` ( A \|`s U ) ) )
110	109	oveqdr	\|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( +g ` C ) y ) = ( x ( +g ` ( A \|`s U ) ) y ) )
111	59 8	eqeltrd	\|- ( ph -> ( F \|`s V ) e. DivRing )
112		eqid	\|- ( F \|`s V ) = ( F \|`s V )
113	3 112	sralvec	\|- ( ( F e. DivRing /\ ( F \|`s V ) e. DivRing /\ V e. ( SubRing ` F ) ) -> C e. LVec )
114	7 111 10 113	syl3anc	\|- ( ph -> C e. LVec )
115		lveclmod	\|- ( C e. LVec -> C e. LMod )
116	114 115	syl	\|- ( ph -> C e. LMod )
117		eqid	\|- ( Scalar ` C ) = ( Scalar ` C )
118		eqid	\|- ( .s ` C ) = ( .s ` C )
119		eqid	\|- ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
120	25 117 118 119	lmodvscl	\|- ( ( C e. LMod /\ x e. ( Base ` ( Scalar ` C ) ) /\ y e. ( Base ` C ) ) -> ( x ( .s ` C ) y ) e. ( Base ` C ) )
121	120	3expb	\|- ( ( C e. LMod /\ ( x e. ( Base ` ( Scalar ` C ) ) /\ y e. ( Base ` C ) ) ) -> ( x ( .s ` C ) y ) e. ( Base ` C ) )
122	116 121	sylan	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` C ) ) /\ y e. ( Base ` C ) ) ) -> ( x ( .s ` C ) y ) e. ( Base ` C ) )
123	2 6 9	drgextvsca	\|- ( ph -> ( .r ` E ) = ( .s ` B ) )
124	50 123	eqtr3d	\|- ( ph -> ( .s ` A ) = ( .s ` B ) )
125	91 82	ressvsca	\|- ( U e. ( SubRing ` E ) -> ( .s ` A ) = ( .s ` ( A \|`s U ) ) )
126	9 125	syl	\|- ( ph -> ( .s ` A ) = ( .s ` ( A \|`s U ) ) )
127	4 74	ressmulr	\|- ( U e. ( SubRing ` E ) -> ( .r ` E ) = ( .r ` F ) )
128	9 127	syl	\|- ( ph -> ( .r ` E ) = ( .r ` F ) )
129	3 7 10	drgextvsca	\|- ( ph -> ( .r ` F ) = ( .s ` C ) )
130	128 123 129	3eqtr3d	\|- ( ph -> ( .s ` B ) = ( .s ` C ) )
131	124 126 130	3eqtr3rd	\|- ( ph -> ( .s ` C ) = ( .s ` ( A \|`s U ) ) )
132	131	oveqdr	\|- ( ( ph /\ ( x e. ( Base ` ( Scalar ` C ) ) /\ y e. ( Base ` C ) ) ) -> ( x ( .s ` C ) y ) = ( x ( .s ` ( A \|`s U ) ) y ) )
133		ovexd	\|- ( ph -> ( A \|`s U ) e. _V )
134	94 98 99 110 122 132 114 133	lindspropd	\|- ( ph -> ( LIndS ` C ) = ( LIndS ` ( A \|`s U ) ) )
135	89 134	eleqtrd	\|- ( ph -> X e. ( LIndS ` ( A \|`s U ) ) )
136	83 91	lsslinds	\|- ( ( A e. LMod /\ U e. ( LSubSp ` A ) /\ X C_ U ) -> ( X e. ( LIndS ` ( A \|`s U ) ) <-> X e. ( LIndS ` A ) ) )
137	136	biimpa	\|- ( ( ( A e. LMod /\ U e. ( LSubSp ` A ) /\ X C_ U ) /\ X e. ( LIndS ` ( A \|`s U ) ) ) -> X e. ( LIndS ` A ) )
138	24 86 87 135 137	syl31anc	\|- ( ph -> X e. ( LIndS ` A ) )
139		eqid	\|- ( 0g ` A ) = ( 0g ` A )
140		eqid	\|- ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` A ) )
141	81 80 79 82 139 140	islinds5	\|- ( ( A e. LMod /\ X C_ ( Base ` A ) ) -> ( X e. ( LIndS ` A ) <-> A. w e. ( ( Base ` ( Scalar ` A ) ) ^m X ) ( ( w finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> w = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) ) )
142	141	biimpa	\|- ( ( ( A e. LMod /\ X C_ ( Base ` A ) ) /\ X e. ( LIndS ` A ) ) -> A. w e. ( ( Base ` ( Scalar ` A ) ) ^m X ) ( ( w finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> w = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
143	24 46 138 142	syl21anc	\|- ( ph -> A. w e. ( ( Base ` ( Scalar ` A ) ) ^m X ) ( ( w finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> w = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
144	143	adantr	\|- ( ( ph /\ j e. Y ) -> A. w e. ( ( Base ` ( Scalar ` A ) ) ^m X ) ( ( w finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> w = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
145		eqid	\|- ( i e. X \|-> ( j W i ) ) = ( i e. X \|-> ( j W i ) )
146		fvexd	\|- ( ( ph /\ j e. Y ) -> ( 0g ` F ) e. _V )
147	14	adantr	\|- ( ( ph /\ j e. Y ) -> Y e. ( LBasis ` B ) )
148	13	adantr	\|- ( ( ph /\ j e. Y ) -> X e. ( LBasis ` C ) )
149		fvexd	\|- ( ph -> ( Scalar ` A ) e. _V )
150	14 13	xpexd	\|- ( ph -> ( Y X. X ) e. _V )
151		eqid	\|- ( ( Scalar ` A ) freeLMod ( Y X. X ) ) = ( ( Scalar ` A ) freeLMod ( Y X. X ) )
152		eqid	\|- ( Base ` ( ( Scalar ` A ) freeLMod ( Y X. X ) ) ) = ( Base ` ( ( Scalar ` A ) freeLMod ( Y X. X ) ) )
153	151 80 140 152	frlmelbas	\|- ( ( ( Scalar ` A ) e. _V /\ ( Y X. X ) e. _V ) -> ( W e. ( Base ` ( ( Scalar ` A ) freeLMod ( Y X. X ) ) ) <-> ( W e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) /\ W finSupp ( 0g ` ( Scalar ` A ) ) ) ) )
154	149 150 153	syl2anc	\|- ( ph -> ( W e. ( Base ` ( ( Scalar ` A ) freeLMod ( Y X. X ) ) ) <-> ( W e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) /\ W finSupp ( 0g ` ( Scalar ` A ) ) ) ) )
155	15 154	mpbid	\|- ( ph -> ( W e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) /\ W finSupp ( 0g ` ( Scalar ` A ) ) ) )
156	155	simpld	\|- ( ph -> W e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) )
157		fvexd	\|- ( ph -> ( Base ` ( Scalar ` A ) ) e. _V )
158	157 150	elmapd	\|- ( ph -> ( W e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) <-> W : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) ) )
159	156 158	mpbid	\|- ( ph -> W : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) )
160	159	ffnd	\|- ( ph -> W Fn ( Y X. X ) )
161	160	adantr	\|- ( ( ph /\ j e. Y ) -> W Fn ( Y X. X ) )
162		simpr	\|- ( ( ph /\ j e. Y ) -> j e. Y )
163	155	simprd	\|- ( ph -> W finSupp ( 0g ` ( Scalar ` A ) ) )
164		drngring	\|- ( E e. DivRing -> E e. Ring )
165	6 164	syl	\|- ( ph -> E e. Ring )
166		ringmnd	\|- ( E e. Ring -> E e. Mnd )
167	165 166	syl	\|- ( ph -> E e. Mnd )
168		subrgsubg	\|- ( V e. ( SubRing ` E ) -> V e. ( SubGrp ` E ) )
169	20 168	syl	\|- ( ph -> V e. ( SubGrp ` E ) )
170		eqid	\|- ( 0g ` E ) = ( 0g ` E )
171	170	subg0cl	\|- ( V e. ( SubGrp ` E ) -> ( 0g ` E ) e. V )
172	169 171	syl	\|- ( ph -> ( 0g ` E ) e. V )
173	53 172	sseldd	\|- ( ph -> ( 0g ` E ) e. U )
174	4 29 170	ress0g	\|- ( ( E e. Mnd /\ ( 0g ` E ) e. U /\ U C_ ( Base ` E ) ) -> ( 0g ` E ) = ( 0g ` F ) )
175	167 173 31 174	syl3anc	\|- ( ph -> ( 0g ` E ) = ( 0g ` F ) )
176	61	fveq2d	\|- ( ph -> ( 0g ` K ) = ( 0g ` ( Scalar ` C ) ) )
177	5 170	subrg0	\|- ( V e. ( SubRing ` E ) -> ( 0g ` E ) = ( 0g ` K ) )
178	20 177	syl	\|- ( ph -> ( 0g ` E ) = ( 0g ` K ) )
179	67	fveq2d	\|- ( ph -> ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` C ) ) )
180	176 178 179	3eqtr4d	\|- ( ph -> ( 0g ` E ) = ( 0g ` ( Scalar ` A ) ) )
181	175 180	eqtr3d	\|- ( ph -> ( 0g ` F ) = ( 0g ` ( Scalar ` A ) ) )
182	163 181	breqtrrd	\|- ( ph -> W finSupp ( 0g ` F ) )
183	182	adantr	\|- ( ( ph /\ j e. Y ) -> W finSupp ( 0g ` F ) )
184	145 146 147 148 161 162 183	fsuppcurry1	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j W i ) ) finSupp ( 0g ` F ) )
185	181	adantr	\|- ( ( ph /\ j e. Y ) -> ( 0g ` F ) = ( 0g ` ( Scalar ` A ) ) )
186	184 185	breqtrd	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j W i ) ) finSupp ( 0g ` ( Scalar ` A ) ) )
187		eqidd	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j W i ) ) = ( i e. X \|-> ( j W i ) ) )
188	159	fovcdmda	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( j W i ) e. ( Base ` ( Scalar ` A ) ) )
189	188	anassrs	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j W i ) e. ( Base ` ( Scalar ` A ) ) )
190	187 189	fvmpt2d	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( i e. X \|-> ( j W i ) ) ` i ) = ( j W i ) )
191	190	oveq1d	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) = ( ( j W i ) ( .s ` A ) i ) )
192	124	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( .s ` A ) = ( .s ` B ) )
193	192	oveqd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .s ` A ) i ) = ( ( j W i ) ( .s ` B ) i ) )
194	191 193	eqtrd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) = ( ( j W i ) ( .s ` B ) i ) )
195	194	mpteq2dva	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) = ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) )
196	195	oveq2d	\|- ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
197	6	adantr	\|- ( ( ph /\ j e. Y ) -> E e. DivRing )
198	20	adantr	\|- ( ( ph /\ j e. Y ) -> V e. ( SubRing ` E ) )
199	8	adantr	\|- ( ( ph /\ j e. Y ) -> K e. DivRing )
200	1 197 198 5 199 148	drgextgsum	\|- ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
201	9	adantr	\|- ( ( ph /\ j e. Y ) -> U e. ( SubRing ` E ) )
202	7	adantr	\|- ( ( ph /\ j e. Y ) -> F e. DivRing )
203	2 197 201 4 202 148	drgextgsum	\|- ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
204	200 203	eqtr3d	\|- ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
205	196 204	eqtrd	\|- ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
206	14	mptexd	\|- ( ph -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) e. _V )
207		eqid	\|- ( 0g ` B ) = ( 0g ` B )
208	2 4	sralvec	\|- ( ( E e. DivRing /\ F e. DivRing /\ U e. ( SubRing ` E ) ) -> B e. LVec )
209	6 7 9 208	syl3anc	\|- ( ph -> B e. LVec )
210		lveclmod	\|- ( B e. LVec -> B e. LMod )
211	209 210	syl	\|- ( ph -> B e. LMod )
212	211	adantr	\|- ( ( ph /\ j e. Y ) -> B e. LMod )
213		lmodabl	\|- ( B e. LMod -> B e. Abel )
214	212 213	syl	\|- ( ( ph /\ j e. Y ) -> B e. Abel )
215	2	a1i	\|- ( ph -> B = ( ( subringAlg ` E ) ` U ) )
216	215 9 31	srasubrg	\|- ( ph -> U e. ( SubRing ` B ) )
217		subrgsubg	\|- ( U e. ( SubRing ` B ) -> U e. ( SubGrp ` B ) )
218	216 217	syl	\|- ( ph -> U e. ( SubGrp ` B ) )
219	218	adantr	\|- ( ( ph /\ j e. Y ) -> U e. ( SubGrp ` B ) )
220	116	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> C e. LMod )
221	68	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` C ) ) )
222	189 221	eleqtrd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j W i ) e. ( Base ` ( Scalar ` C ) ) )
223	28	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> X C_ ( Base ` C ) )
224		simpr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> i e. X )
225	223 224	sseldd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> i e. ( Base ` C ) )
226	25 117 118 119	lmodvscl	\|- ( ( C e. LMod /\ ( j W i ) e. ( Base ` ( Scalar ` C ) ) /\ i e. ( Base ` C ) ) -> ( ( j W i ) ( .s ` C ) i ) e. ( Base ` C ) )
227	220 222 225 226	syl3anc	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .s ` C ) i ) e. ( Base ` C ) )
228	130	oveqd	\|- ( ph -> ( ( j W i ) ( .s ` B ) i ) = ( ( j W i ) ( .s ` C ) i ) )
229	228	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .s ` B ) i ) = ( ( j W i ) ( .s ` C ) i ) )
230	39	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> U = ( Base ` C ) )
231	227 229 230	3eltr4d	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .s ` B ) i ) e. U )
232	231	fmpttd	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) : X --> U )
233	215 31	srasca	\|- ( ph -> ( E \|`s U ) = ( Scalar ` B ) )
234	4 233	eqtrid	\|- ( ph -> F = ( Scalar ` B ) )
235	234	adantr	\|- ( ( ph /\ j e. Y ) -> F = ( Scalar ` B ) )
236		eqid	\|- ( Base ` B ) = ( Base ` B )
237		ovexd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j W i ) e. _V )
238	28 40	sstrd	\|- ( ph -> X C_ ( Base ` E ) )
239	238	adantr	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> X C_ ( Base ` E ) )
240		simprr	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> i e. X )
241	239 240	sseldd	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> i e. ( Base ` E ) )
242	241	anassrs	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> i e. ( Base ` E ) )
243	215 31	srabase	\|- ( ph -> ( Base ` E ) = ( Base ` B ) )
244	243	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( Base ` E ) = ( Base ` B ) )
245	242 244	eleqtrd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> i e. ( Base ` B ) )
246		eqid	\|- ( 0g ` F ) = ( 0g ` F )
247		eqid	\|- ( .s ` B ) = ( .s ` B )
248	148 212 235 236 237 245 207 246 247 184	mptscmfsupp0	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) finSupp ( 0g ` B ) )
249	207 214 148 219 232 248	gsumsubgcl	\|- ( ( ph /\ j e. Y ) -> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) e. U )
250	234	fveq2d	\|- ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` B ) ) )
251	33 250	eqtrd	\|- ( ph -> U = ( Base ` ( Scalar ` B ) ) )
252	251	adantr	\|- ( ( ph /\ j e. Y ) -> U = ( Base ` ( Scalar ` B ) ) )
253	249 252	eleqtrd	\|- ( ( ph /\ j e. Y ) -> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) e. ( Base ` ( Scalar ` B ) ) )
254	253	fmpttd	\|- ( ph -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) : Y --> ( Base ` ( Scalar ` B ) ) )
255	254	ffund	\|- ( ph -> Fun ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) )
256		fvexd	\|- ( ph -> ( 0g ` ( Scalar ` B ) ) e. _V )
257		fconstmpt	\|- ( X X. { ( 0g ` ( Scalar ` A ) ) } ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) )
258	257	eqeq2i	\|- ( ( i e. X \|-> ( k W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) <-> ( i e. X \|-> ( k W i ) ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) ) )
259		ovex	\|- ( k W i ) e. _V
260	259	rgenw	\|- A. i e. X ( k W i ) e. _V
261		mpteqb	\|- ( A. i e. X ( k W i ) e. _V -> ( ( i e. X \|-> ( k W i ) ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) ) <-> A. i e. X ( k W i ) = ( 0g ` ( Scalar ` A ) ) ) )
262	260 261	ax-mp	\|- ( ( i e. X \|-> ( k W i ) ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) ) <-> A. i e. X ( k W i ) = ( 0g ` ( Scalar ` A ) ) )
263	258 262	bitri	\|- ( ( i e. X \|-> ( k W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) <-> A. i e. X ( k W i ) = ( 0g ` ( Scalar ` A ) ) )
264	263	necon3abii	\|- ( ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) <-> -. A. i e. X ( k W i ) = ( 0g ` ( Scalar ` A ) ) )
265		df-ov	\|- ( k W i ) = ( W ` <. k , i >. )
266	265	eqcomi	\|- ( W ` <. k , i >. ) = ( k W i )
267	266	a1i	\|- ( ( ( ph /\ k e. Y ) /\ i e. X ) -> ( W ` <. k , i >. ) = ( k W i ) )
268	267	eqeq1d	\|- ( ( ( ph /\ k e. Y ) /\ i e. X ) -> ( ( W ` <. k , i >. ) = ( 0g ` ( Scalar ` A ) ) <-> ( k W i ) = ( 0g ` ( Scalar ` A ) ) ) )
269	268	necon3abid	\|- ( ( ( ph /\ k e. Y ) /\ i e. X ) -> ( ( W ` <. k , i >. ) =/= ( 0g ` ( Scalar ` A ) ) <-> -. ( k W i ) = ( 0g ` ( Scalar ` A ) ) ) )
270	269	rexbidva	\|- ( ( ph /\ k e. Y ) -> ( E. i e. X ( W ` <. k , i >. ) =/= ( 0g ` ( Scalar ` A ) ) <-> E. i e. X -. ( k W i ) = ( 0g ` ( Scalar ` A ) ) ) )
271		rexnal	\|- ( E. i e. X -. ( k W i ) = ( 0g ` ( Scalar ` A ) ) <-> -. A. i e. X ( k W i ) = ( 0g ` ( Scalar ` A ) ) )
272	270 271	bitr2di	\|- ( ( ph /\ k e. Y ) -> ( -. A. i e. X ( k W i ) = ( 0g ` ( Scalar ` A ) ) <-> E. i e. X ( W ` <. k , i >. ) =/= ( 0g ` ( Scalar ` A ) ) ) )
273	264 272	bitrid	\|- ( ( ph /\ k e. Y ) -> ( ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) <-> E. i e. X ( W ` <. k , i >. ) =/= ( 0g ` ( Scalar ` A ) ) ) )
274	273	rabbidva	\|- ( ph -> { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } = { k e. Y \| E. i e. X ( W ` <. k , i >. ) =/= ( 0g ` ( Scalar ` A ) ) } )
275		fveq2	\|- ( z = <. k , i >. -> ( W ` z ) = ( W ` <. k , i >. ) )
276	275	neeq1d	\|- ( z = <. k , i >. -> ( ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) <-> ( W ` <. k , i >. ) =/= ( 0g ` ( Scalar ` A ) ) ) )
277	276	dmrab	\|- dom { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } = { k e. Y \| E. i e. X ( W ` <. k , i >. ) =/= ( 0g ` ( Scalar ` A ) ) }
278	274 277	eqtr4di	\|- ( ph -> { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } = dom { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } )
279		fvexd	\|- ( ph -> ( 0g ` ( Scalar ` A ) ) e. _V )
280		suppvalfn	\|- ( ( W Fn ( Y X. X ) /\ ( Y X. X ) e. _V /\ ( 0g ` ( Scalar ` A ) ) e. _V ) -> ( W supp ( 0g ` ( Scalar ` A ) ) ) = { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } )
281	160 150 279 280	syl3anc	\|- ( ph -> ( W supp ( 0g ` ( Scalar ` A ) ) ) = { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } )
282	163	fsuppimpd	\|- ( ph -> ( W supp ( 0g ` ( Scalar ` A ) ) ) e. Fin )
283	281 282	eqeltrrd	\|- ( ph -> { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } e. Fin )
284		dmfi	\|- ( { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } e. Fin -> dom { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } e. Fin )
285	283 284	syl	\|- ( ph -> dom { z e. ( Y X. X ) \| ( W ` z ) =/= ( 0g ` ( Scalar ` A ) ) } e. Fin )
286	278 285	eqeltrd	\|- ( ph -> { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } e. Fin )
287		nfv	\|- F/ i ph
288		nfcv	\|- F/_ i Y
289		nfmpt1	\|- F/_ i ( i e. X \|-> ( k W i ) )
290		nfcv	\|- F/_ i ( X X. { ( 0g ` ( Scalar ` A ) ) } )
291	289 290	nfne	\|- F/ i ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } )
292	291 288	nfrabw	\|- F/_ i { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) }
293	288 292	nfdif	\|- F/_ i ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } )
294	293	nfcri	\|- F/ i j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } )
295	287 294	nfan	\|- F/ i ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) )
296		simpr	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) )
297	296	eldifad	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> j e. Y )
298	296	eldifbd	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> -. j e. { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } )
299		oveq1	\|- ( k = j -> ( k W i ) = ( j W i ) )
300	299	mpteq2dv	\|- ( k = j -> ( i e. X \|-> ( k W i ) ) = ( i e. X \|-> ( j W i ) ) )
301	300	neeq1d	\|- ( k = j -> ( ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) <-> ( i e. X \|-> ( j W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
302	301	elrab	\|- ( j e. { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } <-> ( j e. Y /\ ( i e. X \|-> ( j W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
303	298 302	sylnib	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> -. ( j e. Y /\ ( i e. X \|-> ( j W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
304	297 303	mpnanrd	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> -. ( i e. X \|-> ( j W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) )
305		nne	\|- ( -. ( i e. X \|-> ( j W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) <-> ( i e. X \|-> ( j W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) )
306	304 305	sylib	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( i e. X \|-> ( j W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) )
307	306 257	eqtrdi	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( i e. X \|-> ( j W i ) ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) ) )
308		ovex	\|- ( j W i ) e. _V
309	308	rgenw	\|- A. i e. X ( j W i ) e. _V
310		mpteqb	\|- ( A. i e. X ( j W i ) e. _V -> ( ( i e. X \|-> ( j W i ) ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) ) <-> A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) ) )
311	309 310	ax-mp	\|- ( ( i e. X \|-> ( j W i ) ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) ) <-> A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) )
312	307 311	sylib	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) )
313	312	r19.21bi	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> ( j W i ) = ( 0g ` ( Scalar ` A ) ) )
314	313	oveq1d	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> ( ( j W i ) ( .s ` B ) i ) = ( ( 0g ` ( Scalar ` A ) ) ( .s ` B ) i ) )
315	2 6 9	drgext0g	\|- ( ph -> ( 0g ` E ) = ( 0g ` B ) )
316	2 6 9	drgext0gsca	\|- ( ph -> ( 0g ` B ) = ( 0g ` ( Scalar ` B ) ) )
317	315 180 316	3eqtr3d	\|- ( ph -> ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` B ) ) )
318	317	ad2antrr	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` B ) ) )
319	318	oveq1d	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> ( ( 0g ` ( Scalar ` A ) ) ( .s ` B ) i ) = ( ( 0g ` ( Scalar ` B ) ) ( .s ` B ) i ) )
320	211	ad2antrr	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> B e. LMod )
321	297 245	syldanl	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> i e. ( Base ` B ) )
322		eqid	\|- ( Scalar ` B ) = ( Scalar ` B )
323		eqid	\|- ( 0g ` ( Scalar ` B ) ) = ( 0g ` ( Scalar ` B ) )
324	236 322 247 323 207	lmod0vs	\|- ( ( B e. LMod /\ i e. ( Base ` B ) ) -> ( ( 0g ` ( Scalar ` B ) ) ( .s ` B ) i ) = ( 0g ` B ) )
325	320 321 324	syl2anc	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> ( ( 0g ` ( Scalar ` B ) ) ( .s ` B ) i ) = ( 0g ` B ) )
326	314 319 325	3eqtrd	\|- ( ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) /\ i e. X ) -> ( ( j W i ) ( .s ` B ) i ) = ( 0g ` B ) )
327	295 326	mpteq2da	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) = ( i e. X \|-> ( 0g ` B ) ) )
328	327	oveq2d	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( B gsum ( i e. X \|-> ( 0g ` B ) ) ) )
329		ablgrp	\|- ( B e. Abel -> B e. Grp )
330		grpmnd	\|- ( B e. Grp -> B e. Mnd )
331	211 213 329 330	4syl	\|- ( ph -> B e. Mnd )
332	207	gsumz	\|- ( ( B e. Mnd /\ X e. ( LBasis ` C ) ) -> ( B gsum ( i e. X \|-> ( 0g ` B ) ) ) = ( 0g ` B ) )
333	331 13 332	syl2anc	\|- ( ph -> ( B gsum ( i e. X \|-> ( 0g ` B ) ) ) = ( 0g ` B ) )
334	333	adantr	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( B gsum ( i e. X \|-> ( 0g ` B ) ) ) = ( 0g ` B ) )
335	316	adantr	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( 0g ` B ) = ( 0g ` ( Scalar ` B ) ) )
336	328 334 335	3eqtrd	\|- ( ( ph /\ j e. ( Y \ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( 0g ` ( Scalar ` B ) ) )
337	336 14	suppss2	\|- ( ph -> ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) supp ( 0g ` ( Scalar ` B ) ) ) C_ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } )
338		suppssfifsupp	\|- ( ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) e. _V /\ Fun ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) /\ ( 0g ` ( Scalar ` B ) ) e. _V ) /\ ( { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } e. Fin /\ ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) supp ( 0g ` ( Scalar ` B ) ) ) C_ { k e. Y \| ( i e. X \|-> ( k W i ) ) =/= ( X X. { ( 0g ` ( Scalar ` A ) ) } ) } ) ) -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) finSupp ( 0g ` ( Scalar ` B ) ) )
339	206 255 256 286 337 338	syl32anc	\|- ( ph -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) finSupp ( 0g ` ( Scalar ` B ) ) )
340		eqidd	\|- ( ph -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) )
341		ovexd	\|- ( ( ph /\ j e. Y ) -> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) e. _V )
342	340 341	fvmpt2d	\|- ( ( ph /\ j e. Y ) -> ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) = ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
343	342	oveq1d	\|- ( ( ph /\ j e. Y ) -> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) = ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) )
344	343	mpteq2dva	\|- ( ph -> ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) = ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) )
345	344	oveq2d	\|- ( ph -> ( B gsum ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) ) = ( B gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) )
346	124	adantr	\|- ( ( ph /\ j e. Y ) -> ( .s ` A ) = ( .s ` B ) )
347	50	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( .r ` E ) = ( .s ` A ) )
348	347	oveqd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .r ` E ) i ) = ( ( j W i ) ( .s ` A ) i ) )
349	348	mpteq2dva	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) = ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) )
350	123	adantr	\|- ( ( ph /\ j e. Y ) -> ( .r ` E ) = ( .s ` B ) )
351	350	oveqd	\|- ( ( ph /\ j e. Y ) -> ( ( j W i ) ( .r ` E ) i ) = ( ( j W i ) ( .s ` B ) i ) )
352	351	mpteq2dv	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) = ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) )
353	349 352	eqtr3d	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) = ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) )
354	353	oveq2d	\|- ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) = ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
355		eqidd	\|- ( ( ph /\ j e. Y ) -> j = j )
356	346 354 355	oveq123d	\|- ( ( ph /\ j e. Y ) -> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) = ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) )
357	204	oveq1d	\|- ( ( ph /\ j e. Y ) -> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) = ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) )
358	356 357	eqtrd	\|- ( ( ph /\ j e. Y ) -> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) = ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) )
359	358	mpteq2dva	\|- ( ph -> ( j e. Y \|-> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) = ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) )
360	359	oveq2d	\|- ( ph -> ( A gsum ( j e. Y \|-> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) ) = ( A gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) )
361	1 29	sraring	\|- ( ( E e. Ring /\ V C_ ( Base ` E ) ) -> A e. Ring )
362	165 43 361	syl2anc	\|- ( ph -> A e. Ring )
363		ringcmn	\|- ( A e. Ring -> A e. CMnd )
364	362 363	syl	\|- ( ph -> A e. CMnd )
365	165	adantr	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> E e. Ring )
366		eqid	\|- ( LBasis ` B ) = ( LBasis ` B )
367	236 366	lbsss	\|- ( Y e. ( LBasis ` B ) -> Y C_ ( Base ` B ) )
368	14 367	syl	\|- ( ph -> Y C_ ( Base ` B ) )
369	368 243	sseqtrrd	\|- ( ph -> Y C_ ( Base ` E ) )
370	369	adantr	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> Y C_ ( Base ` E ) )
371		simprl	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> j e. Y )
372	370 371	sseldd	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> j e. ( Base ` E ) )
373	29 74	ringcl	\|- ( ( E e. Ring /\ i e. ( Base ` E ) /\ j e. ( Base ` E ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
374	365 241 372 373	syl3anc	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
375	44	adantr	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( Base ` E ) = ( Base ` A ) )
376	374 375	eleqtrd	\|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) )
377	376	ralrimivva	\|- ( ph -> A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) )
378	11	fmpo	\|- ( A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) <-> D : ( Y X. X ) --> ( Base ` A ) )
379	377 378	sylib	\|- ( ph -> D : ( Y X. X ) --> ( Base ` A ) )
380	79 80 82 81 24 159 379 150	lcomf	\|- ( ph -> ( W oF ( .s ` A ) D ) : ( Y X. X ) --> ( Base ` A ) )
381	79 80 82 81 24 159 379 150 139 140 163	lcomfsupp	\|- ( ph -> ( W oF ( .s ` A ) D ) finSupp ( 0g ` A ) )
382	81 139 364 14 13 380 381	gsumxp	\|- ( ph -> ( A gsum ( W oF ( .s ` A ) D ) ) = ( A gsum ( j e. Y \|-> ( A gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) ) ) )
383	165	3ad2ant1	\|- ( ( ph /\ j e. Y /\ i e. X ) -> E e. Ring )
384	159	3ad2ant1	\|- ( ( ph /\ j e. Y /\ i e. X ) -> W : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) )
385	64 62	eqtrd	\|- ( ph -> V = ( Base ` ( Scalar ` C ) ) )
386	385 43	eqsstrrd	\|- ( ph -> ( Base ` ( Scalar ` C ) ) C_ ( Base ` E ) )
387	68 386	eqsstrd	\|- ( ph -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` E ) )
388	387 44	sseqtrd	\|- ( ph -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` A ) )
389	388	3ad2ant1	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` A ) )
390	384 389	fssd	\|- ( ( ph /\ j e. Y /\ i e. X ) -> W : ( Y X. X ) --> ( Base ` A ) )
391		simp2	\|- ( ( ph /\ j e. Y /\ i e. X ) -> j e. Y )
392		simp3	\|- ( ( ph /\ j e. Y /\ i e. X ) -> i e. X )
393	390 391 392	fovcdmd	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( j W i ) e. ( Base ` A ) )
394	44	3ad2ant1	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( Base ` E ) = ( Base ` A ) )
395	393 394	eleqtrrd	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( j W i ) e. ( Base ` E ) )
396	241	3impb	\|- ( ( ph /\ j e. Y /\ i e. X ) -> i e. ( Base ` E ) )
397	372	3impb	\|- ( ( ph /\ j e. Y /\ i e. X ) -> j e. ( Base ` E ) )
398	29 74	ringass	\|- ( ( E e. Ring /\ ( ( j W i ) e. ( Base ` E ) /\ i e. ( Base ` E ) /\ j e. ( Base ` E ) ) ) -> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) = ( ( j W i ) ( .r ` E ) ( i ( .r ` E ) j ) ) )
399	383 395 396 397 398	syl13anc	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) = ( ( j W i ) ( .r ` E ) ( i ( .r ` E ) j ) ) )
400	399	mpoeq3dva	\|- ( ph -> ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) = ( j e. Y , i e. X \|-> ( ( j W i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) )
401		ovexd	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( j W i ) e. _V )
402		ovexd	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( i ( .r ` E ) j ) e. _V )
403		fnov	\|- ( W Fn ( Y X. X ) <-> W = ( j e. Y , i e. X \|-> ( j W i ) ) )
404	160 403	sylib	\|- ( ph -> W = ( j e. Y , i e. X \|-> ( j W i ) ) )
405	11	a1i	\|- ( ph -> D = ( j e. Y , i e. X \|-> ( i ( .r ` E ) j ) ) )
406	14 13 401 402 404 405	offval22	\|- ( ph -> ( W oF ( .r ` E ) D ) = ( j e. Y , i e. X \|-> ( ( j W i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) )
407	50	ofeqd	\|- ( ph -> oF ( .r ` E ) = oF ( .s ` A ) )
408	407	oveqd	\|- ( ph -> ( W oF ( .r ` E ) D ) = ( W oF ( .s ` A ) D ) )
409	400 406 408	3eqtr2rd	\|- ( ph -> ( W oF ( .s ` A ) D ) = ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) )
410	409	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( W oF ( .s ` A ) D ) = ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) )
411	410	oveqd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j ( W oF ( .s ` A ) D ) i ) = ( j ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) i ) )
412		simplr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> j e. Y )
413		ovexd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) e. _V )
414		eqid	\|- ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) = ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) )
415	414	ovmpt4g	\|- ( ( j e. Y /\ i e. X /\ ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) e. _V ) -> ( j ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) i ) = ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) )
416	412 224 413 415	syl3anc	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j ( j e. Y , i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) i ) = ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) )
417	411 416	eqtrd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j ( W oF ( .s ` A ) D ) i ) = ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) )
418	417	mpteq2dva	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) = ( i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) )
419	418	oveq2d	\|- ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) = ( E gsum ( i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) ) )
420	165	adantr	\|- ( ( ph /\ j e. Y ) -> E e. Ring )
421	369	sselda	\|- ( ( ph /\ j e. Y ) -> j e. ( Base ` E ) )
422	165	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> E e. Ring )
423	386	ad2antrr	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( Base ` ( Scalar ` C ) ) C_ ( Base ` E ) )
424	423 222	sseldd	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j W i ) e. ( Base ` E ) )
425	29 74	ringcl	\|- ( ( E e. Ring /\ ( j W i ) e. ( Base ` E ) /\ i e. ( Base ` E ) ) -> ( ( j W i ) ( .r ` E ) i ) e. ( Base ` E ) )
426	422 424 242 425	syl3anc	\|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .r ` E ) i ) e. ( Base ` E ) )
427	315	adantr	\|- ( ( ph /\ j e. Y ) -> ( 0g ` E ) = ( 0g ` B ) )
428	248 352 427	3brtr4d	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) finSupp ( 0g ` E ) )
429	29 170 74 420 148 421 426 428	gsummulc1	\|- ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X \|-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) ) = ( ( E gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) )
430	419 429	eqtrd	\|- ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) = ( ( E gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) )
431	148	mptexd	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) e. _V )
432	24	adantr	\|- ( ( ph /\ j e. Y ) -> A e. LMod )
433	43	adantr	\|- ( ( ph /\ j e. Y ) -> V C_ ( Base ` E ) )
434	1 431 197 432 433	gsumsra	\|- ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) = ( A gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) )
435	148	mptexd	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) e. _V )
436	1 435 197 432 433	gsumsra	\|- ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) = ( A gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) )
437	436	oveq1d	\|- ( ( ph /\ j e. Y ) -> ( ( E gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) = ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) )
438	50	adantr	\|- ( ( ph /\ j e. Y ) -> ( .r ` E ) = ( .s ` A ) )
439	349	oveq2d	\|- ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) = ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) )
440	438 439 355	oveq123d	\|- ( ( ph /\ j e. Y ) -> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) = ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) )
441	437 440	eqtrd	\|- ( ( ph /\ j e. Y ) -> ( ( E gsum ( i e. X \|-> ( ( j W i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) = ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) )
442	430 434 441	3eqtr3d	\|- ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) = ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) )
443	442	mpteq2dva	\|- ( ph -> ( j e. Y \|-> ( A gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) ) = ( j e. Y \|-> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) )
444	443	oveq2d	\|- ( ph -> ( A gsum ( j e. Y \|-> ( A gsum ( i e. X \|-> ( j ( W oF ( .s ` A ) D ) i ) ) ) ) ) = ( A gsum ( j e. Y \|-> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) ) )
445	382 16 444	3eqtr3rd	\|- ( ph -> ( A gsum ( j e. Y \|-> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) ) = ( 0g ` A ) )
446	1 6 20	drgext0g	\|- ( ph -> ( 0g ` E ) = ( 0g ` A ) )
447	445 446 315	3eqtr2d	\|- ( ph -> ( A gsum ( j e. Y \|-> ( ( A gsum ( i e. X \|-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) ) = ( 0g ` B ) )
448	1 6 20 5 8 14	drgextgsum	\|- ( ph -> ( E gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) = ( A gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) )
449	2 6 9 4 7 14	drgextgsum	\|- ( ph -> ( E gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) = ( B gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) )
450	448 449	eqtr3d	\|- ( ph -> ( A gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) = ( B gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) )
451	360 447 450	3eqtr3rd	\|- ( ph -> ( B gsum ( j e. Y \|-> ( ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) = ( 0g ` B ) )
452	345 451	eqtrd	\|- ( ph -> ( B gsum ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) )
453		breq1	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( b finSupp ( 0g ` ( Scalar ` B ) ) <-> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) finSupp ( 0g ` ( Scalar ` B ) ) ) )
454		nfmpt1	\|- F/_ j ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
455	454	nfeq2	\|- F/ j b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) )
456		fveq1	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( b ` j ) = ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) )
457	456	oveq1d	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( ( b ` j ) ( .s ` B ) j ) = ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) )
458	457	adantr	\|- ( ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) /\ j e. Y ) -> ( ( b ` j ) ( .s ` B ) j ) = ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) )
459	455 458	mpteq2da	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) = ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) )
460	459	oveq2d	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( B gsum ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) ) = ( B gsum ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) ) )
461	460	eqeq1d	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( ( B gsum ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) <-> ( B gsum ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) )
462	453 461	anbi12d	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( ( b finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) <-> ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) ) )
463		eqeq1	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( b = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) <-> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) ) )
464	462 463	imbi12d	\|- ( b = ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) -> ( ( ( b finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) -> b = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) ) <-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) ) ) )
465	366	lbslinds	\|- ( LBasis ` B ) C_ ( LIndS ` B )
466	465 14	sselid	\|- ( ph -> Y e. ( LIndS ` B ) )
467		eqid	\|- ( Base ` ( Scalar ` B ) ) = ( Base ` ( Scalar ` B ) )
468	236 467 322 247 207 323	islinds5	\|- ( ( B e. LMod /\ Y C_ ( Base ` B ) ) -> ( Y e. ( LIndS ` B ) <-> A. b e. ( ( Base ` ( Scalar ` B ) ) ^m Y ) ( ( b finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) -> b = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) ) ) )
469	468	biimpa	\|- ( ( ( B e. LMod /\ Y C_ ( Base ` B ) ) /\ Y e. ( LIndS ` B ) ) -> A. b e. ( ( Base ` ( Scalar ` B ) ) ^m Y ) ( ( b finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) -> b = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) ) )
470	211 368 466 469	syl21anc	\|- ( ph -> A. b e. ( ( Base ` ( Scalar ` B ) ) ^m Y ) ( ( b finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( b ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) -> b = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) ) )
471		fvexd	\|- ( ph -> ( Base ` ( Scalar ` B ) ) e. _V )
472		elmapg	\|- ( ( ( Base ` ( Scalar ` B ) ) e. _V /\ Y e. ( LBasis ` B ) ) -> ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) e. ( ( Base ` ( Scalar ` B ) ) ^m Y ) <-> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) : Y --> ( Base ` ( Scalar ` B ) ) ) )
473	472	biimpar	\|- ( ( ( ( Base ` ( Scalar ` B ) ) e. _V /\ Y e. ( LBasis ` B ) ) /\ ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) : Y --> ( Base ` ( Scalar ` B ) ) ) -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) e. ( ( Base ` ( Scalar ` B ) ) ^m Y ) )
474	471 14 254 473	syl21anc	\|- ( ph -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) e. ( ( Base ` ( Scalar ` B ) ) ^m Y ) )
475	464 470 474	rspcdva	\|- ( ph -> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) finSupp ( 0g ` ( Scalar ` B ) ) /\ ( B gsum ( j e. Y \|-> ( ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) ` j ) ( .s ` B ) j ) ) ) = ( 0g ` B ) ) -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) ) )
476	339 452 475	mp2and	\|- ( ph -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) )
477		fconstmpt	\|- ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) = ( j e. Y \|-> ( 0g ` ( Scalar ` B ) ) )
478	476 477	eqtrdi	\|- ( ph -> ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( j e. Y \|-> ( 0g ` ( Scalar ` B ) ) ) )
479		ovex	\|- ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) e. _V
480	479	rgenw	\|- A. j e. Y ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) e. _V
481		mpteqb	\|- ( A. j e. Y ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) e. _V -> ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( j e. Y \|-> ( 0g ` ( Scalar ` B ) ) ) <-> A. j e. Y ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( 0g ` ( Scalar ` B ) ) ) )
482	480 481	ax-mp	\|- ( ( j e. Y \|-> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( j e. Y \|-> ( 0g ` ( Scalar ` B ) ) ) <-> A. j e. Y ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( 0g ` ( Scalar ` B ) ) )
483	478 482	sylib	\|- ( ph -> A. j e. Y ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( 0g ` ( Scalar ` B ) ) )
484	483	r19.21bi	\|- ( ( ph /\ j e. Y ) -> ( B gsum ( i e. X \|-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( 0g ` ( Scalar ` B ) ) )
485	315 446 316	3eqtr3rd	\|- ( ph -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` A ) )
486	485	adantr	\|- ( ( ph /\ j e. Y ) -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` A ) )
487	205 484 486	3eqtrd	\|- ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) )
488	186 487	jca	\|- ( ( ph /\ j e. Y ) -> ( ( i e. X \|-> ( j W i ) ) finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) )
489	189	fmpttd	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j W i ) ) : X --> ( Base ` ( Scalar ` A ) ) )
490		fvexd	\|- ( ( ph /\ j e. Y ) -> ( Base ` ( Scalar ` A ) ) e. _V )
491	490 148	elmapd	\|- ( ( ph /\ j e. Y ) -> ( ( i e. X \|-> ( j W i ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m X ) <-> ( i e. X \|-> ( j W i ) ) : X --> ( Base ` ( Scalar ` A ) ) ) )
492	489 491	mpbird	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j W i ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m X ) )
493		simpr	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> w = ( i e. X \|-> ( j W i ) ) )
494	493	breq1d	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> ( w finSupp ( 0g ` ( Scalar ` A ) ) <-> ( i e. X \|-> ( j W i ) ) finSupp ( 0g ` ( Scalar ` A ) ) ) )
495		nfv	\|- F/ i ( ph /\ j e. Y )
496		nfmpt1	\|- F/_ i ( i e. X \|-> ( j W i ) )
497	496	nfeq2	\|- F/ i w = ( i e. X \|-> ( j W i ) )
498	495 497	nfan	\|- F/ i ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) )
499		simplr	\|- ( ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) /\ i e. X ) -> w = ( i e. X \|-> ( j W i ) ) )
500	499	fveq1d	\|- ( ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) /\ i e. X ) -> ( w ` i ) = ( ( i e. X \|-> ( j W i ) ) ` i ) )
501	500	oveq1d	\|- ( ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) /\ i e. X ) -> ( ( w ` i ) ( .s ` A ) i ) = ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) )
502	498 501	mpteq2da	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) = ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) )
503	502	oveq2d	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) )
504	503	eqeq1d	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> ( ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) <-> ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) )
505	494 504	anbi12d	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> ( ( w finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) <-> ( ( i e. X \|-> ( j W i ) ) finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) ) )
506	493	eqeq1d	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> ( w = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) <-> ( i e. X \|-> ( j W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) )
507	505 506	imbi12d	\|- ( ( ( ph /\ j e. Y ) /\ w = ( i e. X \|-> ( j W i ) ) ) -> ( ( ( w finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> w = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) <-> ( ( ( i e. X \|-> ( j W i ) ) finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> ( i e. X \|-> ( j W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) ) )
508	492 507	rspcdv	\|- ( ( ph /\ j e. Y ) -> ( A. w e. ( ( Base ` ( Scalar ` A ) ) ^m X ) ( ( w finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( w ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> w = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) -> ( ( ( i e. X \|-> ( j W i ) ) finSupp ( 0g ` ( Scalar ` A ) ) /\ ( A gsum ( i e. X \|-> ( ( ( i e. X \|-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) ) -> ( i e. X \|-> ( j W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) ) ) )
509	144 488 508	mp2d	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) )
510	509 257	eqtrdi	\|- ( ( ph /\ j e. Y ) -> ( i e. X \|-> ( j W i ) ) = ( i e. X \|-> ( 0g ` ( Scalar ` A ) ) ) )
511	510 311	sylib	\|- ( ( ph /\ j e. Y ) -> A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) )
512	511	ralrimiva	\|- ( ph -> A. j e. Y A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) )
513		eqidd	\|- ( ( j = k /\ i = l ) -> ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` A ) ) )
514		fvexd	\|- ( ( ph /\ j e. Y /\ i e. X ) -> ( 0g ` ( Scalar ` A ) ) e. _V )
515		fvexd	\|- ( ( ph /\ k e. Y /\ l e. X ) -> ( 0g ` ( Scalar ` A ) ) e. _V )
516	160 513 514 515	fnmpoovd	\|- ( ph -> ( W = ( k e. Y , l e. X \|-> ( 0g ` ( Scalar ` A ) ) ) <-> A. j e. Y A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) ) )
517	512 516	mpbird	\|- ( ph -> W = ( k e. Y , l e. X \|-> ( 0g ` ( Scalar ` A ) ) ) )
518		fconstmpo	\|- ( ( Y X. X ) X. { ( 0g ` ( Scalar ` A ) ) } ) = ( k e. Y , l e. X \|-> ( 0g ` ( Scalar ` A ) ) )
519	517 518	eqtr4di	\|- ( ph -> W = ( ( Y X. X ) X. { ( 0g ` ( Scalar ` A ) ) } ) )

Metamath Proof Explorer

Theorem fedgmullem2

Proof