Metamath Proof Explorer

Theorem fedgmullem1

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 ) )
fedgmullem1.a 
|- ( ph -> Z e. ( Base ` A ) )
fedgmullem1.l 
|- ( ph -> L : Y --> ( Base ` ( Scalar ` B ) ) )
fedgmullem1.1 
|- ( ph -> L finSupp ( 0g ` ( Scalar ` B ) ) )
fedgmullem1.z 
|- ( ph -> Z = ( B gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) )
fedgmullem1.g 
|- ( ph -> G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) )
fedgmullem1.2 
|- ( ( ph /\ j e. Y ) -> ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) )
fedgmullem1.3 
|- ( ( ph /\ j e. Y ) -> ( L ` j ) = ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
Assertion fedgmullem1 
|- ( ph -> ( H finSupp ( 0g ` ( Scalar ` A ) ) /\ Z = ( A gsum ( H oF ( .s ` A ) D ) ) ) )

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 fedgmullem1.a 
 |-  ( ph -> Z e. ( Base ` A ) )
16 fedgmullem1.l 
 |-  ( ph -> L : Y --> ( Base ` ( Scalar ` B ) ) )
17 fedgmullem1.1 
 |-  ( ph -> L finSupp ( 0g ` ( Scalar ` B ) ) )
18 fedgmullem1.z 
 |-  ( ph -> Z = ( B gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) )
19 fedgmullem1.g 
 |-  ( ph -> G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) )
20 fedgmullem1.2 
 |-  ( ( ph /\ j e. Y ) -> ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) )
21 fedgmullem1.3 
 |-  ( ( ph /\ j e. Y ) -> ( L ` j ) = ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
22 simpllr 
 |-  ( ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ j e. Y ) /\ i e. X ) -> G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) )
23 simplr 
 |-  ( ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ j e. Y ) /\ i e. X ) -> j e. Y )
24 22 23 ffvelrnd 
 |-  ( ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ j e. Y ) /\ i e. X ) -> ( G ` j ) e. ( ( Base ` ( Scalar ` C ) ) ^m X ) )
25 elmapi 
 |-  ( ( G ` j ) e. ( ( Base ` ( Scalar ` C ) ) ^m X ) -> ( G ` j ) : X --> ( Base ` ( Scalar ` C ) ) )
26 24 25 syl 
 |-  ( ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ j e. Y ) /\ i e. X ) -> ( G ` j ) : X --> ( Base ` ( Scalar ` C ) ) )
27 26 anasss 
 |-  ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ ( j e. Y /\ i e. X ) ) -> ( G ` j ) : X --> ( Base ` ( Scalar ` C ) ) )
28 simprr 
 |-  ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ ( j e. Y /\ i e. X ) ) -> i e. X )
29 27 28 ffvelrnd 
 |-  ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ ( j e. Y /\ i e. X ) ) -> ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` C ) ) )
30 1 a1i 
 |-  ( ph -> A = ( ( subringAlg ` E ) ` V ) )
31 4 subsubrg 
 |-  ( U e. ( SubRing ` E ) -> ( V e. ( SubRing ` F ) <-> ( V e. ( SubRing ` E ) /\ V C_ U ) ) )
32 31 biimpa 
 |-  ( ( U e. ( SubRing ` E ) /\ V e. ( SubRing ` F ) ) -> ( V e. ( SubRing ` E ) /\ V C_ U ) )
33 9 10 32 syl2anc 
 |-  ( ph -> ( V e. ( SubRing ` E ) /\ V C_ U ) )
34 33 simpld 
 |-  ( ph -> V e. ( SubRing ` E ) )
35 eqid 
 |-  ( Base ` E ) = ( Base ` E )
36 35 subrgss 
 |-  ( V e. ( SubRing ` E ) -> V C_ ( Base ` E ) )
37 34 36 syl 
 |-  ( ph -> V C_ ( Base ` E ) )
38 30 37 srasca 
 |-  ( ph -> ( E |`s V ) = ( Scalar ` A ) )
39 5 38 syl5eq 
 |-  ( ph -> K = ( Scalar ` A ) )
40 33 simprd 
 |-  ( ph -> V C_ U )
41 ressabs 
 |-  ( ( U e. ( SubRing ` E ) /\ V C_ U ) -> ( ( E |`s U ) |`s V ) = ( E |`s V ) )
42 9 40 41 syl2anc 
 |-  ( ph -> ( ( E |`s U ) |`s V ) = ( E |`s V ) )
43 4 oveq1i 
 |-  ( F |`s V ) = ( ( E |`s U ) |`s V )
44 42 43 5 3eqtr4g 
 |-  ( ph -> ( F |`s V ) = K )
45 3 a1i 
 |-  ( ph -> C = ( ( subringAlg ` F ) ` V ) )
46 eqid 
 |-  ( Base ` F ) = ( Base ` F )
47 46 subrgss 
 |-  ( V e. ( SubRing ` F ) -> V C_ ( Base ` F ) )
48 10 47 syl 
 |-  ( ph -> V C_ ( Base ` F ) )
49 45 48 srasca 
 |-  ( ph -> ( F |`s V ) = ( Scalar ` C ) )
50 44 49 eqtr3d 
 |-  ( ph -> K = ( Scalar ` C ) )
51 39 50 eqtr3d 
 |-  ( ph -> ( Scalar ` A ) = ( Scalar ` C ) )
52 51 fveq2d 
 |-  ( ph -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` C ) ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ ( j e. Y /\ i e. X ) ) -> ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` C ) ) )
54 29 53 eleqtrrd 
 |-  ( ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) /\ ( j e. Y /\ i e. X ) ) -> ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) )
55 54 ralrimivva 
 |-  ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) -> A. j e. Y A. i e. X ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) )
56 12 fmpo 
 |-  ( A. j e. Y A. i e. X ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) <-> H : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) )
57 55 56 sylib 
 |-  ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) -> H : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) )
58 fvexd 
 |-  ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) -> ( Base ` ( Scalar ` A ) ) e. _V )
59 14 13 xpexd 
 |-  ( ph -> ( Y X. X ) e. _V )
60 59 adantr 
 |-  ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) -> ( Y X. X ) e. _V )
61 58 60 elmapd 
 |-  ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) -> ( H e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) <-> H : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) ) )
62 57 61 mpbird 
 |-  ( ( ph /\ G : Y --> ( ( Base ` ( Scalar ` C ) ) ^m X ) ) -> H e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) )
63 19 62 mpdan 
 |-  ( ph -> H e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) )
64 simpl 
 |-  ( ( ph /\ j e. Y ) -> ph )
65 64 adantr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ph )
66 19 ffvelrnda 
 |-  ( ( ph /\ j e. Y ) -> ( G ` j ) e. ( ( Base ` ( Scalar ` C ) ) ^m X ) )
67 66 25 syl 
 |-  ( ( ph /\ j e. Y ) -> ( G ` j ) : X --> ( Base ` ( Scalar ` C ) ) )
68 67 adantr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( G ` j ) : X --> ( Base ` ( Scalar ` C ) ) )
69 52 feq3d 
 |-  ( ph -> ( ( G ` j ) : X --> ( Base ` ( Scalar ` A ) ) <-> ( G ` j ) : X --> ( Base ` ( Scalar ` C ) ) ) )
70 69 biimpar 
 |-  ( ( ph /\ ( G ` j ) : X --> ( Base ` ( Scalar ` C ) ) ) -> ( G ` j ) : X --> ( Base ` ( Scalar ` A ) ) )
71 65 68 70 syl2anc 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( G ` j ) : X --> ( Base ` ( Scalar ` A ) ) )
72 simpr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> i e. X )
73 71 72 ffvelrnd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) )
74 73 ralrimiva 
 |-  ( ( ph /\ j e. Y ) -> A. i e. X ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) )
75 74 ralrimiva 
 |-  ( ph -> A. j e. Y A. i e. X ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` A ) ) )
76 75 56 sylib 
 |-  ( ph -> H : ( Y X. X ) --> ( Base ` ( Scalar ` A ) ) )
77 76 ffund 
 |-  ( ph -> Fun H )
78 drngring 
 |-  ( E e. DivRing -> E e. Ring )
79 6 78 syl 
 |-  ( ph -> E e. Ring )
80 ringgrp 
 |-  ( E e. Ring -> E e. Grp )
81 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
82 35 81 grpidcl 
 |-  ( E e. Grp -> ( 0g ` E ) e. ( Base ` E ) )
83 79 80 82 3syl 
 |-  ( ph -> ( 0g ` E ) e. ( Base ` E ) )
84 17 fsuppimpd 
 |-  ( ph -> ( L supp ( 0g ` ( Scalar ` B ) ) ) e. Fin )
85 simpl 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> ph )
86 simpr 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) )
87 86 eldifad 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> j e. Y )
88 ssidd 
 |-  ( ph -> ( L supp ( 0g ` ( Scalar ` B ) ) ) C_ ( L supp ( 0g ` ( Scalar ` B ) ) ) )
89 fvexd 
 |-  ( ph -> ( 0g ` ( Scalar ` B ) ) e. _V )
90 16 88 14 89 suppssr 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> ( L ` j ) = ( 0g ` ( Scalar ` B ) ) )
91 87 21 syldan 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> ( L ` j ) = ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
92 2 a1i 
 |-  ( ph -> B = ( ( subringAlg ` E ) ` U ) )
93 35 subrgss 
 |-  ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) )
94 9 93 syl 
 |-  ( ph -> U C_ ( Base ` E ) )
95 92 94 srasca 
 |-  ( ph -> ( E |`s U ) = ( Scalar ` B ) )
96 4 95 syl5eq 
 |-  ( ph -> F = ( Scalar ` B ) )
97 96 fveq2d 
 |-  ( ph -> ( 0g ` F ) = ( 0g ` ( Scalar ` B ) ) )
98 3 7 10 drgext0g 
 |-  ( ph -> ( 0g ` F ) = ( 0g ` C ) )
99 97 98 eqtr3d 
 |-  ( ph -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` C ) )
100 99 adantr 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> ( 0g ` ( Scalar ` B ) ) = ( 0g ` C ) )
101 90 91 100 3eqtr3d 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) )
102 breq1 
 |-  ( g = ( G ` j ) -> ( g finSupp ( 0g ` ( Scalar ` C ) ) <-> ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) ) )
103 fveq1 
 |-  ( g = ( G ` j ) -> ( g ` i ) = ( ( G ` j ) ` i ) )
104 103 oveq1d 
 |-  ( g = ( G ` j ) -> ( ( g ` i ) ( .s ` C ) i ) = ( ( ( G ` j ) ` i ) ( .s ` C ) i ) )
105 104 mpteq2dv 
 |-  ( g = ( G ` j ) -> ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) = ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) )
106 105 oveq2d 
 |-  ( g = ( G ` j ) -> ( C gsum ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) ) = ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
107 106 eqeq1d 
 |-  ( g = ( G ` j ) -> ( ( C gsum ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) <-> ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) )
108 102 107 anbi12d 
 |-  ( g = ( G ` j ) -> ( ( g finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) <-> ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) ) )
109 eqeq1 
 |-  ( g = ( G ` j ) -> ( g = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) <-> ( G ` j ) = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) )
110 108 109 imbi12d 
 |-  ( g = ( G ` j ) -> ( ( ( g finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) -> g = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) <-> ( ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) -> ( G ` j ) = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ) )
111 44 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 116 adantr 
 |-  ( ( ph /\ j e. Y ) -> C e. LMod )
118 eqid 
 |-  ( Base ` C ) = ( Base ` C )
119 eqid 
 |-  ( LBasis ` C ) = ( LBasis ` C )
120 118 119 lbsss 
 |-  ( X e. ( LBasis ` C ) -> X C_ ( Base ` C ) )
121 13 120 syl 
 |-  ( ph -> X C_ ( Base ` C ) )
122 121 adantr 
 |-  ( ( ph /\ j e. Y ) -> X C_ ( Base ` C ) )
123 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
124 118 119 123 islbs4 
 |-  ( X e. ( LBasis ` C ) <-> ( X e. ( LIndS ` C ) /\ ( ( LSpan ` C ) ` X ) = ( Base ` C ) ) )
125 13 124 sylib 
 |-  ( ph -> ( X e. ( LIndS ` C ) /\ ( ( LSpan ` C ) ` X ) = ( Base ` C ) ) )
126 125 simpld 
 |-  ( ph -> X e. ( LIndS ` C ) )
127 126 adantr 
 |-  ( ( ph /\ j e. Y ) -> X e. ( LIndS ` C ) )
128 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
129 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
130 eqid 
 |-  ( .s ` C ) = ( .s ` C )
131 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
132 eqid 
 |-  ( 0g ` ( Scalar ` C ) ) = ( 0g ` ( Scalar ` C ) )
133 118 128 129 130 131 132 islinds5 
 |-  ( ( C e. LMod /\ X C_ ( Base ` C ) ) -> ( X e. ( LIndS ` C ) <-> A. g e. ( ( Base ` ( Scalar ` C ) ) ^m X ) ( ( g finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) -> g = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ) )
134 133 biimpa 
 |-  ( ( ( C e. LMod /\ X C_ ( Base ` C ) ) /\ X e. ( LIndS ` C ) ) -> A. g e. ( ( Base ` ( Scalar ` C ) ) ^m X ) ( ( g finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) -> g = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) )
135 117 122 127 134 syl21anc 
 |-  ( ( ph /\ j e. Y ) -> A. g e. ( ( Base ` ( Scalar ` C ) ) ^m X ) ( ( g finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( g ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) -> g = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) )
136 110 135 66 rspcdva 
 |-  ( ( ph /\ j e. Y ) -> ( ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) /\ ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) -> ( G ` j ) = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) )
137 20 136 mpand 
 |-  ( ( ph /\ j e. Y ) -> ( ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) -> ( G ` j ) = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) )
138 137 imp 
 |-  ( ( ( ph /\ j e. Y ) /\ ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( 0g ` C ) ) -> ( G ` j ) = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) )
139 85 87 101 138 syl21anc 
 |-  ( ( ph /\ j e. ( Y \ ( L supp ( 0g ` ( Scalar ` B ) ) ) ) ) -> ( G ` j ) = ( X X. { ( 0g ` ( Scalar ` C ) ) } ) )
140 19 139 suppss 
 |-  ( ph -> ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) C_ ( L supp ( 0g ` ( Scalar ` B ) ) ) )
141 84 140 ssfid 
 |-  ( ph -> ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) e. Fin )
142 suppssdm 
 |-  ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) C_ dom G
143 142 19 fssdm 
 |-  ( ph -> ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) C_ Y )
144 143 sselda 
 |-  ( ( ph /\ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ) -> w e. Y )
145 eleq1w 
 |-  ( j = w -> ( j e. Y <-> w e. Y ) )
146 145 anbi2d 
 |-  ( j = w -> ( ( ph /\ j e. Y ) <-> ( ph /\ w e. Y ) ) )
147 fveq2 
 |-  ( j = w -> ( G ` j ) = ( G ` w ) )
148 147 breq1d 
 |-  ( j = w -> ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) <-> ( G ` w ) finSupp ( 0g ` ( Scalar ` C ) ) ) )
149 146 148 imbi12d 
 |-  ( j = w -> ( ( ( ph /\ j e. Y ) -> ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) ) <-> ( ( ph /\ w e. Y ) -> ( G ` w ) finSupp ( 0g ` ( Scalar ` C ) ) ) ) )
150 149 20 chvarvv 
 |-  ( ( ph /\ w e. Y ) -> ( G ` w ) finSupp ( 0g ` ( Scalar ` C ) ) )
151 150 fsuppimpd 
 |-  ( ( ph /\ w e. Y ) -> ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) e. Fin )
152 144 151 syldan 
 |-  ( ( ph /\ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ) -> ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) e. Fin )
153 152 ralrimiva 
 |-  ( ph -> A. w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) e. Fin )
154 iunfi 
 |-  ( ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) e. Fin /\ A. w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) e. Fin ) -> U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) e. Fin )
155 141 153 154 syl2anc 
 |-  ( ph -> U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) e. Fin )
156 xpfi 
 |-  ( ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) e. Fin /\ U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) e. Fin ) -> ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) e. Fin )
157 141 155 156 syl2anc 
 |-  ( ph -> ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) e. Fin )
158 fveq2 
 |-  ( v = j -> ( G ` v ) = ( G ` j ) )
159 158 fveq1d 
 |-  ( v = j -> ( ( G ` v ) ` u ) = ( ( G ` j ) ` u ) )
160 159 mpteq2dv 
 |-  ( v = j -> ( u e. X |-> ( ( G ` v ) ` u ) ) = ( u e. X |-> ( ( G ` j ) ` u ) ) )
161 fveq2 
 |-  ( u = i -> ( ( G ` j ) ` u ) = ( ( G ` j ) ` i ) )
162 161 cbvmptv 
 |-  ( u e. X |-> ( ( G ` j ) ` u ) ) = ( i e. X |-> ( ( G ` j ) ` i ) )
163 160 162 eqtrdi 
 |-  ( v = j -> ( u e. X |-> ( ( G ` v ) ` u ) ) = ( i e. X |-> ( ( G ` j ) ` i ) ) )
164 163 cbvmptv 
 |-  ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) = ( j e. Y |-> ( i e. X |-> ( ( G ` j ) ` i ) ) )
165 fvexd 
 |-  ( ph -> ( 0g ` ( Scalar ` C ) ) e. _V )
166 fvexd 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( ( G ` j ) ` i ) e. _V )
167 12 164 14 13 165 166 suppovss 
 |-  ( ph -> ( H supp ( 0g ` ( Scalar ` C ) ) ) C_ ( ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) )
168 5 81 subrg0 
 |-  ( V e. ( SubRing ` E ) -> ( 0g ` E ) = ( 0g ` K ) )
169 34 168 syl 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` K ) )
170 50 fveq2d 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` ( Scalar ` C ) ) )
171 169 170 eqtr2d 
 |-  ( ph -> ( 0g ` ( Scalar ` C ) ) = ( 0g ` E ) )
172 171 oveq2d 
 |-  ( ph -> ( H supp ( 0g ` ( Scalar ` C ) ) ) = ( H supp ( 0g ` E ) ) )
173 19 feqmptd 
 |-  ( ph -> G = ( v e. Y |-> ( G ` v ) ) )
174 eleq1w 
 |-  ( j = v -> ( j e. Y <-> v e. Y ) )
175 174 anbi2d 
 |-  ( j = v -> ( ( ph /\ j e. Y ) <-> ( ph /\ v e. Y ) ) )
176 fveq2 
 |-  ( j = v -> ( G ` j ) = ( G ` v ) )
177 176 feq1d 
 |-  ( j = v -> ( ( G ` j ) : X --> ( Base ` E ) <-> ( G ` v ) : X --> ( Base ` E ) ) )
178 175 177 imbi12d 
 |-  ( j = v -> ( ( ( ph /\ j e. Y ) -> ( G ` j ) : X --> ( Base ` E ) ) <-> ( ( ph /\ v e. Y ) -> ( G ` v ) : X --> ( Base ` E ) ) ) )
179 5 35 ressbas2 
 |-  ( V C_ ( Base ` E ) -> V = ( Base ` K ) )
180 37 179 syl 
 |-  ( ph -> V = ( Base ` K ) )
181 50 fveq2d 
 |-  ( ph -> ( Base ` K ) = ( Base ` ( Scalar ` C ) ) )
182 180 181 eqtrd 
 |-  ( ph -> V = ( Base ` ( Scalar ` C ) ) )
183 182 37 eqsstrrd 
 |-  ( ph -> ( Base ` ( Scalar ` C ) ) C_ ( Base ` E ) )
184 183 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( Base ` ( Scalar ` C ) ) C_ ( Base ` E ) )
185 67 184 fssd 
 |-  ( ( ph /\ j e. Y ) -> ( G ` j ) : X --> ( Base ` E ) )
186 178 185 chvarvv 
 |-  ( ( ph /\ v e. Y ) -> ( G ` v ) : X --> ( Base ` E ) )
187 186 feqmptd 
 |-  ( ( ph /\ v e. Y ) -> ( G ` v ) = ( u e. X |-> ( ( G ` v ) ` u ) ) )
188 187 mpteq2dva 
 |-  ( ph -> ( v e. Y |-> ( G ` v ) ) = ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) )
189 173 188 eqtr2d 
 |-  ( ph -> ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) = G )
190 189 oveq1d 
 |-  ( ph -> ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) = ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) )
191 189 fveq1d 
 |-  ( ph -> ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) ` w ) = ( G ` w ) )
192 191 oveq1d 
 |-  ( ph -> ( ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) ` w ) supp ( 0g ` ( Scalar ` C ) ) ) = ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) )
193 190 192 iuneq12d 
 |-  ( ph -> U_ w e. ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) ` w ) supp ( 0g ` ( Scalar ` C ) ) ) = U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) )
194 190 193 xpeq12d 
 |-  ( ph -> ( ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( ( v e. Y |-> ( u e. X |-> ( ( G ` v ) ` u ) ) ) ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) = ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) )
195 167 172 194 3sstr3d 
 |-  ( ph -> ( H supp ( 0g ` E ) ) C_ ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) )
196 suppssfifsupp 
 |-  ( ( ( H e. ( ( Base ` ( Scalar ` A ) ) ^m ( Y X. X ) ) /\ Fun H /\ ( 0g ` E ) e. ( Base ` E ) ) /\ ( ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) e. Fin /\ ( H supp ( 0g ` E ) ) C_ ( ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) X. U_ w e. ( G supp ( X X. { ( 0g ` ( Scalar ` C ) ) } ) ) ( ( G ` w ) supp ( 0g ` ( Scalar ` C ) ) ) ) ) ) -> H finSupp ( 0g ` E ) )
197 63 77 83 157 195 196 syl32anc 
 |-  ( ph -> H finSupp ( 0g ` E ) )
198 51 fveq2d 
 |-  ( ph -> ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` C ) ) )
199 198 171 eqtr2d 
 |-  ( ph -> ( 0g ` E ) = ( 0g ` ( Scalar ` A ) ) )
200 197 199 breqtrd 
 |-  ( ph -> H finSupp ( 0g ` ( Scalar ` A ) ) )
201 2 6 9 4 7 14 drgextgsum 
 |-  ( ph -> ( E gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) = ( B gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) )
202 13 adantr 
 |-  ( ( ph /\ j e. Y ) -> X e. ( LBasis ` C ) )
203 9 adantr 
 |-  ( ( ph /\ j e. Y ) -> U e. ( SubRing ` E ) )
204 subrgsubg 
 |-  ( U e. ( SubRing ` E ) -> U e. ( SubGrp ` E ) )
205 subgsubm 
 |-  ( U e. ( SubGrp ` E ) -> U e. ( SubMnd ` E ) )
206 203 204 205 3syl 
 |-  ( ( ph /\ j e. Y ) -> U e. ( SubMnd ` E ) )
207 116 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> C e. LMod )
208 67 ffvelrnda 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` C ) ) )
209 121 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> X C_ ( Base ` C ) )
210 209 72 sseldd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> i e. ( Base ` C ) )
211 118 129 130 128 lmodvscl 
 |-  ( ( C e. LMod /\ ( ( G ` j ) ` i ) e. ( Base ` ( Scalar ` C ) ) /\ i e. ( Base ` C ) ) -> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) e. ( Base ` C ) )
212 207 208 210 211 syl3anc 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) e. ( Base ` C ) )
213 4 35 ressbas2 
 |-  ( U C_ ( Base ` E ) -> U = ( Base ` F ) )
214 94 213 syl 
 |-  ( ph -> U = ( Base ` F ) )
215 45 48 srabase 
 |-  ( ph -> ( Base ` F ) = ( Base ` C ) )
216 214 215 eqtrd 
 |-  ( ph -> U = ( Base ` C ) )
217 216 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> U = ( Base ` C ) )
218 212 217 eleqtrrd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) e. U )
219 218 fmpttd 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) : X --> U )
220 202 206 219 4 gsumsubm 
 |-  ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( F gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
221 eqid 
 |-  ( .r ` E ) = ( .r ` E )
222 4 221 ressmulr 
 |-  ( U e. ( SubRing ` E ) -> ( .r ` E ) = ( .r ` F ) )
223 9 222 syl 
 |-  ( ph -> ( .r ` E ) = ( .r ` F ) )
224 45 48 sravsca 
 |-  ( ph -> ( .r ` F ) = ( .s ` C ) )
225 223 224 eqtr2d 
 |-  ( ph -> ( .s ` C ) = ( .r ` E ) )
226 225 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( .s ` C ) = ( .r ` E ) )
227 226 oveqd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) = ( ( ( G ` j ) ` i ) ( .r ` E ) i ) )
228 227 mpteq2dva 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) = ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) )
229 228 oveq2d 
 |-  ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) ) )
230 3 7 10 112 111 13 drgextgsum 
 |-  ( ph -> ( F gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
231 230 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( F gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) = ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
232 220 229 231 3eqtr3d 
 |-  ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) ) = ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) )
233 232 oveq1d 
 |-  ( ( ph /\ j e. Y ) -> ( ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) = ( ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) ( .r ` E ) j ) )
234 79 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> E e. Ring )
235 183 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( Base ` ( Scalar ` C ) ) C_ ( Base ` E ) )
236 235 208 sseldd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( G ` j ) ` i ) e. ( Base ` E ) )
237 216 94 eqsstrrd 
 |-  ( ph -> ( Base ` C ) C_ ( Base ` E ) )
238 121 237 sstrd 
 |-  ( ph -> X C_ ( Base ` E ) )
239 238 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> X C_ ( Base ` E ) )
240 239 72 sseldd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> i e. ( Base ` E ) )
241 eqid 
 |-  ( Base ` B ) = ( Base ` B )
242 eqid 
 |-  ( LBasis ` B ) = ( LBasis ` B )
243 241 242 lbsss 
 |-  ( Y e. ( LBasis ` B ) -> Y C_ ( Base ` B ) )
244 14 243 syl 
 |-  ( ph -> Y C_ ( Base ` B ) )
245 92 94 srabase 
 |-  ( ph -> ( Base ` E ) = ( Base ` B ) )
246 244 245 sseqtrrd 
 |-  ( ph -> Y C_ ( Base ` E ) )
247 246 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> Y C_ ( Base ` E ) )
248 simplr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> j e. Y )
249 247 248 sseldd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> j e. ( Base ` E ) )
250 35 221 ringass 
 |-  ( ( E e. Ring /\ ( ( ( G ` j ) ` i ) e. ( Base ` E ) /\ i e. ( Base ` E ) /\ j e. ( Base ` E ) ) ) -> ( ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ( .r ` E ) j ) = ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) )
251 234 236 240 249 250 syl13anc 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ( .r ` E ) j ) = ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) )
252 251 mpteq2dva 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ( .r ` E ) j ) ) = ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) )
253 252 oveq2d 
 |-  ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X |-> ( ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ( .r ` E ) j ) ) ) = ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) ) )
254 eqid 
 |-  ( +g ` E ) = ( +g ` E )
255 79 adantr 
 |-  ( ( ph /\ j e. Y ) -> E e. Ring )
256 244 adantr 
 |-  ( ( ph /\ j e. Y ) -> Y C_ ( Base ` B ) )
257 245 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( Base ` E ) = ( Base ` B ) )
258 256 257 sseqtrrd 
 |-  ( ( ph /\ j e. Y ) -> Y C_ ( Base ` E ) )
259 simpr 
 |-  ( ( ph /\ j e. Y ) -> j e. Y )
260 258 259 sseldd 
 |-  ( ( ph /\ j e. Y ) -> j e. ( Base ` E ) )
261 35 221 ringcl 
 |-  ( ( E e. Ring /\ ( ( G ` j ) ` i ) e. ( Base ` E ) /\ i e. ( Base ` E ) ) -> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) e. ( Base ` E ) )
262 234 236 240 261 syl3anc 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) e. ( Base ` E ) )
263 171 breq2d 
 |-  ( ph -> ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) <-> ( G ` j ) finSupp ( 0g ` E ) ) )
264 263 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) <-> ( G ` j ) finSupp ( 0g ` E ) ) )
265 20 264 mpbid 
 |-  ( ( ph /\ j e. Y ) -> ( G ` j ) finSupp ( 0g ` E ) )
266 35 255 202 240 185 265 rmfsupp2 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) finSupp ( 0g ` E ) )
267 35 81 254 221 255 202 260 262 266 gsummulc1 
 |-  ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X |-> ( ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ( .r ` E ) j ) ) ) = ( ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) )
268 253 267 eqtr3d 
 |-  ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) ) = ( ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) ) ( .r ` E ) j ) )
269 21 oveq1d 
 |-  ( ( ph /\ j e. Y ) -> ( ( L ` j ) ( .r ` E ) j ) = ( ( C gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .s ` C ) i ) ) ) ( .r ` E ) j ) )
270 233 268 269 3eqtr4rd 
 |-  ( ( ph /\ j e. Y ) -> ( ( L ` j ) ( .r ` E ) j ) = ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) ) )
271 92 94 sravsca 
 |-  ( ph -> ( .r ` E ) = ( .s ` B ) )
272 271 adantr 
 |-  ( ( ph /\ j e. Y ) -> ( .r ` E ) = ( .s ` B ) )
273 272 oveqd 
 |-  ( ( ph /\ j e. Y ) -> ( ( L ` j ) ( .r ` E ) j ) = ( ( L ` j ) ( .s ` B ) j ) )
274 fvexd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( ( G ` j ) ` i ) e. _V )
275 ovexd 
 |-  ( ( ph /\ j e. Y /\ i e. X ) -> ( i ( .r ` E ) j ) e. _V )
276 12 a1i 
 |-  ( ph -> H = ( j e. Y , i e. X |-> ( ( G ` j ) ` i ) ) )
277 11 a1i 
 |-  ( ph -> D = ( j e. Y , i e. X |-> ( i ( .r ` E ) j ) ) )
278 14 13 274 275 276 277 offval22 
 |-  ( ph -> ( H oF ( .r ` E ) D ) = ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) )
279 278 oveqd 
 |-  ( ph -> ( j ( H oF ( .r ` E ) D ) i ) = ( j ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) i ) )
280 279 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j ( H oF ( .r ` E ) D ) i ) = ( j ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) i ) )
281 ovexd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) e. _V )
282 eqid 
 |-  ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) = ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) )
283 282 ovmpt4g 
 |-  ( ( j e. Y /\ i e. X /\ ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) e. _V ) -> ( j ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) i ) = ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) )
284 248 72 281 283 syl3anc 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( j ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) i ) = ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) )
285 280 284 eqtr2d 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) = ( j ( H oF ( .r ` E ) D ) i ) )
286 285 mpteq2dva 
 |-  ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) = ( i e. X |-> ( j ( H oF ( .r ` E ) D ) i ) ) )
287 286 oveq2d 
 |-  ( ( ph /\ j e. Y ) -> ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) ) = ( E gsum ( i e. X |-> ( j ( H oF ( .r ` E ) D ) i ) ) ) )
288 270 273 287 3eqtr3d 
 |-  ( ( ph /\ j e. Y ) -> ( ( L ` j ) ( .s ` B ) j ) = ( E gsum ( i e. X |-> ( j ( H oF ( .r ` E ) D ) i ) ) ) )
289 288 mpteq2dva 
 |-  ( ph -> ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) = ( j e. Y |-> ( E gsum ( i e. X |-> ( j ( H oF ( .r ` E ) D ) i ) ) ) ) )
290 289 oveq2d 
 |-  ( ph -> ( E gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) = ( E gsum ( j e. Y |-> ( E gsum ( i e. X |-> ( j ( H oF ( .r ` E ) D ) i ) ) ) ) ) )
291 ringcmn 
 |-  ( E e. Ring -> E e. CMnd )
292 79 291 syl 
 |-  ( ph -> E e. CMnd )
293 79 adantr 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> E e. Ring )
294 52 183 eqsstrd 
 |-  ( ph -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` E ) )
295 294 adantr 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` E ) )
296 simprl 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> l e. ( Base ` ( Scalar ` A ) ) )
297 295 296 sseldd 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> l e. ( Base ` E ) )
298 simprr 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> k e. ( Base ` A ) )
299 30 37 srabase 
 |-  ( ph -> ( Base ` E ) = ( Base ` A ) )
300 299 adantr 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> ( Base ` E ) = ( Base ` A ) )
301 298 300 eleqtrrd 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> k e. ( Base ` E ) )
302 35 221 ringcl 
 |-  ( ( E e. Ring /\ l e. ( Base ` E ) /\ k e. ( Base ` E ) ) -> ( l ( .r ` E ) k ) e. ( Base ` E ) )
303 293 297 301 302 syl3anc 
 |-  ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> ( l ( .r ` E ) k ) e. ( Base ` E ) )
304 35 221 ringcl 
 |-  ( ( E e. Ring /\ i e. ( Base ` E ) /\ j e. ( Base ` E ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
305 234 240 249 304 syl3anc 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) )
306 299 ad2antrr 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( Base ` E ) = ( Base ` A ) )
307 305 306 eleqtrd 
 |-  ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) )
308 307 anasss 
 |-  ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) )
309 308 ralrimivva 
 |-  ( ph -> A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) )
310 11 fmpo 
 |-  ( A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) <-> D : ( Y X. X ) --> ( Base ` A ) )
311 309 310 sylib 
 |-  ( ph -> D : ( Y X. X ) --> ( Base ` A ) )
312 inidm 
 |-  ( ( Y X. X ) i^i ( Y X. X ) ) = ( Y X. X )
313 303 76 311 59 59 312 off 
 |-  ( ph -> ( H oF ( .r ` E ) D ) : ( Y X. X ) --> ( Base ` E ) )
314 79 adantr 
 |-  ( ( ph /\ u e. ( Base ` A ) ) -> E e. Ring )
315 simpr 
 |-  ( ( ph /\ u e. ( Base ` A ) ) -> u e. ( Base ` A ) )
316 299 adantr 
 |-  ( ( ph /\ u e. ( Base ` A ) ) -> ( Base ` E ) = ( Base ` A ) )
317 315 316 eleqtrrd 
 |-  ( ( ph /\ u e. ( Base ` A ) ) -> u e. ( Base ` E ) )
318 35 221 81 ringlz 
 |-  ( ( E e. Ring /\ u e. ( Base ` E ) ) -> ( ( 0g ` E ) ( .r ` E ) u ) = ( 0g ` E ) )
319 314 317 318 syl2anc 
 |-  ( ( ph /\ u e. ( Base ` A ) ) -> ( ( 0g ` E ) ( .r ` E ) u ) = ( 0g ` E ) )
320 59 83 83 76 311 197 319 offinsupp1 
 |-  ( ph -> ( H oF ( .r ` E ) D ) finSupp ( 0g ` E ) )
321 35 81 292 14 13 313 320 gsumxp 
 |-  ( ph -> ( E gsum ( H oF ( .r ` E ) D ) ) = ( E gsum ( j e. Y |-> ( E gsum ( i e. X |-> ( j ( H oF ( .r ` E ) D ) i ) ) ) ) ) )
322 30 37 sravsca 
 |-  ( ph -> ( .r ` E ) = ( .s ` A ) )
323 322 ofeqd 
 |-  ( ph -> oF ( .r ` E ) = oF ( .s ` A ) )
324 323 oveqd 
 |-  ( ph -> ( H oF ( .r ` E ) D ) = ( H oF ( .s ` A ) D ) )
325 324 oveq2d 
 |-  ( ph -> ( E gsum ( H oF ( .r ` E ) D ) ) = ( E gsum ( H oF ( .s ` A ) D ) ) )
326 290 321 325 3eqtr2rd 
 |-  ( ph -> ( E gsum ( H oF ( .s ` A ) D ) ) = ( E gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) )
327 ovexd 
 |-  ( ph -> ( H oF ( .s ` A ) D ) e. _V )
328 15 elfvexd 
 |-  ( ph -> A e. _V )
329 1 327 6 328 37 gsumsra 
 |-  ( ph -> ( E gsum ( H oF ( .s ` A ) D ) ) = ( A gsum ( H oF ( .s ` A ) D ) ) )
330 326 329 eqtr3d 
 |-  ( ph -> ( E gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) = ( A gsum ( H oF ( .s ` A ) D ) ) )
331 18 201 330 3eqtr2d 
 |-  ( ph -> Z = ( A gsum ( H oF ( .s ` A ) D ) ) )
332 200 331 jca 
 |-  ( ph -> ( H finSupp ( 0g ` ( Scalar ` A ) ) /\ Z = ( A gsum ( H oF ( .s ` A ) D ) ) ) )