Metamath Proof Explorer

Theorem fedgmullem2

Description: Lemma for fedgmul . (Contributed by Thierry Arnoux, 20-Jul-2023)

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 fovrnda 
 |-  ( ( 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 syl5bb 
 |-  ( ( 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 211 213 syl 
 |-  ( ph -> B e. Abel )
330 ablgrp 
 |-  ( B e. Abel -> B e. Grp )
331 grpmnd 
 |-  ( B e. Grp -> B e. Mnd )
332 329 330 331 3syl 
 |-  ( ph -> B e. Mnd )
333 207 gsumz 
 |-  ( ( B e. Mnd /\ X e. ( LBasis ` C ) ) -> ( B gsum ( i e. X |-> ( 0g ` B ) ) ) = ( 0g ` B ) )
334 332 13 333 syl2anc 
 |-  ( ph -> ( B gsum ( i e. X |-> ( 0g ` B ) ) ) = ( 0g ` B ) )
335 334 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 ) )
336 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 ) ) )
337 328 335 336 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 ) ) )
338 337 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 ) ) } ) } )
339 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 ) ) )
340 206 255 256 286 338 339 syl32anc 
 |-  ( ph -> ( j e. Y |-> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) ) finSupp ( 0g ` ( Scalar ` B ) ) )
341 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 ) ) ) ) )
342 ovexd 
 |-  ( ( ph /\ j e. Y ) -> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) e. _V )
343 341 342 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 ) ) ) )
344 343 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 ) )
345 344 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 ) ) )
346 345 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 ) ) ) )
347 124 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( .s ` A ) = ( .s ` B ) )
348 50 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( .r ` E ) = ( .s ` A ) )
349 348 oveqd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .r ` E ) i ) = ( ( j W i ) ( .s ` A ) i ) )
350 349 mpteq2dva 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( j W i ) ( .r ` E ) i ) ) = ( i e. X |-> ( ( j W i ) ( .s ` A ) i ) ) )
351 123 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( .r ` E ) = ( .s ` B ) )
352 351 oveqd 
 |-  ( ( ph /\ j e. Y ) -> ( ( j W i ) ( .r ` E ) i ) = ( ( j W i ) ( .s ` B ) i ) )
353 352 mpteq2dv 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( j W i ) ( .r ` E ) i ) ) = ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) )
354 350 353 eqtr3d 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( j W i ) ( .s ` A ) i ) ) = ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) )
355 354 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 ) ) ) )
356 eqidd 
 |-  ( ( ph /\ j e. Y ) -> j = j )
357 347 355 356 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 ) )
358 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 ) )
359 357 358 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 ) )
360 359 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 ) ) )
361 360 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 ) ) ) )
362 1 29 sraring 
 |-  ( ( E e. Ring /\ V C_ ( Base ` E ) ) -> A e. Ring )
363 165 43 362 syl2anc 
 |-  ( ph -> A e. Ring )
364 ringcmn 
 |-  ( A e. Ring -> A e. CMnd )
365 363 364 syl 
 |-  ( ph -> A e. CMnd )
366 165 adantr 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> E e. Ring )
367 eqid 
 |-  ( LBasis ` B ) = ( LBasis ` B )
368 236 367 lbsss 
 |-  ( Y e. ( LBasis ` B ) -> Y C_ ( Base ` B ) )
369 14 368 syl 
 |-  ( ph -> Y C_ ( Base ` B ) )
370 369 243 sseqtrrd 
 |-  ( ph -> Y C_ ( Base ` E ) )
371 370 adantr 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> Y C_ ( Base ` E ) )
372 simprl 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> j e. Y )
373 371 372 sseldd 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> j e. ( Base ` E ) )
374 29 74 ringcl 
 |-  ( ( E e. Ring /\ i e. ( Base ` E ) /\ j e. ( Base ` E ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
375 366 241 373 374 syl3anc 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
376 44 adantr 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( Base ` E ) = ( Base ` A ) )
377 375 376 eleqtrd 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) )
378 377 ralrimivva 
 |-  ( ph -> A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) )
379 11 fmpo 
 |-  ( A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) <-> D : ( Y X. X ) --> ( Base ` A ) )
380 378 379 sylib 
 |-  ( ph -> D : ( Y X. X ) --> ( Base ` A ) )
381 79 80 82 81 24 159 380 150 lcomf 
 |-  ( ph -> ( W oF ( .s ` A ) D ) : ( Y X. X ) --> ( Base ` A ) )
382 79 80 82 81 24 159 380 150 139 140 163 lcomfsupp 
 |-  ( ph -> ( W oF ( .s ` A ) D ) finSupp ( 0g ` A ) )
383 81 139 365 14 13 381 382 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 ) ) ) ) ) )
384 165 3ad2ant1 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> E e. Ring )
385 159 3ad2ant1 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> W : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) )
386 64 62 eqtrd 
 |-  ( ph -> V = ( Base ` ( Scalar ` C ) ) )
387 386 43 eqsstrrd 
 |-  ( ph -> ( Base ` ( Scalar ` C ) ) C_ ( Base ` E ) )
388 68 387 eqsstrd 
 |-  ( ph -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` E ) )
389 388 44 sseqtrd 
 |-  ( ph -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` A ) )
390 389 3ad2ant1 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` A ) )
391 385 390 fssd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> W : ( Y X. X ) --> ( Base ` A ) )
392 simp2 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> j e. Y )
393 simp3 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> i e. X )
394 391 392 393 fovrnd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( j W i ) e. ( Base ` A ) )
395 44 3ad2ant1 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( Base ` E ) = ( Base ` A ) )
396 394 395 eleqtrrd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( j W i ) e. ( Base ` E ) )
397 241 3impb 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> i e. ( Base ` E ) )
398 373 3impb 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> j e. ( Base ` E ) )
399 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 ) ) )
400 384 396 397 398 399 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 ) ) )
401 400 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 ) ) ) )
402 ovexd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( j W i ) e. _V )
403 ovexd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( i ( .r ` E ) j ) e. _V )
404 fnov 
 |-  ( W Fn ( Y X. X ) <-> W = ( j e. Y , i e. X |-> ( j W i ) ) )
405 160 404 sylib 
 |-  ( ph -> W = ( j e. Y , i e. X |-> ( j W i ) ) )
406 11 a1i 
 |-  ( ph -> D = ( j e. Y , i e. X |-> ( i ( .r ` E ) j ) ) )
407 14 13 402 403 405 406 offval22 
 |-  ( ph -> ( W oF ( .r ` E ) D ) = ( j e. Y , i e. X |-> ( ( j W i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) )
408 50 ofeqd 
 |-  ( ph -> oF ( .r ` E ) = oF ( .s ` A ) )
409 408 oveqd 
 |-  ( ph -> ( W oF ( .r ` E ) D ) = ( W oF ( .s ` A ) D ) )
410 401 407 409 3eqtr2rd 
 |-  ( ph -> ( W oF ( .s ` A ) D ) = ( j e. Y , i e. X |-> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) ) )
411 410 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 ) ) )
412 411 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 ) )
413 simplr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> j e. Y )
414 ovexd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) e. _V )
415 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 ) )
416 415 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 ) )
417 413 224 414 416 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 ) )
418 412 417 eqtrd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j ( W oF ( .s ` A ) D ) i ) = ( ( ( j W i ) ( .r ` E ) i ) ( .r ` E ) j ) )
419 418 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 ) ) )
420 419 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 ) ) ) )
421 165 adantr 
 |-  ( ( ph /\ j e. Y ) -> E e. Ring )
422 370 sselda 
 |-  ( ( ph /\ j e. Y ) -> j e. ( Base ` E ) )
423 165 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> E e. Ring )
424 387 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( Base ` ( Scalar ` C ) ) C_ ( Base ` E ) )
425 424 222 sseldd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j W i ) e. ( Base ` E ) )
426 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 ) )
427 423 425 242 426 syl3anc 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( j W i ) ( .r ` E ) i ) e. ( Base ` E ) )
428 315 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( 0g ` E ) = ( 0g ` B ) )
429 248 353 428 3brtr4d 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( j W i ) ( .r ` E ) i ) ) finSupp ( 0g ` E ) )
430 29 170 100 74 421 148 422 427 429 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 ) )
431 420 430 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 ) )
432 148 mptexd 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( j ( W oF ( .s ` A ) D ) i ) ) e. _V )
433 24 adantr 
 |-  ( ( ph /\ j e. Y ) -> A e. LMod )
434 43 adantr 
 |-  ( ( ph /\ j e. Y ) -> V C_ ( Base ` E ) )
435 1 432 197 433 434 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 ) ) ) )
436 148 mptexd 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( j W i ) ( .r ` E ) i ) ) e. _V )
437 1 436 197 433 434 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 ) ) ) )
438 437 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 ) )
439 50 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( .r ` E ) = ( .s ` A ) )
440 350 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 ) ) ) )
441 439 440 356 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 ) )
442 438 441 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 ) )
443 431 435 442 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 ) )
444 443 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 ) ) )
445 444 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 ) ) ) )
446 383 16 445 3eqtr3rd 
 |-  ( ph -> ( A gsum ( j e. Y |-> ( ( A gsum ( i e. X |-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) ) = ( 0g ` A ) )
447 1 6 20 drgext0g 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` A ) )
448 446 447 315 3eqtr2d 
 |-  ( ph -> ( A gsum ( j e. Y |-> ( ( A gsum ( i e. X |-> ( ( j W i ) ( .s ` A ) i ) ) ) ( .s ` A ) j ) ) ) = ( 0g ` B ) )
449 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 ) ) ) )
450 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 ) ) ) )
451 449 450 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 ) ) ) )
452 361 448 451 3eqtr3rd 
 |-  ( ph -> ( B gsum ( j e. Y |-> ( ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) ( .s ` B ) j ) ) ) = ( 0g ` B ) )
453 346 452 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 ) )
454 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 ) ) ) )
455 nfmpt1 
 |-  F/_ j ( j e. Y |-> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) )
456 455 nfeq2 
 |-  F/ j b = ( j e. Y |-> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) )
457 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 ) )
458 457 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 ) )
459 458 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 ) )
460 456 459 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 ) ) )
461 460 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 ) ) ) )
462 461 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 ) ) )
463 454 462 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 ) ) ) )
464 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 ) ) } ) ) )
465 463 464 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 ) ) } ) ) ) )
466 367 lbslinds 
 |-  ( LBasis ` B ) C_ ( LIndS ` B )
467 466 14 sselid 
 |-  ( ph -> Y e. ( LIndS ` B ) )
468 eqid 
 |-  ( Base ` ( Scalar ` B ) ) = ( Base ` ( Scalar ` B ) )
469 236 468 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 ) ) } ) ) ) )
470 469 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 ) ) } ) ) )
471 211 369 467 470 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 ) ) } ) ) )
472 fvexd 
 |-  ( ph -> ( Base ` ( Scalar ` B ) ) e. _V )
473 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 ) ) ) )
474 473 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 ) )
475 472 14 254 474 syl21anc 
 |-  ( ph -> ( j e. Y |-> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) ) e. ( ( Base ` ( Scalar ` B ) ) ^m Y ) )
476 465 471 475 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 ) ) } ) ) )
477 340 453 476 mp2and 
 |-  ( ph -> ( j e. Y |-> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) )
478 fconstmpt 
 |-  ( Y X. { ( 0g ` ( Scalar ` B ) ) } ) = ( j e. Y |-> ( 0g ` ( Scalar ` B ) ) )
479 477 478 eqtrdi 
 |-  ( ph -> ( j e. Y |-> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) ) = ( j e. Y |-> ( 0g ` ( Scalar ` B ) ) ) )
480 ovex 
 |-  ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) e. _V
481 480 rgenw 
 |-  A. j e. Y ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) e. _V
482 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 ) ) ) )
483 481 482 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 ) ) )
484 479 483 sylib 
 |-  ( ph -> A. j e. Y ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( 0g ` ( Scalar ` B ) ) )
485 484 r19.21bi 
 |-  ( ( ph /\ j e. Y ) -> ( B gsum ( i e. X |-> ( ( j W i ) ( .s ` B ) i ) ) ) = ( 0g ` ( Scalar ` B ) ) )
486 315 447 316 3eqtr3rd 
 |-  ( ph -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` A ) )
487 486 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` A ) )
488 205 485 487 3eqtrd 
 |-  ( ( ph /\ j e. Y ) -> ( A gsum ( i e. X |-> ( ( ( i e. X |-> ( j W i ) ) ` i ) ( .s ` A ) i ) ) ) = ( 0g ` A ) )
489 186 488 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 ) ) )
490 189 fmpttd 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( j W i ) ) : X --> ( Base ` ( Scalar ` A ) ) )
491 fvexd 
 |-  ( ( ph /\ j e. Y ) -> ( Base ` ( Scalar ` A ) ) e. _V )
492 491 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 ) ) ) )
493 490 492 mpbird 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( j W i ) ) e. ( ( Base ` ( Scalar ` A ) ) ^m X ) )
494 simpr 
 |-  ( ( ( ph /\ j e. Y ) /\ w = ( i e. X |-> ( j W i ) ) ) -> w = ( i e. X |-> ( j W i ) ) )
495 494 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 ) ) ) )
496 nfv 
 |-  F/ i ( ph /\ j e. Y )
497 nfmpt1 
 |-  F/_ i ( i e. X |-> ( j W i ) )
498 497 nfeq2 
 |-  F/ i w = ( i e. X |-> ( j W i ) )
499 496 498 nfan 
 |-  F/ i ( ( ph /\ j e. Y ) /\ w = ( i e. X |-> ( j W i ) ) )
500 simplr 
 |-  ( ( ( ( ph /\ j e. Y ) /\ w = ( i e. X |-> ( j W i ) ) ) /\ i e. X ) -> w = ( i e. X |-> ( j W i ) ) )
501 500 fveq1d 
 |-  ( ( ( ( ph /\ j e. Y ) /\ w = ( i e. X |-> ( j W i ) ) ) /\ i e. X ) -> ( w ` i ) = ( ( i e. X |-> ( j W i ) ) ` i ) )
502 501 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 ) )
503 499 502 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 ) ) )
504 503 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 ) ) ) )
505 504 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 ) ) )
506 495 505 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 ) ) ) )
507 494 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 ) ) } ) ) )
508 506 507 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 ) ) } ) ) ) )
509 493 508 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 ) ) } ) ) ) )
510 144 489 509 mp2d 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( j W i ) ) = ( X X. { ( 0g ` ( Scalar ` A ) ) } ) )
511 510 257 eqtrdi 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( j W i ) ) = ( i e. X |-> ( 0g ` ( Scalar ` A ) ) ) )
512 511 311 sylib 
 |-  ( ( ph /\ j e. Y ) -> A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) )
513 512 ralrimiva 
 |-  ( ph -> A. j e. Y A. i e. X ( j W i ) = ( 0g ` ( Scalar ` A ) ) )
514 eqidd 
 |-  ( ( j = k /\ i = l ) -> ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` A ) ) )
515 fvexd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( 0g ` ( Scalar ` A ) ) e. _V )
516 fvexd 
 |-  ( ( ph /\ k e. Y /\ l e. X ) -> ( 0g ` ( Scalar ` A ) ) e. _V )
517 160 514 515 516 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 ) ) ) )
518 513 517 mpbird 
 |-  ( ph -> W = ( k e. Y , l e. X |-> ( 0g ` ( Scalar ` A ) ) ) )
519 fconstmpo 
 |-  ( ( Y X. X ) X. { ( 0g ` ( Scalar ` A ) ) } ) = ( k e. Y , l e. X |-> ( 0g ` ( Scalar ` A ) ) )
520 518 519 eqtr4di 
 |-  ( ph -> W = ( ( Y X. X ) X. { ( 0g ` ( Scalar ` A ) ) } ) )