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↾𝑠U
fedgmul.k ⊢K=E↾𝑠V
fedgmul.1 ⊢φ→E∈DivRing
fedgmul.2 ⊢φ→F∈DivRing
fedgmul.3 ⊢φ→K∈DivRing
fedgmul.4 ⊢φ→U∈SubRing⁡E
fedgmul.5 ⊢φ→V∈SubRing⁡F
fedgmullem.d ⊢D=j∈Y,i∈X⟼i⋅Ej
fedgmullem.h ⊢H=j∈Y,i∈X⟼G⁡j⁡i
fedgmullem.x ⊢φ→X∈LBasis⁡C
fedgmullem.y ⊢φ→Y∈LBasis⁡B
fedgmullem1.a ⊢φ→Z∈BaseA
fedgmullem1.l ⊢φ→L:Y⟶BaseScalar⁡B
fedgmullem1.1 ⊢φ→finSupp0Scalar⁡B⁡L
fedgmullem1.z ⊢φ→Z=∑Bj∈YL⁡j⋅Bj
fedgmullem1.g ⊢φ→G:Y⟶BaseScalar⁡CX
fedgmullem1.2 ⊢φ∧j∈Y→finSupp0Scalar⁡C⁡G⁡j
fedgmullem1.3 ⊢φ∧j∈Y→L⁡j=∑Ci∈XG⁡j⁡i⋅Ci
Assertion fedgmullem1 ⊢φ→finSupp0Scalar⁡A⁡H∧Z=∑AH⋅AfD

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