| 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
|
ffvelcdmd |
|- ( ( ( ( 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
|
ffvelcdmd |
|- ( ( ( 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
|
eqtrid |
|- ( 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
|
ffvelcdmda |
|- ( ( 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
|
ffvelcdmd |
|- ( ( ( 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
|
eqtrid |
|- ( 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
|
ffvelcdmda |
|- ( ( ( 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 |
79
|
adantr |
|- ( ( ph /\ j e. Y ) -> E e. Ring ) |
| 255 |
244
|
adantr |
|- ( ( ph /\ j e. Y ) -> Y C_ ( Base ` B ) ) |
| 256 |
245
|
adantr |
|- ( ( ph /\ j e. Y ) -> ( Base ` E ) = ( Base ` B ) ) |
| 257 |
255 256
|
sseqtrrd |
|- ( ( ph /\ j e. Y ) -> Y C_ ( Base ` E ) ) |
| 258 |
|
simpr |
|- ( ( ph /\ j e. Y ) -> j e. Y ) |
| 259 |
257 258
|
sseldd |
|- ( ( ph /\ j e. Y ) -> j e. ( Base ` E ) ) |
| 260 |
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 ) ) |
| 261 |
234 236 240 260
|
syl3anc |
|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) e. ( Base ` E ) ) |
| 262 |
171
|
breq2d |
|- ( ph -> ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) <-> ( G ` j ) finSupp ( 0g ` E ) ) ) |
| 263 |
262
|
adantr |
|- ( ( ph /\ j e. Y ) -> ( ( G ` j ) finSupp ( 0g ` ( Scalar ` C ) ) <-> ( G ` j ) finSupp ( 0g ` E ) ) ) |
| 264 |
20 263
|
mpbid |
|- ( ( ph /\ j e. Y ) -> ( G ` j ) finSupp ( 0g ` E ) ) |
| 265 |
35 254 202 240 185 264
|
rmfsupp2 |
|- ( ( ph /\ j e. Y ) -> ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) i ) ) finSupp ( 0g ` E ) ) |
| 266 |
35 81 221 254 202 259 261 265
|
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 ) ) |
| 267 |
253 266
|
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 ) ) |
| 268 |
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 ) ) |
| 269 |
233 267 268
|
3eqtr4rd |
|- ( ( ph /\ j e. Y ) -> ( ( L ` j ) ( .r ` E ) j ) = ( E gsum ( i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) ) ) |
| 270 |
92 94
|
sravsca |
|- ( ph -> ( .r ` E ) = ( .s ` B ) ) |
| 271 |
270
|
adantr |
|- ( ( ph /\ j e. Y ) -> ( .r ` E ) = ( .s ` B ) ) |
| 272 |
271
|
oveqd |
|- ( ( ph /\ j e. Y ) -> ( ( L ` j ) ( .r ` E ) j ) = ( ( L ` j ) ( .s ` B ) j ) ) |
| 273 |
|
fvexd |
|- ( ( ph /\ j e. Y /\ i e. X ) -> ( ( G ` j ) ` i ) e. _V ) |
| 274 |
|
ovexd |
|- ( ( ph /\ j e. Y /\ i e. X ) -> ( i ( .r ` E ) j ) e. _V ) |
| 275 |
12
|
a1i |
|- ( ph -> H = ( j e. Y , i e. X |-> ( ( G ` j ) ` i ) ) ) |
| 276 |
11
|
a1i |
|- ( ph -> D = ( j e. Y , i e. X |-> ( i ( .r ` E ) j ) ) ) |
| 277 |
14 13 273 274 275 276
|
offval22 |
|- ( ph -> ( H oF ( .r ` E ) D ) = ( j e. Y , i e. X |-> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) ) ) |
| 278 |
277
|
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 ) ) |
| 279 |
278
|
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 ) ) |
| 280 |
|
ovexd |
|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) e. _V ) |
| 281 |
|
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 ) ) ) |
| 282 |
281
|
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 ) ) ) |
| 283 |
248 72 280 282
|
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 ) ) ) |
| 284 |
279 283
|
eqtr2d |
|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( ( ( G ` j ) ` i ) ( .r ` E ) ( i ( .r ` E ) j ) ) = ( j ( H oF ( .r ` E ) D ) i ) ) |
| 285 |
284
|
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 ) ) ) |
| 286 |
285
|
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 ) ) ) ) |
| 287 |
269 272 286
|
3eqtr3d |
|- ( ( ph /\ j e. Y ) -> ( ( L ` j ) ( .s ` B ) j ) = ( E gsum ( i e. X |-> ( j ( H oF ( .r ` E ) D ) i ) ) ) ) |
| 288 |
287
|
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 ) ) ) ) ) |
| 289 |
288
|
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 ) ) ) ) ) ) |
| 290 |
|
ringcmn |
|- ( E e. Ring -> E e. CMnd ) |
| 291 |
79 290
|
syl |
|- ( ph -> E e. CMnd ) |
| 292 |
79
|
adantr |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> E e. Ring ) |
| 293 |
52 183
|
eqsstrd |
|- ( ph -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` E ) ) |
| 294 |
293
|
adantr |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> ( Base ` ( Scalar ` A ) ) C_ ( Base ` E ) ) |
| 295 |
|
simprl |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> l e. ( Base ` ( Scalar ` A ) ) ) |
| 296 |
294 295
|
sseldd |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> l e. ( Base ` E ) ) |
| 297 |
|
simprr |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> k e. ( Base ` A ) ) |
| 298 |
30 37
|
srabase |
|- ( ph -> ( Base ` E ) = ( Base ` A ) ) |
| 299 |
298
|
adantr |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> ( Base ` E ) = ( Base ` A ) ) |
| 300 |
297 299
|
eleqtrrd |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> k e. ( Base ` E ) ) |
| 301 |
35 221
|
ringcl |
|- ( ( E e. Ring /\ l e. ( Base ` E ) /\ k e. ( Base ` E ) ) -> ( l ( .r ` E ) k ) e. ( Base ` E ) ) |
| 302 |
292 296 300 301
|
syl3anc |
|- ( ( ph /\ ( l e. ( Base ` ( Scalar ` A ) ) /\ k e. ( Base ` A ) ) ) -> ( l ( .r ` E ) k ) e. ( Base ` E ) ) |
| 303 |
35 221
|
ringcl |
|- ( ( E e. Ring /\ i e. ( Base ` E ) /\ j e. ( Base ` E ) ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) ) |
| 304 |
234 240 249 303
|
syl3anc |
|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( i ( .r ` E ) j ) e. ( Base ` E ) ) |
| 305 |
298
|
ad2antrr |
|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( Base ` E ) = ( Base ` A ) ) |
| 306 |
304 305
|
eleqtrd |
|- ( ( ( ph /\ j e. Y ) /\ i e. X ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) ) |
| 307 |
306
|
anasss |
|- ( ( ph /\ ( j e. Y /\ i e. X ) ) -> ( i ( .r ` E ) j ) e. ( Base ` A ) ) |
| 308 |
307
|
ralrimivva |
|- ( ph -> A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) ) |
| 309 |
11
|
fmpo |
|- ( A. j e. Y A. i e. X ( i ( .r ` E ) j ) e. ( Base ` A ) <-> D : ( Y X. X ) --> ( Base ` A ) ) |
| 310 |
308 309
|
sylib |
|- ( ph -> D : ( Y X. X ) --> ( Base ` A ) ) |
| 311 |
|
inidm |
|- ( ( Y X. X ) i^i ( Y X. X ) ) = ( Y X. X ) |
| 312 |
302 76 310 59 59 311
|
off |
|- ( ph -> ( H oF ( .r ` E ) D ) : ( Y X. X ) --> ( Base ` E ) ) |
| 313 |
79
|
adantr |
|- ( ( ph /\ u e. ( Base ` A ) ) -> E e. Ring ) |
| 314 |
|
simpr |
|- ( ( ph /\ u e. ( Base ` A ) ) -> u e. ( Base ` A ) ) |
| 315 |
298
|
adantr |
|- ( ( ph /\ u e. ( Base ` A ) ) -> ( Base ` E ) = ( Base ` A ) ) |
| 316 |
314 315
|
eleqtrrd |
|- ( ( ph /\ u e. ( Base ` A ) ) -> u e. ( Base ` E ) ) |
| 317 |
35 221 81
|
ringlz |
|- ( ( E e. Ring /\ u e. ( Base ` E ) ) -> ( ( 0g ` E ) ( .r ` E ) u ) = ( 0g ` E ) ) |
| 318 |
313 316 317
|
syl2anc |
|- ( ( ph /\ u e. ( Base ` A ) ) -> ( ( 0g ` E ) ( .r ` E ) u ) = ( 0g ` E ) ) |
| 319 |
59 83 83 76 310 197 318
|
offinsupp1 |
|- ( ph -> ( H oF ( .r ` E ) D ) finSupp ( 0g ` E ) ) |
| 320 |
35 81 291 14 13 312 319
|
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 ) ) ) ) ) ) |
| 321 |
30 37
|
sravsca |
|- ( ph -> ( .r ` E ) = ( .s ` A ) ) |
| 322 |
321
|
ofeqd |
|- ( ph -> oF ( .r ` E ) = oF ( .s ` A ) ) |
| 323 |
322
|
oveqd |
|- ( ph -> ( H oF ( .r ` E ) D ) = ( H oF ( .s ` A ) D ) ) |
| 324 |
323
|
oveq2d |
|- ( ph -> ( E gsum ( H oF ( .r ` E ) D ) ) = ( E gsum ( H oF ( .s ` A ) D ) ) ) |
| 325 |
289 320 324
|
3eqtr2rd |
|- ( ph -> ( E gsum ( H oF ( .s ` A ) D ) ) = ( E gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) ) |
| 326 |
|
ovexd |
|- ( ph -> ( H oF ( .s ` A ) D ) e. _V ) |
| 327 |
15
|
elfvexd |
|- ( ph -> A e. _V ) |
| 328 |
1 326 6 327 37
|
gsumsra |
|- ( ph -> ( E gsum ( H oF ( .s ` A ) D ) ) = ( A gsum ( H oF ( .s ` A ) D ) ) ) |
| 329 |
325 328
|
eqtr3d |
|- ( ph -> ( E gsum ( j e. Y |-> ( ( L ` j ) ( .s ` B ) j ) ) ) = ( A gsum ( H oF ( .s ` A ) D ) ) ) |
| 330 |
18 201 329
|
3eqtr2d |
|- ( ph -> Z = ( A gsum ( H oF ( .s ` A ) D ) ) ) |
| 331 |
200 330
|
jca |
|- ( ph -> ( H finSupp ( 0g ` ( Scalar ` A ) ) /\ Z = ( A gsum ( H oF ( .s ` A ) D ) ) ) ) |